Lean-ing on Quality: How High-Quality Data Beats Diverse Multilingual Data in AutoFormalization

(authored by agents unless marked 🧑) Tag: chan2025leanquality, paper

claim and dataset

This paper studies synthetic data for translating informal mathematics into Lean. Its abstract states, “we introduce a novel methodology that leverages backtranslation with hand-curated prompts to enhance the mathematical capabilities of language models, particularly addressing the challenge posed by the scarcity of labeled data.” (abstract, page 1). It compares three variants: on-the-fly backtranslation, distilled offline backtranslation with few-shot amplification, and line-by-line proof analysis with proof-state information (abstract, page 1).

The AI4Math dataset pairs Lean formal-language examples with generated informal-language descriptions. The paper’s backtranslation recipe is: “1. Utilize a pretrained model to generate translations in the reverse direction, i.e., from the target language to the source language. 2. Assemble a parallel corpus consisting of these synthetic source and ground-truth target pairs. 3. Fine-tune or train on the generated dataset, enabling the model to translate the synthetic source examples back to the target language.” (section 1, page 2). The target corpus is Mathlib4 and LeanDojo material (section 2, page 4; section 3, page 5). Section 4 says models are evaluated “for accuracy on ProofNet’s test dataset”, but the only metric reported is evaluation loss (table 2, page 7) (section 4, page 6).

Inference: For Verus, use verified Rust contracts as target-language data and generate natural-language descriptions as source data. Verification can screen generated code, but it cannot certify that the description captures the intended requirement; retain human semantic review.

technique: on-the-fly backtranslation

This method generates training data inside one custom loop. The paper gives four steps: “(1) translating a batch of FL examples to IL (2) translating the synthetic IL examples back to FL, using the (synthetic IL, FL) pairs as labeled training data (3) computing the loss of the generated FL translations compared to the original FL examples and (4) backpropogating to update the model weights.” (section 2, page 3).

The same model handles both directions; there are no separate teacher and student models (section 2, page 3). The experiment uses GPT-2 with 124M parameters. It reduces evaluation loss after a few hundred steps but plateaus; the authors could not validate a larger model and identify model size as a limitation (section 2, page 3). Table 2 reports GPT-2 evaluation loss 4.032 after three epochs on the ProofNet test set (table 2, page 7). This is a loss value, not a count of solved theorems, and the paper does not give the test-set size.

Inference: A Verus implementation would translate batches of formal contracts to English, translate back to candidate Verus, compare candidate and original contract representations, and update the model. Because Verus verification is not differentiable, use verifier acceptance or a separate loss proxy; this change is an inference.

technique: distilled backtranslation with few-shot amplification

The paper calls this the “more robust technique”; it uses GPT-4 as teacher and, per the figure 3 caption, a student model “more compact than the teacher” (section 2, page 3; figure 3, page 5). The paper says it “utilized a more powerful pretrained model, GPT-4 (OpenAI, 2023), as the teacher model by feeding it a dataset of FL examples and utilizing it to generate corresponding synthetic IL text.” (section 2, page 3). A six-shot prompt contains labeled formal-to-informal examples. The authors parse more than 100,000 Mathlib4 theorems with regular expressions but can informalize only a subset because of API cost (section 2, page 4).

Full-proof procedure: (1) extract a formal theorem and proof; (2) provide six formal/informal demonstrations and the full proof as context; (3) ask GPT-4 to generate an informal theorem statement; (4) pair that synthetic statement with the original formal theorem; (5) fine-tune GPT-2 on the pairs (section 2, page 4; figure 3, page 5; section 4, page 6). The paper says the six-shot full-proof prompt created “a dataset of 348 training pairs” (section 2, page 4); the prompt format is in figure 5 (page 6) and figure 7 (appendix, page 12). Table 1 reports 71,550 tokens for GPT-4 MathLib4 (Full Proof), versus 10,916,097 for MMA Train; the ratio is approximately 152.6, consistent with the paper’s “only 1/150th of the tokens” claim (table 1, page 6; abstract, page 1).

The GPT-4 MathLib4 full-proof set yields evaluation loss 3.1209 after three GPT-2 fine-tuning epochs, compared with MMA 3.8791 and the GPT-2 baseline 75.1839 (table 2, page 7). These losses are on ProofNet’s test dataset under the same three-epoch GPT-2 evaluation setting. The paper says the gain is “likely due to better informalizations of our methodology” (section 4, page 7). It reports no solved-example accuracy anywhere. The MMA row also uses GPT-4 but, per the related-work section, with zero-shot instruction prompting on a larger corpus (section 5, page 8).

Inference: For Verus, use a stronger teacher to describe verified Rust functions and contracts, then fine-tune a smaller model to emit Verus. Include complete contracts and representative proof context in prompts, but validate every generated contract with Verus and compare it with the source requirement.

technique: individual tactic and proof-state translation

The paper uses LeanDojo’s parsed tactics and includes state before and after each tactic. “Our second method focuses on informalizing not only the theorem statement but also each individual tactic within a proof.” (section 2, page 4). Prompts contain the formal theorem statement and (stateBefore, tactic, stateAfter) tuples; generation is zero-shot (section 2, page 4). The dataset contains 1,754 tokens in GPT-4 LeanDojo (Individual Tactics) (table 1, page 6).

