Technical Summary: Formalize Once, Edit the Rest (BASE)

1. Problem Statement

As Large Language Models (LLMs) are increasingly applied to mathematical reasoning, they often generate multiple distinct reasoning paths and candidate answers for a single problem. A critical challenge arises in answer selection: how to verify which candidate is correct without access to ground-truth labels during test-time scaling.

While existing approaches like majority voting or learned reward models offer statistical signals, they lack formal guarantees. Recent work has leveraged formal proof assistants (specifically Lean 4) to verify candidates. In this paradigm, an "autoformalizer" translates a problem and a candidate answer into a Lean theorem statement asserting the answer's correctness. A prover then attempts to verify this statement.

However, a significant bottleneck exists: to verify $K$ candidate answers, the autoformalizer must be invoked $K$ times independently. This incurs a computational cost of $\Theta(K)$, which scales linearly with the number of samples. The authors observe that for a single problem, the $K$ formal statements are nearly identical, sharing the same problem structure and differing only in the answer expression. The core problem is how to exploit this shared structure to reduce formalization costs from $\Theta(K)$ to $\Theta(1)$ without sacrificing selection accuracy.

2. Methodology: The BASE Pipeline

The authors propose BASE (Base-and-Substitute-Edit), a pipeline designed to formalize a single "base" candidate and derive the remaining $K-1$ statements through localized editing.

2.1 Base Discovery

The pipeline begins with an upstream solver generating a ranked list of $K$ candidate answers, $S(x) = (a_1, \dots, a_K)$, ordered by the solver's confidence.

• The system iterates through candidates in rank order.
• For each candidate $a_i$, it attempts to formalize the problem-answer pair $(x, a_i)$ into a Lean statement $F_i$.
• The process stops at the first candidate $a_b$ whose formalization $F_b$ successfully type-checks in Lean.
• $F_b$ becomes the base formalization, and $a_b$ is the base answer.
• If no candidate type-checks, the system falls back to the top-ranked candidate $a_1$.

2.2 Substitution Cascade

Once a valid base $F_b$ is established, the system generates the remaining $K-1$ statements by editing $F_b$ in place to reflect the other candidates. This is handled by a two-tier cascade:

1. Tier 1 (R1): Rule-Based Direct Localization

   • The system attempts to locate the answer expression in $F_b$ via exact string matching within a "gated region" (the theorem body, excluding comments/headers).
   • If a unique match is found, the system performs a direct substitution of the answer string.
   • If multiple matches occur, a small disambiguation model selects the correct slot.
   • This tier is efficient but fails when the autoformalizer encodes the answer in a syntactically diverse form (e.g., a tuple (3, 5) encoded as separate bindings or a Prod value) rather than a verbatim string.

2. Tier 2 (R2): LEANSCRIBE (Learned Rewriter)

   • For cases where R1 fails, the system invokes LEANSCRIBE, a specialized fine-tuned LLM.
   • Input: The problem $x$, the base formalization $F_b$, and the base answer $a_b$.
   • Output:
     • A local block $s$: A contiguous segment of $F_b$ containing the answer-dependent expression.
     • A fill function $f$: A lightweight Python function that maps any informal answer $a_i$ to the corresponding Lean expression replacing $s$.
   • Execution: LEANSCRIBE runs once per problem. The generated function $f$ is then applied to all remaining candidates $a_i$ to produce their formal statements $F_i = f(a_i)$. This amortizes the cost of the model call across all $K-1$ candidates.

2.3 Verification and Selection

The pipeline relies on statement-level type-checking as the primary selection signal.

• A candidate is considered "verified" if its formal statement $F_i$ type-checks in Lean (i.e., is a well-formed proposition).
• The system selects the highest-ranked candidate $a_j$ such that $F_j$ type-checks.
• If no candidate type-checks, it falls back to the top-ranked candidate $a_1$.
• The authors note that while proof-level verification (running a prover) is more rigorous, current provers have low pass@1 rates, making statement-level type-checking a more practical signal for selection in this budget-constrained setting.

3. Key Contributions

1. BASE Pipeline: The first work to amortize formalization costs by sharing a single verified base statement across multiple candidates, reducing autoformalizer calls from $\Theta(K)$ to $\Theta(1)$.
2. LEANSCRIBE Model: A learned rewriter trained to localize answer-dependent blocks and generate reusable edit functions, handling syntactic variations that rule-based substitution cannot.
3. Pareto Improvement: The method achieves higher selection accuracy while significantly reducing computational cost across all tested configurations.

4. Experimental Results

The authors evaluated BASE on four benchmarks (MATH-500, OlympiadBench, AMC-AIMO, AIME 2024) using three different upstream solvers (Gemini 3 Pro, Qwen3-8B, DeepSeek-R1-Qwen3-8B) with $K=8$ candidates.

• Accuracy: BASE improved selection accuracy (Acc) in all 12 (dataset, solver) configurations compared to independent formalization, with gains ranging from +0.7 to +23.3 percentage points.
• Robustness: The "Gold-Answer Pass" rate (GT-pass)—the fraction of problems where the correct answer's statement type-checks—increased significantly (up to +33.3 points), reaching 96–100% in many cases. This indicates that sharing a verified base makes the formalization of the correct answer more robust.
• Cost Efficiency: At $K=8$, BASE reduced the number of autoformalizer calls by approximately 5.4× (mean reduction of 4.7–6.5×). The cost scales as $\Theta(1)$ rather than $\Theta(K)$.
• Ablation: Removing the learned rewriter (LEANSCRIBE) and relying solely on rule-based substitution (R1) resulted in a significant drop in candidate coverage (8–22 percentage points), demonstrating the necessity of the learned component for handling diverse syntactic encodings.
• Proof-Level Analysis: Even when using a prover (DeepSeek-Prover-V2) with a single attempt per candidate, BASE improved proof-level accuracy in 11 out of 12 configurations, suggesting that better-structured formal statements aid downstream provers.

5. Significance and Claims

The paper claims that BASE represents a Pareto improvement for Lean-based answer selection. By formalizing once and editing the rest, the method simultaneously:

• Reduces Cost: Drastically lowers the inference cost of formal verification, making test-time scaling with large $K$ more feasible.
• Improves Accuracy: Enhances the reliability of selecting the correct answer, likely because the shared base structure reduces the variance and failure rate of the autoformalizer for the correct candidate.

The authors emphasize that this approach is a "drop-in replacement" for the formalization stage in existing pipelines (demonstrated by integrating it into the FANS pipeline) and that the gains are driven by the verifier's ability to retain correct answers more effectively when a shared, verified scaffold is used, rather than by changes in the upstream solver's generation.

The work acknowledges limitations, noting that it focuses on statement-level type-checking due to current prover limitations and assumes that candidate answers share a problem-side structure. It does not claim to solve the faithfulness of autoformalization (where an incorrect answer might still type-check) but suggests that combining formal signals with solver rankings mitigates this risk.