用少量形式化+编辑，高效筛选数学推理答案。
Formalize Once, Edit the Rest: Efficient Lean-Based Answer Selection for Math Reasoning
- 先形式化一个基准答案，其余通过修改生成。
- 在K=8时减少约5倍形式化调用，准确率不降。
- 适合需要大量候选答案的数学推理任务。
随着大语言模型在数学推理中的应用增多，形式化证明助手如Lean可用来以机器可验证的方式检验推理结果，支持测试时扩展中选择多个候选答案。然而，使用Lean需将自然语言输出转化为形式化陈述，现有方法对每个候选答案独立进行自动形式化，计算开销巨大。本文提出BASE框架：为每道题仅形式化一个基础答案，其余K-1个答案通过修改该基础形式化内容生成。为此，训练了重写模型LEANSCRIBE，能定位基础形式化中的答案部分，并生成可复用的编辑函数。BASE在四个基准数据集、三个求解器共12种配置下均实现准确率提升与形式化成本降低，达到帕累托改进；当K=8时，自动形式化调用减少约5倍，且随K增大优势更明显。代码已开源。
原文摘要 · Abstract (English)
With large language models (LLMs) increasingly applied to mathematical reasoning, formal proof assistants such as Lean can be leveraged to verify reasoning outputs with machine-checkable rigor, enabling use cases such as answer selection in test-time scaling with K sampled candidate answers. However, employing Lean requires that LLM outputs, originally in natural language, first be formalized. Existing Lean-based answer-selection work uses an autoformalization model to generate a formal statement in Lean for each candidate answer independently, incurring a significant computational cost. We propose BASE, a base-and-edit pipeline that formalizes a single base candidate per problem and derives the remaining K-1 statements by editing the answer expression in place. To facilitate this, we train a rewriter model LEANSCRIBE to localize the answer in the base formalization and generate a reusable edit function for the other K-1 candidates. BASE simultaneously improves selection accuracy and reduces formalization cost - a Pareto improvement that holds on all 12 (dataset, solver) configurations across four benchmarks and three solvers, cutting autoformalizer calls by about 5x at K=8, with the reduction expected to become larger as K grows. Code is available at https://github.com/ucr-rai/base-and-edit.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。