一次形式化，其余皆编辑：基于 Lean 的高效数学推理答案选择

随着大语言模型在数学推理中的应用日益广泛，利用 Lean 等形式化证明助手可机器严谨地验证推理输出。现有方法需对每个候选答案独立进行形式化，计算成本高昂。本文提出 BASE 框架，采用“基础 - 编辑”流水线：仅对单个基础候选进行形式化，并通过训练重写模型 LEANSCRIBE 定位答案并生成编辑函数，从而推导其余候选的形式化陈述。该方法在四个基准测试中显著降低了形式化成本（约 5 倍），同时提升了答案选择的准确率。