Paper deep dive
Formalize Once, Edit the Rest: Efficient Lean-Based Answer Selection for Math Reasoning
Ji Feng, Zhouxing Shi
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 99%
Last extracted: 6/20/2026, 7:37:06 AM
Summary
The paper introduces BASE (Base-And-Substitute-Edit), an efficient pipeline for mathematical answer selection using the Lean 4 proof assistant. Instead of the computationally expensive approach of autoformalizing every candidate answer independently, BASE formalizes a single 'base' candidate and derives the remaining K-1 statements by editing the answer expression in place. The core of the method is LeanScribe, a specialized LLM-based rewriter that localizes the answer in the base formalization and generates a reusable Python function to transform other informal answers into the correct formal syntax. Experiments across four math benchmarks (MATH-500, OlympiadBench, AMC-AIMO, AIME 2024) and three solvers show that BASE achieves a Pareto improvement, increasing selection accuracy while reducing autoformalizer calls by approximately 5x at K=8.
Entities (10)
Relation Signals (5)
LeanScribe → isbasedon → Qwen3-8b
confidence 100% · For the learned rewriter LeanScribe (Section 3.3), it is based on Qwen3-8B (Yang et al., 2025) fine-tuned via LoRA
Kimina-Autoformalizer-7B → isusedas → autoformalizer
confidence 100% · For verification, the autoformalizer F is Kimina-Autoformalizer-7B
BASE → uses → LeanScribe
confidence 100% · To facilitate this, we train a rewriter model LEANSCRIBE to localize the answer in the base formalization and generate a reusable edit function
BASE → verifieswith → Lean 4
confidence 100% · formal proof assistants such as Lean can be leveraged to verify reasoning outputs
BASE → improvesaccuracyon → MATH-500
confidence 90% · Across four benchmarks and three solvers, Base improves selection accuracy on all twelve (dataset, solver) configurations
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract: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 this https URL.
Tags
Links
- Source: https://arxiv.org/abs/2606.15972v1
- Canonical: https://arxiv.org/abs/2606.15972v1
Trouble viewing inline? Open PDF directly →
Full Text
62,582 characters extracted from source content.
Expand or collapse full text
Formalize Once, Edit the Rest: Efficient Lean-Based Answer Selection for Math Reasoning Ji Feng and Zhouxing Shi University of California, Riverside jfeng080, zhouxing.shi@ucr.edu Abstract 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−1K-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−1K-1 candidates. Base simultaneously improves selection accuracy and reduces formalization cost—a Pareto improvement that holds on all 1212 (dataset, solver) configurations across four benchmarks and three solvers, cutting autoformalizer calls by about 5×5× at K=8K=8, with the reduction expected to become larger as K grows. Code is available at https://github.com/ucr-rai/base-and-edit. Formalize Once, Edit the Rest: Efficient Lean-Based Answer Selection for Math Reasoning Ji Feng and Zhouxing Shi University of California, Riverside jfeng080, zhouxing.shi@ucr.edu 1 Introduction Figure 1: The Base pipeline. An upstream solver emits K ranked candidate answers; Base autoformalizes them in rank order until one type-checks, giving the base statement FbF_b (a failure triggers “try next answer”). A two-tier cascade—R1 direct substitution and R2 LeanScribe—edits FbF_b into the remaining K−1K-1 statements, and the highest-ranked type-checking candidate is selected. As large language models (LLMs) tackle increasingly hard mathematical reasoning tasks, they can often generate distinct reasoning paths for a given problem. In particular, for computational problems that require a concrete answer, as opposed to theorem-proving tasks for which only a proof is required, such reasoning paths often arrive at different answers, which raises a fundamental question: how to verify which answer is correct? The paradigm of sampling a large number of answers and selecting among them is an instance of test-time scaling and has driven much of the recent progress on mathematical reasoning (Snell et al., 2025; Brown et al., 2024). A central challenge, however, lies in the selection step—choosing the correct answer without access to a ground-truth label. The dominant approaches are majority voting (Wang et al., 2023) and best-of-N selection with learned reward models (Cobbe et al., 2021; Lightman et al., 2024), the former relying on consensus within the candidate set and the latter on a scalar score. However, majority voting is a heuristic and fails when the correct answer is in the minority; reward models are typically black boxes. More fundamentally, both provide no formal guarantee of correctness. To address this, a recent line of work leverages a formal verifier (Zhou et al., 2024; Yao et al., 2025). For each candidate answer, the problem and the answer are jointly formalized by an LLM known as an autoformalizer (Wang et al., 2025) into a Lean 4 (Moura and Ullrich, 2021) theorem statement asserting that the candidate is the correct answer to the problem; a prover then attempts to prove this statement (Ren et al., 2025; Lin et al., 2025b; Liu et al., 2026), with the proof verified by the Lean 4 compiler. The highest-ranked provable candidate is then selected. This paradigm is grounded in formal mathematics, as a statement with a verified proof is guaranteed to be correct. This reliability, however, introduces a significant computational cost — to verify K candidates for a single problem, the autoformalization model is invoked K times, once per candidate. We observe, however, that the K statements for one problem are nearly identical: they typically share the same problem structure and differ only in the answer slots. A correct formalization of any one candidate already captures this shared structure; thus the remaining K−1K-1 statements can in principle be obtained by reusing one formalization and editing the answer expression in place. Realizing this efficiency gain, however, is nontrivial, as candidate answers often do not appear verbatim in the Lean statement but are instead encoded in syntactically diverse forms. Therefore, reuse often requires localizing and rewriting the answer-bearing expression rather than a simple string substitution alone. In this work, we exploit the shared structure across a problem’s candidate statements for efficient formalization, taking a step toward scalable Lean-based verification for computational problems. Specifically, we propose Base (Base-And-Substitute-Edit; base-and-edit for short), an answer-selection pipeline that reuses a type-checked base formalization, i.e., a Lean statement accepted by the compiler as well-formed. In this pipeline, an upstream solver first produces a list of K candidate answers ranked by its own confidence—highest first. Rather than formalizing all K candidate statements independently, Base formalizes them in rank order until one type-checks, and this type-checked base statement is then reused across the remaining candidates, deriving the remaining statements by editing only the answer expression in place. This editing step is the technical core, handled by a two-tier cascade: a rule-based substitution for answers that appear verbatim in the base statement, and LeanScribe, a learned rewriter we train, for the syntactically diverse forms that rules cannot reach. Base then returns the highest-ranked type-checked candidate, without invoking the autoformalizer for all K candidates. In this work, Base focuses on efficient statement formalization and treats proof generation as orthogonal, leaving its efficiency to future work; nevertheless, statement-level type-checking already serves as an effective selection signal (Section 3.4). Figure 1 gives an overview and our contributions are summarized below: 1. Pipeline. We propose Base, an answer-selection pipeline that efficiently formalizes K candidates by formalizing a single base candidate and deriving the remaining K−1K-1 statements with localized answer edits, thereby reducing the autoformalizer cost from Θ(K) (K) to Θ(1) (1). To our knowledge, this is the first work to amortize formalization through a shared base. Base also serves as an efficient drop-in replacement for the per-candidate formalization stage in existing formal-selection pipelines (Section 5.5). 2. Model. We introduce LeanScribe, a learned rewriter model trained to localize and re-express answers across diverse formal encodings. It is lightweight and invoked only once per problem, generating a reusable edit function applied to all K−1K-1 candidates. 3. Experiments. Across four benchmarks and three solvers, Base improves selection accuracy on all twelve (dataset, solver) configurations (up to +23+23 percentage points) while reducing formalization cost by roughly 5×5×—a Pareto improvement over independent formalization. 2 Related Work Answer selection for math reasoning. Step-by-step reasoning (Wei et al., 2022) with many sampled candidates is often adopted for math reasoning (Lewkowycz et al., 2022; Azerbayev et al., 2024). Without gold labels, candidates are usually selected by majority voting (Wang et al., 2023) or a learned reward model—outcome- (Cobbe et al., 2021), process- (Uesato et al., 2022; Lightman et al., 2024; Wang et al., 2024), or generative (Zhang et al., 2024)—with related work on test-time compute allocation (Snell et al., 2025). These signals are statistical rather than formal, offering no guarantee of correctness. Formal verification for mathematical reasoning. A growing line of work incorporates a proof assistant for mathematical reasoning. Fans (Yao et al., 2025) formalizes each candidate answer into a Lean 4 theorem and selects among verified ones; Safe (Liu et al., 2025) applies Lean 4 verification to verify reasoning steps. Others integrate Lean into the reasoning loop (Ospanov et al., 2025b) or repair proofs from compiler feedback (Ospanov et al., 2025a). However, these approaches formalize each statement independently, so the autoformalization cost scales linearly with the number of statements (Yao et al., 2025; Ospanov et al., 2025b; Lu et al., 2026), and the shared structure across them is left unexploited. Autoformalization and theorem proving. Autoformalization aims to translate natural-language mathematics into formal languages such as Lean (Moura and Ullrich, 2021). Existing work trains specialized models and builds pipelines for autoformalizing individual statements (Lu et al., 2025; Wang et al., 2025; Gao et al., 2025; Chan et al., 2025; Guo et al., 2025b) and proofs (Cabral et al., 2025; Jana et al., 2025), each targeting a single statement or proof at a time. Automated theorem provers generate or search for machine-checkable proofs of given formal statements. Modern approaches are commonly LLM-based, including next-tactic prediction (Polu and Sutskever, 2020; Lample et al., 2022; Yang et al., 2023) and whole-proof generation (Ren et al., 2025; Xin et al., 2025a; Lin et al., 2025a; Xin et al., 2025b). In this work, we focus on the efficient autoformalization of statements across multiple candidates, and our pipeline builds on existing autoformalization and prover models as underlying components. 3 Method We design a pipeline for efficient Lean-based answer selection. Given an informal mathematics problem x, we first elicit a ranked list of K distinct candidate answers (x)=(a1,…,aK)S(x)=(a_1,…,a_K) from an upstream LLM solver S in a single generation call. We then formalize each problem-answer pair (x,ai)(x,a_i) as a Lean 4 theorem statement, type-check the statements, and return the highest-ranked candidate whose verification passes (falling back to the top candidate if none does) (Section 3.4). A naive instantiation of this pipeline requires a separate autoformalizer call for each of the K candidates, which we call independent formalization. In contrast, with our proposed Base (Section 3.2), we derive the remaining K−1K-1 formal statements from a single successfully formalized and type-checked base statement, via a two-tier cascade of a rule-based rewriter and LeanScribe—a learned answer rewriter we train (Section 3.3). 3.1 Candidate Generation The upstream solver S produces a ranked list of K distinct candidate answers, ordered by the solver’s own confidence: higher-ranked candidates are those the solver believes more likely to be correct. We obtain this list from a single generation call for simplicity. The selection method described below, however, is agnostic to how the candidates are produced and may be applied to candidates independently sampled through different reasoning paths. We denote the solver’s output as (x)=(a1,a2,…,aK),S(x)=(a_1,a_2,…,a_K), where a1≺a2≺⋯≺aKa_1 a_2 ·s a_K reflects the solver’s preference: a1a_1 is the most likely candidate, aKa_K the least. We use this ordering both during formalization and as a tiebreaker during selection. 3.2 Formalization: Independent and Base-and-Edit To verify a candidate answer aia_i with Lean, we translate the problem and that specific answer into a formal theorem statement FiF_i using an answer-conditioned autoformalizer ℱF: Fi=ℱ(x,ai),i=1,…,K.F_i=F(x,a_i), i=1,…,K. Each statement FiF_i asserts that aia_i is the correct answer to x. We describe two strategies for generating these statements: a costly baseline (independent formalization) and our proposed efficient approach (base-and-edit). Independent formalization (baseline). In this brute-force approach, ℱF is invoked independently for each candidate, incurring K autoformalizer calls per problem. This matches the per-candidate strategy of prior formal answer-selection pipelines (Yao et al., 2025) and serves as our efficiency reference point. Base-and-edit (Base). In contrast, we propose Base, which replaces these K independent formalizations with one formalization plus K−1K-1 local edits. It proceeds in two steps: base discovery and a substitution cascade. Base discovery. We iterate candidates in rank order; for each aia_i, we compute Fi=ℱ(x,ai)F_i=F(x,a_i) and check whether FiF_i type-checks in Lean. Let b=mini:Fi type-checks.b= \\,i:F_i type-checks\,\. (1) When such a b exists, FbF_b becomes the base formalization and aba_b the base answer. Base discovery requires at most b autoformalizer calls, and since recent autoformalizers (Wang et al., 2025) achieve a high compilation rate, b is typically small and thus the base discovery effectively costs only Θ(1) (1) autoformalizer calls in practice. If no candidate type-checks, we fall back to the top-ranked candidate a1a_1, which is rare (1.5%1.5\% of problems overall; Appendix F) and identical for both strategies. Substitution cascade. Given (Fb,ab)(F_b,a_b), the cascade evaluates each remaining candidate aia_i (i≠bi≠ b) by constructing Fb→iF_b→ i, a modified statement that reuses FbF_b’s structure with only the answer expression replaced by aia_i. The cascade applies two tiers of increasing flexibility. The first tier (R1) is a rule-based direct localization: it locates the base answer aba_b by exact string matching within the gated region of FbF_b, where the gate is a filter that restricts matches to the theorem statement body and excludes other parts such as comments and headers (Appendix B). A unique match gives the substitution site directly; when aba_b matches at several positions, a small disambiguation model conditioned on the statement (Appendix C) selects the occurrence that serves as the answer slot. R1 is cheap and exact, but it fails whenever the autoformalizer does not encode the answer as a verbatim copy of aba_b. For these cases the second tier (R2) invokes LeanScribe, the answer rewriter we train (Section 3.3). For each candidate, the cascade applies R1 when direct localization and insertion are feasible, and otherwise falls back to R2 (Algorithm 1). Algorithm 1 Base substitution cascade 1:base statement FbF_b, base answer aba_b, candidate aia_i 2:←Gate(Fb,ab)P← Gate(F_b,a_b) ⊳ valid substitution sites for aba_b 3:⊳ R1: direct localization 4:if ||≥1|P|≥ 1 then 5: if ||=1|P|=1 then 6: p←p← unique element of P 7: else 8: p←Disambig(Fb,)p← Disambig(F_b,P) 9: return Substitute(Fb,p,ai) Substitute(F_b,p,a_i) 10:⊳ R2: predict local block s and fill function f 11:(s,f)←LeanScribe(x,Fb,ab)(s,f)← LeanScribe(x,F_b,a_b) 12:if Gate(Fb,s) Gate(F_b,s) is a singleton then 13: return Substitute(Fb,s,f(ai)) Substitute(F_b,s,f(a_i)) 14:return ⊥ ⊳ no substitution for aia_i 3.3 LeanScribe: Learned Semantic Localization and Rewriting Model The forms that defeat R1 span a broad range. For example, a tuple “(3,5)(3,5)” may be formalized as two bindings (a = 3, b = 5) or as a single Prod value ((3, 5) : ℕN × ℕN), so often no verbatim “(3,5)(3,5)” substring exists to be replaced. Similarly, intervals, sets, and symbolic forms require structural rewrites that no string match can produce—“[0,2)[0,2)” becomes Set.Ico 0 2 and “3133 13” becomes 3 * Real.sqrt 13. In each case, the surrounding theorem structure binds the answer. Locating and rewriting it thus requires modeling how the autoformalizer encoded the answer in context, which is a semantic-parsing problem rather than a string-matching one. To this end, we propose LeanScribe, a specialized fine-tuned LLM. Given (x,Fb,ab)(x,F_b,a_b), it (i) predicts a contiguous, answer-dependent local block s within FbF_b (localization) and (i) generates a lightweight Python function f mapping any informal answer to the Lean expression that replaces s (transformation). Editing only this block preserves the verified base structure, and the reusability of f allows the cost of a single model call to be amortized across all K−1K-1 candidates: we run f on each aia_i (i≠bi≠ b) to obtain Fi=f(ai)F_i\!=\!f(a_i), effectively replacing the answer expression of aba_b with that of aia_i while leaving the rest of FbF_b intact. Figure 2 shows a concrete example. LeanScribe input Problem x. “Find the distance between (2,−6)(2,-6) and (−4,3)(-4,3).” Base answer aba_b. 3 13 Base formalization FbF_b. theorem ex : xxReal.sqrt ((2+4)ˆ2 + (-6-3)ˆ2) x= 3 * Real.sqrt 13 := by sorry LeanScribe output Local block s. "3 * Real.sqrt 13" Fill function g. def fill_answer(a: str) -> str: xxm = re.match(r’( +) ( +)’, a) xxreturn f"m[1] * Real.sqrt m[2]" Inference. For each remaining candidate aia_i (e.g. 2 13), the cascade replaces this block in FbF_b with fill_answer(ai)(a_i); LeanScribe runs once per problem, and the synthesized function runs once per remaining candidate. Figure 2: LeanScribe prediction on a MATH-500 distance problem. The model identifies the answer-dependent local block in FbF_b and generates a Python function that converts any informal answer of the same shape into the corresponding Lean expression. To train LeanScribe, we construct a training dataset via a Lean-filtered expert iteration, inspired by prior work training reasoning models or theorem provers (Zelikman et al., 2022; Lin et al., 2025a): we iteratively collect model predictions, retain only those whose outputs pass the Lean type-check, and incorporate the accepted predictions into the training dataset for supervised fine-tuning (SFT). We first build a seed dataset from NuminaMath (Li et al., 2024): for each problem we autoformalize the gold answer with ℱF to obtain a base statement, predict local blocks and fill functions using the base model, and keep only those whose reconstructed statements pass a Lean type-check. The seed dataset is used for the first iteration of training. For subsequent iterations, using the current LeanScribe checkpoint, we generate block/function predictions on a broader set of problems, particularly previously failed examples, and expand the training dataset with the additional type-checked predictions. A new, stronger LeanScribe model is trained by SFT at each iteration as the dataset grows. 3.4 Verification and Selection Each formal statement FiF_i, encoding a particular candidate answer aia_i, is verified at two levels. The statement level involves a Lean type-check: ci=1c_i=1 iff the Lean 4 compiler accepts FiF_i as a well-formed proposition asserting aia_i as the answer. The proof level is stricter: a prover attempts a proof for the given type-checked statement, and the Lean kernel then verifies the proof, giving pi=1p_i=1 iff the proof passes Lean verification. In this work, we focus on efficient statement formalization. Proof-level verification, while more rigorous, remains too limited in coverage to serve as a practical selection signal: although current provers achieve strong performance at large pass@K (Ren et al., 2025; Lin et al., 2025a; Liu et al., 2026), their pass@1 success rates remain low (Section 5.4), making proof-level selection impractical at the single-attempt budget we target. We therefore base selection on the statement-level signal cic_i and leave efficient proof generation to future work. A statement-level type-check certifies well-formedness of FiF_i rather than mathematical truth of aia_i, so selecting by cic_i is a practical choice that does not yet provide a correctness guarantee for the selected answer, a gap we expect stronger and more efficient provers to close in future work. Nevertheless, since the autoformalizer encodes the answer into a typed expression, a structurally inconsistent answer is more likely to yield an ill-typed statement, and combined with the solver’s ranking this proves an effective selection signal in practice (Sections 5.3, 5.4). We study proof-level verification separately in Section 5.4. Given the signals c1,…,cK\c_1,…,c_K\ and the solver’s rank order a1≺⋯≺aKa_1 ·s a_K (Section 3.1), we return the highest-ranked type-checking candidate: a^=aj∗,j∗=minj:cj=1, a=a_j^*, j^*= \\,j:c_j=1\,\, (2) falling back to a1a_1 if none type-checks. This design combines the formal type-check signal with the solver’s ranking as a tiebreaker, requiring no separate reward model. 4 Experimental Settings 4.1 Datasets We evaluate on four mathematics benchmarks requiring concrete answers, spanning high-school olympiad to Putnam-level difficulty: MATH-500 (Lightman et al., 2024; Hendrycks et al., 2021), comprising the standard 500500-problem subset of MATH; OlympiadBench (He et al., 2024), 566566 English single-answer olympiad problems; AMC-AIMO (AI-MO, 2024), 8383 AMC12 problems (2022–2023) from the AIMO validation set; and AIME 2024 (AI-MO, 2024), the 3030 problems from the 2024 AIME. Answer types range from integers and rationals to algebraic expressions, intervals, sets, and natural-language descriptors; subset selection and answer normalization are detailed in Appendix A. 4.2 Models and Implementation To assess generality across solver families, we use three upstream solvers for generating candidates: Gemini 3 Pro, Qwen3-8B (Yang et al., 2025), and DeepSeek-R1-0528-Qwen3-8B (Guo et al., 2025a) (R1-Qwen3-8B in tables), all at K=8K=8. For verification, the autoformalizer ℱF is Kimina-Autoformalizer-7B (Wang et al., 2025); type-checking uses the Lean 4 compiler (Moura and Ullrich, 2021), and the proof step uses DeepSeek-Prover-V2-7B (Ren et al., 2025) with a single greedy attempt per type-checked statement. For the learned rewriter LeanScribe (Section 3.3), it is based on Qwen3-8B (Yang et al., 2025) fine-tuned via LoRA on the expert-iterated training dataset with details in Appendix C. All inference runs on a single RTX PRO 6000 GPU with vLLM and greedy decoding, and Lean 4 (Moura and Ullrich, 2021) verification uses Mathlib 4 (mathlib Community, 2020) with a 6060s per-statement timeout. 4.3 Baseline and Metrics Baseline. We compare primarily against independent formalization (Section 3.2): the same pipeline but with K independent autoformalizer calls, instead of one base call plus K−1K-1 local edits. We use identical verifier components, prompts, and selection rule for both methods, so any difference is attributable to the formalization strategy. Metrics. All main results use the statement-level signal (type-check); the proof level is studied separately (Section 5.4), and “verification” means the statement level unless noted. Acc is the fraction of problems whose selected answer equals the gold answer. GT@K is the fraction whose gold answer appears in the ranked list (determined solely by the upstream solver and thus identical for both methods), and Acc | GT@K is Acc on that subset, isolating verifier quality; thereby, Acc=GT@K⋅Acc|GT@KAcc=GT@K·Acc\,|\,GT@K. For verifier diagnostics, GT-pass is the fraction whose gold statement type-checks and P-cand the average fraction of candidate statements that type-check (ablation only). For computational costs, we report autoformalizer calls per problem. 5 Main Results 5.1 Accuracy Table 1 reports our main result: Base’s end-to-end accuracy (Acc) and gold-pass rate (GT-pass) across four datasets and three upstream solvers, against the independent formalization baseline. The pattern is consistent across solvers and datasets. Base exceeds independent formalization on Acc in all twelve (dataset, solver) cells, with gains from +0.7+0.7 to +23.3+23.3 points. It also raises GT-pass in all twelve cells (up to +33.3+33.3 points, remaining high across all cells, 9696–100%100\%): the gold candidate’s statement almost always survives under Base, so sharing a verified base makes the gold formalization markedly more robust. Acc (%) GT-pass (%) Dataset Solver Indep. Base (ours) Indep. Base (ours) MATH-500 Gemini 3 Pro 70.2 79.4+9.2 87.3 98.7+11.4 Qwen3-8B 45.7 51.2+5.5 88.2 96.3+8.1 R1-Qwen3-8B 58.7 67.5+8.8 85.4 98.8+13.4 OlympiadBench Gemini 3 Pro 41.7 53.4+11.7 77.6 99.0+21.4 Qwen3-8B 31.6 39.7+8.1 80.4 98.1+17.7 R1-Qwen3-8B 42.8 53.2+10.4 79.4 100.0+20.6 AMC-AIMO Gemini 3 Pro 73.5 86.7+13.2 82.9 100.0+17.1 Qwen3-8B 37.8 46.8+9.0 72.9 97.9+25.0 R1-Qwen3-8B 67.5 85.0+17.5 81.2 100.0+18.8 AIME 2024 Gemini 3 Pro 40.0 63.3+23.3 66.7 100.0+33.3 Qwen3-8B 20.0 20.7+0.7 85.7 100.0+14.3 R1-Qwen3-8B 44.8 60.7+15.9 73.7 100.0+26.3 Table 1: Main results across four datasets and three upstream solvers (K=8K=8). Indep.==independent formalization. 5.2 Cost Table 2 gives the per-problem formalization cost. The autoformalizer dominates pipeline cost and is where the two pipelines differ in scaling: the baseline issues one call per candidate (Θ(K) (K)), while Base issues one base call plus at most one substitution call, giving Θ(1) (1) cost determined by the base rank b(≈1.5)b\,(≈1.5). The substitution call invokes LeanScribe once per problem to predict a reusable edit function (Section 3.3); this single prediction is applied to all K−1K-1 candidates and is far cheaper than the K−1K-1 autoformalizer calls it replaces, so it does not affect the Θ(1) (1) scaling. At K=8K=8 this is b/K=0.19×b/K=0.19× of independent formalization—a 4.74.7–6.5×6.5× reduction (mean 5.4×5.4×)—and the gap widens with K. Together with the accuracy result of Section 5.1, Base is strictly cheaper while never less accurate across all twelve configurations, achieving a Pareto improvement. Dataset Gemini 3 Pro Qwen3-8B R1-Qwen3-8B MATH-500 1.23 1.29 1.23 AMC-AIMO 1.49 1.65 1.43 AIME 2024 1.67 1.50 1.70 OlympiadBench 1.65 1.57 1.45 Table 2: Per-problem formalization cost of Base (average number of base-discovery calls). In contrast, the independent formalization baseline requires K=8K=8 autoformalizer calls per problem. 5.3 Ablations Dataset Indep. Base −-R2 ΔR2 _R2 MATH-500 87.5 87.9 67.9 +20.0 AMC-AIMO 76.6 93.9 85.6 +8.3 AIME 2024 76.1 82.6 60.1 +22.5 OlympiadBench 76.8 86.4 67.7 +18.7 Table 3: Component ablation (P-cand %, Gemini, K=8K=8). “Indep.” is the baseline; Base uses both R1 and R2; “−-R2” disables R2, leaving R1 only; “ΔR2 _R2” indicates the contribution of R2 on top of using R1 only. Table 3 isolates the contribution of LeanScribe, the learned answer rewriter (R2). The ablation study is performed on MATH-500 (Gemini K=8K=8), measured by the per-candidate Lean pass rate (P-cand)—the fraction of all candidate statements that verify. Removing R2 leaves only the rule-based localization tier (R1). LeanScribe accounts for 88 to 2222 points of per-candidate coverage (ΔR2 _ R2). Rule-only localization (R1) handles answers appearing as verbatim substrings of the base, but LeanScribe recovers many candidates that encode answers differently; the two tiers are thus complementary, with R1 covering easy verbatim edits and R2 the harder cases. LeanScribe also generalizes out of distribution: although fine-tuned only on NuminaMath (Section 4.2), it attains high GT-pass on every benchmark (Table 1, 9696–100%100\%), indicating that its localization-and-rewriting behavior transfers rather than memorizing NuminaMath patterns, with residual failures concentrated on very long answer expressions and unusual geometric constructions. 5.4 Proof-level analysis We also run the full pipeline that further consists of proving the formal statements with a prover, and we first use DeepSeek-Prover-V2 (Ren et al., 2025). This studies whether the statement-level gains carry through to a prover that must close each theorem. Prior work on provers typically reports pass@k with a large k, sampling many proof attempts per theorem. In our setting, however, each of the K candidate answers needs its own proof, so a large k for sampling proofs would multiply the prover cost by a factor of K and is impractical. We therefore use a single pass@1 proof attempt per candidate. Dataset Gemini 3 Pro Qwen3-8B R1-Qwen3-8B MATH-500 31.4+3.9 25.9+3.2 28.4+3.2 AMC-AIMO 13.3+3.5 8.9+1.3 16.2+5.0 AIME 2024 6.7+3.4 6.9+3.5 3.6−-7.1 OlympiadBench 11.9+2.8 11.2+2.5 11.8+3.3 Table 4: Proof-level accuracy (%) for Base, compared against the independent formalization baseline with gains denoted in the subscripts. We use K=8K=8 for candidates and DeepSeek-Prover-V2 for the prover. Table 4 shows the results. We notice that the proof-level accuracies are low (44–31%31\%) compared to results in Table 1, which is because of the limited capability of the prover under the single-attempt budget. Nevertheless, we still compare Base against independent formalization in each setting, which is the focus of this work. Base improves proof-level accuracy on 11 out of 12 cells (sign test p=0.006p=0.006), the lone exception being the smallest cell (AIME-2024, R1-Qwen3-8B, n=28n=28). This echoes prior findings that the quality of the formal statement shapes how a downstream prover fares (Jiang et al., 2023; Wu et al., 2022). The per-candidate false-positive rate—an incorrect answer receiving a complete proof—is a low ∼7% 7\% on average (11–14%14\% across cells), arising when the autoformalizer renders an incorrect answer as a statement that type-checks and admits a proof. Given such false positives, we combine the formal signal with the solver’s ranking rather than relying on a single proof. Swapping the prover. Base feeds type-checked candidates to an off-the-shelf prover, so the prover should be interchangeable. Replacing DeepSeek-Prover-V2 with Kimina-Prover-Preview-Distill-7B (Wang et al., 2025) (Table 5), the two are close on MATH-500 but DeepSeek-Prover-V2 is about twice as strong on AMC-AIMO. The advantage is dataset-dependent, and base-and-edit is agnostic to the prover used. Dataset Prover Complete (%) GT-complete (%) MATH-500 DSP-V2 7.3+0.8 31.4+2.3 Kimina 6.5 29.1 AMC-AIMO DSP-V2 8.1+3.9 14.5+6.1 Kimina 4.2 8.4 Table 5: Prover swap on Base-formalized candidates. Complete/GT-complete: candidate-level and gold-answer proof-completion rates. 5.5 Drop-in for an Existing Pipeline Dataset Calls (Indep.→ ) Acc MATH-500 4000→6894000→ 689 (5.8×5.8× ↓ ) 88.2→88.688.2→ 88.6 AMC-AIMO 664→116664→ 116 (5.7×5.7× ↓ ) 62.7→61.462.7→ 61.4 AIME 2024 240→53240→ 53 (4.5×4.5× ↓ ) 13.3→13.313.3→ 13.3 Table 6: Dropping Base into a Fans-style majority-voting pipeline (Qwen2.5-Math-7B-Instruct, K=8K=8) by replacing only the formalization stage. Calls: autoformalizer calls per dataset; Acc: selection accuracy (%). Our Base pipeline described in Section 3 is streamlined to focus on the formalization stage and enable efficient formalization for K candidates. In practice, Lean-based answer selection can be more sophisticated and can contain proving statements in addition to formalization. Our efficient base-and-edit formalization in Base can be seamlessly integrated into other Lean-based answer-selection pipelines. We demonstrate this with Fans (Yao et al., 2025), which generates proofs for statements, checks consistency between natural language and formal language with a QwQ-32B judge, and enhances the selection by majority vote. We use candidate answers from Qwen2.5-Math-7B-Instruct, following Fans, and sample K=8K=8 candidates. Keeping other components fixed, we replace only the formalization stage: Fans originally uses independent formalization; in contrast, we derive one Lean-verified base statement and edit it for the rest. In this way, we isolate the impact of our improved autoformalization, and compare the number of autoformalizer calls and final selection accuracy under an otherwise identical downstream pipeline. Table 6 shows the results, with experimental details in Appendix D. Our Base cuts autoformalizer calls by 4.54.5–5.8×5.8× while maintaining accuracy. This demonstrates that Base is a flexible and efficient module that can be integrated into other pipelines, such as Fans, that make contributions orthogonal to efficient autoformalization for Lean-based answer-selection. 6 Mechanism and Analysis Factorizing the gain. End-to-end accuracy factorizes cleanly into Acc=GT@K⋅Acc|GT@K,Acc=GT@K·Acc\,|\,GT@K, (3) where the first factor depends mostly on the upstream solver (both methods score the same candidate list) and the second is the verifier’s conversion rate on solver-correct problems, so any sizable difference in AccAcc comes from the verifier. Table 7 confirms this on MATH-500: GT@KGT@K is essentially identical across methods, while Base’s Acc|GT@KAcc\,|\,GT@K is uniformly higher across all three solvers. The gain is thus a verifier effect: Base does not change which answers the solver proposes, but raises the rate at which a solver-correct answer is retained. Solver Method GT@KGT@K Acc|GT@KAcc\,|\,GT@K AccAcc Gemini 3 Pro Indep. 80.4 87.3 70.2 Base 80.6 98.5 79.4 Qwen3-8B Indep. 60.9 75.0 45.7 Base 60.7 84.3 51.2 R1-Qwen3-8B Indep. 69.0 85.1 58.7 Base 68.8 98.2 67.5 Table 7: Factorization on MATH-500 (%). Where the gain comes from: the shared verified base. Setting GT-pass P-cand Acc Acc || GT@K Indep. baseline 81.9 81.2 39.3 66.7 First verified base 98.2 91.7 47.1 79.5 Random verified base 95.4 91.2 45.6 77.0 Table 8: Ablating the shared verified base (%) on a matched set of OlympiadBench, AMC-AIMO, and AIME 2024. To trace the gain to the shared verified base, we compare three strategies on the same candidate lists (Table 8). Both variants that reuse a single verified base—Base, which reuses the first type-checking candidate, and a control that reuses a random one—outperform independent formalization, and crucially first ≈ random: the benefit comes from structural reuse, not from cherry-picking a good formalization. This traces to one mechanism—sharing a single verified scaffold rather than formalizing independently. Statistically, sharing cuts per-candidate formalization noise (6.3×6.3× lower pairwise variance, though only part of the story: r=0.22r=0.22 with per-problem gains); mechanistically, every candidate inherits the base’s verified structure rather than risking its own autoformalizer failure. Either way, sharing raises the type-check rate by +9.9+9.9 points (Appendix G). 7 Conclusion We present Base, a base-and-edit approach to formal answer selection that formalizes a single verified base per problem and derives the remaining candidates by editing only the answer block. Replacing K independent autoformalizer calls with one base call plus localized edits cuts formalization cost from Θ(K) (K) to Θ(1) (1) while improving selection accuracy—a Pareto improvement on all twelve configurations. Our analysis traces the gain to the verifier and the use of shared base formalization. We believe this work will enable more practical answer-selection and verification for natural-language reasoning with Lean. Acknowledgement This work is supported in part by an NVIDIA Academic Grant Program award. This work used the Delta system at the National Center for Supercomputing Applications [award OAC 2005572] through allocation CIS250704 from the Advanced Cyberinfrastructure Coordination Ecosystem: Services & Support (ACCESS) program, which is supported by National Science Foundation grants #2138259, #2138286, #2138307, #2137603, and #2138296. Limitations This work focuses on the efficiency of statement autoformalization for K candidate answers, and we use statement-level type-checking as the selection signal due to the limitation of provers. Future work is needed to address the efficiency of provers when handling K relevant theorem statements for the candidate answers, and enable an efficient answer-selection with both statement autoformalization and theorem proving. In our method, base-and-edit assumes the K candidate answers share problem-side structure so that a single base formalization can be reused; this holds for the tasks we study but may not transfer to settings where each candidate requires a structurally different statement. Lastly, since we find that prover can appear to complete proofs for some of the incorrect answers, the faithfulness of autoformalization remains a challenge for future work. Ethics Statement This work studies answer selection for mathematical reasoning using public benchmarks (MATH-500, OlympiadBench, AMC-AIMO, AIME 2024) and models; it involves no human subjects, no private or personally identifiable data, and no sensitive content. LeanScribe is fine-tuned on the openly available NuminaMath dataset. The primary intended use is reducing the inference cost of formal answer verification while improving the reliability, which lowers the energy and compute footprint of test-time scaling rather than increasing it. As we emphasize in Section 5.4, a single Lean proof is not a standalone correctness guarantee; practitioners should not treat the formal signal as infallible certification, particularly in high-stakes settings, since residual errors can arise from mis-formalization. We see no foreseeable risk of harm specific to this work beyond those general to mathematical reasoning systems. References AI-MO (2024) AI-MO. 2024. AIMO validation datasets (AMC, AIME). https://huggingface.co/AI-MO. Azerbayev et al. (2024) Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen Marcus McAleer, Albert Q. Jiang, Jia Deng, Stella Biderman, and Sean Welleck. 2024. Llemma: An open language model for mathematics. In The Twelfth International Conference on Learning Representations. Brown et al. (2024) Bradley Brown, Jordan Juravsky, Ryan Ehrlich, Ronald Clark, Quoc V Le, Christopher Ré, and Azalia Mirhoseini. 2024. Large language monkeys: Scaling inference compute with repeated sampling. arXiv preprint arXiv:2407.21787. Cabral et al. (2025) Rafael Cabral, Tuan Manh Do, Xuejun Yu, Wai Ming Tai, Zijin Feng, and Xin Shen. 2025. Proofflow: A dependency graph approach to faithful proof autoformalization. arXiv preprint arXiv:2510.15981. Chan et al. (2025) Willy Chan, Michael Souliman, Jakob Nordhagen, Brando Miranda, and Sanmi Koyejo. 2025. Lean-ing on quality: How high-quality data beats diverse multilingual data in autoformalization. Cobbe et al. (2021) Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, and 1 others. 2021. Training verifiers to solve math word problems. arXiv preprint arXiv:2110.14168. Gao et al. (2025) Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. 2025. Herald: A natural language annotated lean 4 dataset. In The Thirteenth International Conference on Learning Representations. Guo et al. (2025a) Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Peiyi Wang, Qihao Zhu, Runxin Xu, Ruoyu Zhang, Shirong Ma, Xiao Bi, Xiaokang Zhang, Xingkai Yu, Yu Wu, Z. F. Wu, Zhibin Gou, Zhihong Shao, Zhuoshu Li, Ziyi Gao, Aixin Liu, and 175 others. 2025a. Deepseek-r1 incentivizes reasoning in llms through reinforcement learning. Nature, 645(8081). Guo et al. (2025b) Qi Guo, Jianing Wang, Jianfei Zhang, Deyang Kong, Xiangzhou Huang, Xiangyu Xi, Wei Wang, Jingang Wang, Xunliang Cai, Shikun Zhang, and 1 others. 2025b. Autoformalizer with tool feedback. arXiv preprint arXiv:2510.06857. He et al. (2024) Chaoqun He, Renjie Luo, Yuzhuo Bai, Shengding Hu, Zhen Thai, Junhao Shen, Jinyi Hu, Xu Han, Yujie Huang, Yuxiang Zhang, and 1 others. 2024. Olympiadbench: A challenging benchmark for promoting agi with olympiad-level bilingual multimodal scientific problems. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 3828–3850. Hendrycks et al. (2021) Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. 2021. Measuring mathematical problem solving with the MATH dataset. In Thirty-fifth Conference on Neural Information Processing Systems Datasets and Benchmarks Track (Round 2). Jana et al. (2025) Prithwish Jana, Kaan Kale, Ahmet Ege Tanriverdi, Cruise Song, Sriram Vishwanath, and Vijay Ganesh. 2025. Proofbridge: Auto-formalization of natural language proofs in lean via joint embeddings. arXiv preprint arXiv:2510.15681. Jiang et al. (2023) Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. 2023. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representations. Lample et al. (2022) Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. 2022. Hypertree proof search for neural theorem proving. Advances in neural information processing systems, 35:26337–26349. Lewkowycz et al. (2022) Aitor Lewkowycz, Anders Johan Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay Venkatesh Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra. 2022. Solving quantitative reasoning problems with language models. In Advances in Neural Information Processing Systems. Li et al. (2024) Jia Li, Edward Beeching, Lewis Tunstall, Ben Lipkin, Roman Soletskyi, Shengyi Huang, Kashif Rasul, Longhui Yu, Albert Q Jiang, Ziju Shen, and 1 others. 2024. Numinamath: The largest public dataset in ai4maths with 860k pairs of competition math problems and solutions. Hugging Face repository, 13(9):9. Lightman et al. (2024) Hunter Lightman, Vineet Kosaraju, Yuri Burda, Harrison Edwards, Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever, and Karl Cobbe. 2024. Let’s verify step by step. In The Twelfth International Conference on Learning Representations. Lin et al. (2025a) Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia LI, Mengzhou Xia, Danqi Chen, Sanjeev Arora, and Chi Jin. 2025a. Goedel-prover: A frontier model for open-source automated theorem proving. In Second Conference on Language Modeling. Lin et al. (2025b) Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, and 1 others. 2025b. Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction. arXiv preprint arXiv:2508.03613. Liu et al. (2025) Chengwu Liu, Ye Yuan, Yichun Yin, Yan Xu, Xin Xu, Zaoyu Chen, Yasheng Wang, Lifeng Shang, Qun Liu, and Ming Zhang. 2025. Safe: Enhancing mathematical reasoning in large language models via retrospective step-aware formal verification. In Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 12171–12186. Liu et al. (2026) Junqi Liu, Zihao Zhou, Zekai Zhu, Marco Dos Santos, Weikun He, Jiawei Liu, Ran Wang, Yunzhou Xie, Junqiao Zhao, Qiufeng Wang, and 1 others. 2026. Numina-lean-agent: An open and general agentic reasoning system for formal mathematics. arXiv preprint arXiv:2601.14027. Lu et al. (2026) Haijian Lu, Wei Wang, and Jing Liu. 2026. Formalevolve: Neuro-symbolic evolutionary search for diverse and prover-effective autoformalization. Preprint, arXiv:2603.19828. Lu et al. (2025) Jianqiao Lu, Yingjia Wan, Zhengying Liu, Yinya Huang, Jing Xiong, Liu Chengwu, Jianhao Shen, Hui Jin, Jipeng Zhang, Haiming Wang, Zhicheng Yang, Jing Tang, and Zhijiang Guo. 2025. Process-driven autoformalization in lean 4. mathlib Community (2020) The mathlib Community. 2020. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, page 367–381. ACM. Moura and Ullrich (2021) Leonardo de Moura and Sebastian Ullrich. 2021. The lean 4 theorem prover and programming language. In International Conference on Automated Deduction, pages 625–635. Springer. Ospanov et al. (2025a) Azim Ospanov, Farzan Farnia, and Roozbeh Yousefzadeh. 2025a. APOLLO: Automated LLM and lean collaboration for advanced formal reasoning. In The Thirty-ninth Annual Conference on Neural Information Processing Systems. Ospanov et al. (2025b) Azim Ospanov, Zijin Feng, Jiacheng Sun, Haoli Bai, Xin Shen, and Farzan Farnia. 2025b. Hermes: Towards efficient and verifiable mathematical reasoning in llms. Preprint, arXiv:2511.18760. Polu and Sutskever (2020) Stanislas Polu and Ilya Sutskever. 2020. Generative language modeling for automated theorem proving. Preprint, arXiv:2009.03393. Ren et al. (2025) Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, and Chong Ruan. 2025. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. Preprint, arXiv:2504.21801. Snell et al. (2025) Charlie Victor Snell, Jaehoon Lee, Kelvin Xu, and Aviral Kumar. 2025. Scaling LLM test-time compute optimally can be more effective than scaling parameters for reasoning. In The Thirteenth International Conference on Learning Representations. Uesato et al. (2022) Jonathan Uesato, Nate Kushman, Ramana Kumar, Francis Song, Noah Siegel, Lisa Wang, Antonia Creswell, Geoffrey Irving, and Irina Higgins. 2022. Solving math word problems with process-and outcome-based feedback. arXiv preprint arXiv:2211.14275. Wang et al. (2025) Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, Jianqiao Lu, Hugues de Saxcé, Bolton Bailey, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, and 21 others. 2025. Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. Preprint, arXiv:2504.11354. Wang et al. (2024) Peiyi Wang, Lei Li, Zhihong Shao, Runxin Xu, Damai Dai, Yifei Li, Deli Chen, Yu Wu, and Zhifang Sui. 2024. Math-shepherd: Verify and reinforce LLMs step-by-step without human annotations. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 9426–9439, Bangkok, Thailand. Association for Computational Linguistics. Wang et al. (2023) Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc V Le, Ed H. Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou. 2023. Self-consistency improves chain of thought reasoning in language models. In The Eleventh International Conference on Learning Representations. Wei et al. (2022) Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Fei Xia, Ed Chi, Quoc V Le, Denny Zhou, and 1 others. 2022. Chain-of-thought prompting elicits reasoning in large language models. Advances in neural information processing systems, 35:24824–24837. Wu et al. (2022) Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Norman Rabe, Charles E Staats, Mateja Jamnik, and Christian Szegedy. 2022. Autoformalization with large language models. In Advances in Neural Information Processing Systems. Xin et al. (2025a) Huajian Xin, Z.Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Haowei Zhang, Qihao Zhu, Dejian Yang, Zhibin Gou, Z.F. Wu, Fuli Luo, and Chong Ruan. 2025a. Deepseek-prover-v1.5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. In The Thirteenth International Conference on Learning Representations. Xin et al. (2025b) Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Ming Ding. 2025b. BFS-prover: Scalable best-first tree search for LLM-based automatic theorem proving. In Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 32588–32599, Vienna, Austria. Association for Computational Linguistics. Yang et al. (2025) An Yang, Anfeng Li, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chang Gao, Chengen Huang, Chenxu Lv, Chujie Zheng, Dayiheng Liu, Fan Zhou, Fei Huang, Feng Hu, Hao Ge, Haoran Wei, Huan Lin, Jialong Tang, and 41 others. 2025. Qwen3 technical report. Preprint, arXiv:2505.09388. Yang et al. (2023) Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. 2023. Leandojo: Theorem proving with retrieval-augmented language models. Advances in Neural Information Processing Systems, 36:21573–21612. Yao et al. (2025) Jiarui Yao, Ruida Wang, and Tong Zhang. 2025. FANS: Formal answer selection for LLM natural language math reasoning using lean4. In Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing, pages 3181–3200, Suzhou, China. Association for Computational Linguistics. Zelikman et al. (2022) Eric Zelikman, Yuhuai Wu, Jesse Mu, and Noah Goodman. 2022. Star: Bootstrapping reasoning with reasoning. Advances in Neural Information Processing Systems, 35:15476–15488. Zhang et al. (2024) Lunjun Zhang, Arian Hosseini, Hritik Bansal, Mehran Kazemi, Aviral Kumar, and Rishabh Agarwal. 2024. Generative verifiers: Reward modeling as next-token prediction. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24. Zhou et al. (2024) Jin Zhou, Charles Staats, Wenda Li, Christian Szegedy, Kilian Weinberger, and Yuhuai Wu. 2024. Don’t trust: Verify–grounding llm quantitative reasoning with autoformalization. In International Conference on Learning Representations, volume 2024, pages 2544–2563. Appendix A Dataset Details MATH-500 is the 500500-problem evaluation subset (Lightman et al., 2024) of MATH (Hendrycks et al., 2021). OlympiadBench (He et al., 2024): we use the English mathematics open-ended subset, restricted to single-answer problems with Numerical or Expression answer types, yielding 566566 problems; proof-only problems are excluded as they fall outside the answer-construction setting (Section 1). AMC-AIMO is the AIMO validation AMC set (AI-MO, 2024): 8383 AMC12 problems from 2022–2023, extracted from the AoPS wiki and normalized to integer-answer form. AIME 2024 is the 3030-problem AIME subset of the AIMO validation set (AI-MO, 2024). Appendix B Substitution Gate The substitution gate referenced in Section 3.2 filters candidate positions through two structural checks: 1. Comment-aware filter. Exclude positions inside Lean block comments (/- … -/) and line comments (-- …). 2. Theorem-body filter. Restrict positions to the local block between the theorem/lemma/example keyword and the := by proof marker, excluding imports, helper definitions, and content after the proof. A position survives the gate iff it passes both filters. The gate is deterministic and stateless. We additionally short-circuit the base candidate aba_b in the cascade: since the base statement FbF_b type-checks by construction, we mark aba_b as verified without re-running the substitution, avoiding spurious failures from non-round-tripping edits. A per-candidate fallback further routes individual unsafe candidates (e.g., natural-language labels) to LeanScribe even when R1 would otherwise apply; we ablate this in Section 5.3. Appendix C LeanScribe SFT Details Each LeanScribe training example consists of: • Input. An informal problem x, a Lean statement FbF_b that the autoformalizer produced for some verified base answer aba_b, and the natural-language original answer string. • Output. A JSON object specifying (i) the predicted local block inside FbF_b that encodes the answer, and (i) a Python function fill_answer(answer: str) -> str that, given any informal answer string, returns the Lean expression replacing that block. The local block is required to occur exactly once in FbF_b outside comments and inside the theorem body; otherwise the example is discarded during inference. Lean-filtered expert iteration. The corpus is built in stages, each Lean-filtered. Phase 1 (225225 examples) consists of verified seed rewrites mined directly from NuminaMath formalizations. Phase 2 (699699 examples after strict filtering) is generated by an intermediate LeanScribe checkpoint under rejection sampling: the checkpoint produces several block/function predictions per problem, and we keep only those whose reconstructed statements pass an independent Lean type-check. We additionally mine hard cases—problems where direct localization fails—with earlier checkpoints, again retaining only Lean-passing rewrites (3,2623,262 examples after de-duplication against Phases 1–2). Merging these gives 4,1864,186 examples (3,7683,768 train / 418418 test). The final LeanScribe is a Qwen3-8B model LoRA-fine-tuned on this aggregated corpus, with rank 32, α=64α=64, and dropout 0.050.05 on all attention and MLP projections, for 3 epochs at learning rate 1×10−41\!×\!10^-4 in bfloat16. The R1 disambiguation step (choosing among multiple occurrences of the answer string) uses the same base model without the LoRA adapter, prompted to return the index of the answer slot; only LeanScribe (R2) uses the fine-tuned adapter. Appendix D Drop-in Pipeline Setup The drop-in experiment (Section 5.5) embeds base-and-edit into a Fans-style pipeline (Yao et al., 2025). This setting differs from our main rank-based pipeline in three ways: a single solver, Qwen2.5-Math-7B-Instruct, produces the K=8K=8 candidate answers; an NL–FL consistency judge (QwQ-32B) filters formalizations; and the final selector aggregates surviving candidates by majority vote rather than by generator rank. The full pipeline is proof-level. Candidate answers are converted into formal statements using either independent Kimina formalization or Base. DeepSeek-Prover-V2 then generates proofs for the resulting statements; QwQ-32B checks natural-language–formal consistency; the Lean server verifies the generated proofs; and majority vote is applied over candidates that pass both the proof and consistency filters. Thus, in this section, “verified candidates” refers to candidates whose generated proofs are accepted by Lean and whose formal statements pass the NL–FL consistency judge, not merely statements that type-check before proof search. We hold the answer generator, prover, NL–FL judge, Lean proof verifier, majority-vote selector, and candidate inputs fixed, and swap only the formalization stage. Independent formalization is the Fans default, while Base preserves the K candidate slots and fills them with base-and-edit formal statements. Therefore, the differences in autoformalizer calls and final accuracy in Table 6 are attributable to the formalization strategy. Appendix E Proof-Complete Criterion In the prover-swap ablation (Section 5.4) we report the proof-complete rate—the fraction of statements for which the prover returns a proof that Lean accepts with no remaining sorry placeholder—rather than the raw pass rate. DeepSeek-Prover-V2 sometimes returns proofs that compile but leave a sorry, which would admit a goal without proving it; on MATH-500 its raw pass rate is 15.1%15.1\% but its proof-complete rate is 7.3%7.3\%. Kimina-Prover does not emit such proofs, so the two rates coincide for it. We use proof-complete throughout for a consistent comparison across provers. Appendix F Fall-back Rate On a small fraction of problems no candidate’s autoformalization type-checks in Lean, so neither independent formalization nor Base has a verified statement to select from; for these we fall back to the top-ranked candidate a1a_1 (Section 3.2). Table 9 reports the per-dataset fall-back rate on the Gemini 3 Pro line. Dataset n Fall-backs Rate MATH-500 500 6 1.2% OlympiadBench 566 12 2.1% AIME 2024 30 0 0.0% AMC-AIMO 83 0 0.0% Total 1179 18 1.5% Table 9: Per-dataset fall-back rates (Gemini K=8K=8): the fraction of problems where no candidate formalization type-checks. The rate is identical for the baseline and Base, so it does not affect their comparison. Appendix G Variance Reduction Detail The base-ablation of Section 6 (Table 8) excludes MATH-500: substituting alternative answers into its bases produces statements whose Lean elaboration is prohibitively slow, hitting the type-check timeout on nearly every candidate, so the matched-set comparison there is run on OlympiadBench, AMC-AIMO, and AIME 2024. This exclusion affects only the three-way base-ablation; the main results (Table 1) and the factorization (Table 7) do include MATH-500 and show the same qualitative pattern there—Base raises Acc|GT@KAcc\,|\,GT@K while leaving GT@KGT@K nearly unchanged—so we do not expect the shared-base effect to be specific to the smaller datasets, though we cannot run the matched random-base control on MATH-500 itself. Formalizing once rather than K times reduces the variance among a problem’s K candidate statements. Measuring pairwise character n-gram distance between the K statements of each problem, Base is 6.3×6.3× more consistent than independent formalization, stable across both solvers and all datasets. At the per-problem level, the magnitude of variance reduction predicts the type-check gain (Pearson r=0.22r=0.22, p<10−3p<10^-3, n=2015n=2015), and the gain concentrates on problems the baseline struggles to formalize. Importantly, the variance signal predicts the type-check gain but not the downstream prove-completion gain (|r|<0.05|r|<0.05): variance reduction acts at the formalization stage, raising how many candidates—and how many correct candidates—type-check and reach the prover, rather than changing what the prover can close. Appendix H Qualitative Formulation Examples The examples below are drawn from MATH-500 (Gemini 3 Pro, K=8K=8). Each shows a single problem with its verified base statement FbF_b, and then a second candidate answer aia_i formalized two ways: by Base (editing only the answer block of FbF_b) and by independent formalization (a fresh autoformalizer call). In every case the Base edit type-checks (✓ ) while the independent statement does not (×). The independent call, re-deriving the whole statement from scratch, drifts in ways that break the Lean check—dropping the theorem header, re-encoding the goal, or changing the domain—whereas Base preserves the well-typed structure of the shared base and rewrites only the answer term. (import Mathlib headers are elided for space.) Example 1: tuple answer split across a conjunction. Problem. Find (p,q,r)(p,q,r) such that x3−3x2+4x−1x^3-3x^2+4x-1 divides x9+px6+qx3+rx^9+px^6+qx^3+r. Base answer ab=(6,31,−1)a_b=(6,31,-1); candidate ai=(−6,−31,1)a_i=(-6,-31,1). FbF_b (✓ ): open Polynomial theorem thm p q r : ℝR x(h : (Xˆ3 - 3*Xˆ2 + 4*X - C 1 : ℝR[X]) x∣ (Xˆ9 + C p*Xˆ6 + C q*Xˆ3 + C r)) : xxp = 6 ∧ q = 31 ∧ r = -1 := by sorry Base Fb→iF_b→ i (✓ ): same body, xxp = -6 ∧ q = -31 ∧ r = 1 := by sorry Independent FiF_i (×): theorem (p q r : ℝR) x(h : ∀ (z : ℂC), zˆ3 - 3*zˆ2 + 4*z - 1 = 0 x→ zˆ9 + p*zˆ6 + q*zˆ3 + r = 0) : xxp = -6 ∧ q = -31 ∧ r = 1 := by sorry Base edits the three scalar slots of the verified divisibility statement. The independent call instead re-encodes divisibility as a quantifier over complex roots and omits the theorem name, and does not type-check. Example 2: set-valued answer. Problem. Find all real x with (x−3)3+(x−7)3=(2x−10)3(x-3)^3+(x-7)^3=(2x-10)^3. Base answer ab=3,5,7a_b=\3,5,7\; candidate ai=−3,7a_i=\-3,7\. FbF_b (✓ ): theorem thm : xx ∣ (x-3)ˆ3 + (x-7)ˆ3 = (2*x-10)ˆ3 x= 3, 5, 7 := by sorry Base Fb→iF_b→ i (✓ ): same body, = -3, 7 Independent FiF_i (×): theorem (x : ℝR) : x(x-3)ˆ3 + (x-7)ˆ3 = (2*x-10)ˆ3 x↔ x = -3 ∨ x = 7 := by sorry Base keeps the set-equality form and edits the solution set. The independent call rewrites the same answer as a biconditional over a free variable (and drops the header), changing the proposition’s shape; it does not type-check. Example 3: domain divergence (ℤZ vs. ℝR). Problem. For f:ℝ→ℝf:R with f(x)+f(y)=f(x+y)−xy−1f(x)+f(y)=f(x+y)-xy-1 and f(1)=1f(1)=1, find the integer fixed points. Base answer ab=−2,1a_b=\-2,1\; candidate ai=−1,1a_i=\-1,1\. FbF_b (✓ ): theorem thm f : ℝR → ℝR x(h : ∀ x y, f x + f y = f (x+y) - x*y - 1) x(h’ : f 1 = 1) : xn ∣ ∃ m : ℤZ, n = m ∧ f n = n = -2, 1 x:= by sorry Base Fb→iF_b→ i (✓ ): same body, = -1, 1 Independent FiF_i (×): theorem (f : ℝR → ℝR) (h : …) (h’ : f 1 = 1) : xn : ℤZ ∣ f n = n = -1, 1 := by sorry Base’s base encodes the fixed-point set over ℝR with an integrality constraint. The independent call re-types the set over ℤZ and applies f:ℝ→ℝf:R to an integer index, which is ill-typed; it does not type-check. Summary. Across these cases the same answer is well-typed under Base but not under independent formalization—not because the answer is intrinsically hard to formalize, but because re-formalizing from scratch introduces structural and typing variance that the shared verified base eliminates. This is the per-example face of the variance reduction quantified in Appendix G.