Formalize Once, Edit the Rest: Efficient Lean-Based Answer Selection for Math Reasoning
For LLM-based math reasoning systems using formal verification, BASE offers a Pareto improvement in efficiency and accuracy, addressing the computational bottleneck of autoformalization.
The paper proposes BASE, a base-and-edit pipeline for Lean-based answer selection in math reasoning that formalizes one candidate per problem and edits the answer expression for others, reducing autoformalizer calls by about 5x at K=8 while improving selection accuracy across 12 configurations.
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.