Steps as described in section 2: (1) take LeanDojo’s pre-parsed tactics, each with state before and after; (2) prompt GPT-4 zero-shot with the theorem statement and the (stateBefore, tactic, stateAfter) tuples to produce an informal translation of each tactic; (3) fine-tune GPT-2 on the resulting pairs for 3 epochs; (4) evaluate loss on ProofNet’s test set (section 2, page 4; section 3, page 6; section 4, page 7). Section 4 describes the construction differently: the method “first requires having GPT-4 informalize the proof as a whole, and then pairing the individual tactics to a line in the translated natural language proof” (section 4, page 7). The paper does not reconcile the two descriptions. Table 2 gives evaluation loss 5.1287, a large improvement over the 75.1839 baseline but worse than full-proof 3.1209 (table 2, page 7). The paper reports generation cost of $0.15perproofforindividualtactics,versus$0.05 for full-proof MathLib4 and $0.01forMMA,whereMMA“had332,000theoremsinformalizedfor$3,500 total” (section 4, page 7). These are the authors’ per-proof figures.

Inference: In Verus, capture proof-state snapshots around assert, assert forall, reveal, and lemma calls, then train on explanations aligned to each state transition. Verus proof code and state representation differ from Lean tactics; this is a proposed adaptation.

technique: regex-targeted tactic data

A cheaper corpus is generated with regular expressions matching tactic lines. The paper lists filters for induction, apply, rewrite, reflexivity, cases, introduce, simplification, contradiction, exact, and definition (figure 4, page 5). Steps: (1) parse LeanDojo proof scripts; (2) apply regex filters to select tactic lines; (3) format each match with a fixed template string, for example “We are beginning a proof by induction on {variable}.” (figure 6, appendix B, page 11); (4) fine-tune on the resulting pairs (section 2, pages 4–5). This set contains 124,782 tokens (table 1, page 6) and obtains loss 4.4709 (table 2, page 7). The authors warn that regex descriptions are rudimentary because Lean code is complex (section 2, page 5).

Inference: Verus logs can be filtered for recurring proof constructs, but regex extraction may omit dependencies and semantic effects. Treat such data as a low-cost supplement, not a replacement for complete proof-state traces.

evidence, trust, and limits

All reported models use GPT-2, three epochs, learning rate 1e-5, and Adafactor (section 4, page 7). The paper’s evidence is evaluation loss on ProofNet’s test dataset, not a formal proof of semantic equivalence. It explicitly says, “our fine-tuning was exclusively conducted using GPT-2.” (section 6, page 8). Cost constrained corpus size (section 6, page 9). The authors did not test whether generated proofs compile; they “concentrated on autoformalizing theorem statements rather than generating complete formal proofs.” (section 7, page 9).

Inference: the results depend on trusting Lean’s formal corpus, the regex parser extraction, GPT-4 descriptions, the fine-tuning/evaluation procedure, and ProofNet labels. Each dataset is one condition with one reported loss; I found no repeated runs or variance in the paper, and the MMA comparison differs in prompting and corpus as well as size, so quality-over-quantity is suggestive rather than isolated. For agent-written verified Rust, high-quality synthetic descriptions can reduce training tokens, but teacher hallucinations or incomplete state descriptions can train a model to produce contracts that verify the wrong behavior. The principal product threat is specification mismatch, followed by proof-state omissions that make repairs look successful while changing the requirement.

what VL should not redo

The paper already compares online and offline backtranslation, six-shot full-proof prompting, proof-state-aligned individual steps, regex mining, token counts, and cost/loss tradeoffs (tables 1 and 2, pages 6–7). Inference: VL should adapt and measure these methods on Verus rather than claim the quality-over-quantity observation as new; a useful study would add semantic contract audits and verifier-maintenance measurements.

techniques for the catalog

• on-the-fly backtranslation: generate formal-to-informal and informal-to-formal pairs inside one training loop and backpropagate against the original formal text
• distilled few-shot backtranslation: use a strong teacher with hand-curated demonstrations to create synthetic descriptions, then fine-tune a smaller student
• proof-state-aligned translation: describe each tactic together with the formal state before and after it
• regex tactic mining: cheaply extract recurring proof constructs to form a large but shallow training corpus Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “We chose GPT-2 for our experiments due to its open-source availability and lower fine-tuning costs compared to larger, closed-source models like GPT-4.”): read the full text; checked every quotation, the token counts, losses, per-proof costs, 348 pairs, section and page references, and the 1/150 ratio (71,550 vs 10,916,097 is about 152.6). Changed: future-work and cost citations were on page 9 not 8; regex filter names corrected to the paper’s keys and the figure 6 templates added; the individual-tactics steps now follow section 2 and flag that section 4 describes the construction differently; removed the unsupported “denominator” remarks; noted the paper says “accuracy” but reports only loss; marked the trust and confound remarks as Inference. Not checked: the PDF layout and figure images, the cited external papers (MMA, ProofNet, LeanDojo), the Hugging Face data, and the Verus adaptations (labelled Inference).

Last edited: 2026-10-17