TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?

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

purpose

TaoBench tests whether Lean theorem-proving models transfer from MathLib definitions to an equivalent but bespoke definitional framework. It contains 150 undergraduate Analysis I exercises from Terence Tao’s Lean formalization, paired with MathLib translations. The benchmark isolates definition familiarity from mathematical difficulty by keeping the problem pairs mathematically equivalent. The authors write: “We introduce TAO B ENCH, the first benchmark designed to measure ATP robustness beyond MathLib by targeting generalization to a novel definitional framework.” (Section 1, p.2; the paper’s small-caps name renders as “TAO B ENCH” in the text extraction)

technique 1: self-contained extraction of local formal environments

What it is: construct a minimal compilable context for every textbook exercise instead of importing an entire chapter. A problem is packaged with definitions, notation, lemmas, and references needed to state it and compile it in isolation.

How to apply: (1) start with the textbook exercise and its source file; (2) use JiXia static analysis to recursively retrieve references to constants, theorems, and structure declarations; (3) give the retrieved references and source file to an agent so it can recover local syntactic sugar and notation; (4) compile the generated context in a clean Lean environment; (5) return compiler stack traces; (6) iterate retrieval and correction until the context compiles. The paper says, “We approach this by retrieving only the definitions strictly required to faithfully compile each exercise.” (Section 2.1, p.3) JiXia alone misses sugared syntax (for example postfix notation), so the authors add a file-lookup tool that returns source files for JiXia-identified references (Section 2.1, p.3-4). The orchestrating agent is GPT-5 (Figure 2, p.2). The extraction prompt (Appendix A.5.1-A.5.2, pp.17-21) requires declarations to be copied verbatim from the textbook source and forbids placeholder definitions (such as redefining Real as Q); it lets the agent replace only the proof of a lemma or theorem with by sorry when copying its dependencies would balloon the snippet; and it requires the target theorem to end with by sorry.

Verus form (inference): build a per-task Rust module containing only the structs, traits, spec functions, and lemmas referenced by the target proof. Use compiler/verifier diagnostics to request missing declarations, and re-run cargo verus after each repair. Keep the extracted context immutable once evaluation begins so proof success measures reasoning rather than accidental imports. The paper’s Lean tools and namespaces do not transfer directly.

Evidence and limits: context matters. Without retrieved context, Pass@128 for DeepSeek-Prover-V2-7B falls from 62/150 (41.33%) to 44/150 (29.33%); Goedel-Prover-V2-32B falls from 74/150 (49.33%) to 46/150 (30.00%) (Table 2, p.5). The authors motivate minimal context this way: “providing too little context may result in missing useful information, while providing too much context introduces substantial noise.” (Section 2.1, p.3) Their footnote 2 says: “We leave defining, identifying, and retrieving all useful contextual information to future work.” (p.3) Footnote 1 says models “often have to reference material outside the context for successful proofs.” (p.3)

technique 2: paired definitional translation with compilation and equivalence checks

What it is: create TAO B ENCH MATH LIB by rewriting every Tao-style statement to standard MathLib definitions, then check both syntax and mathematical equivalence. The pipeline has rewriting, Lean compilation with iterative error repair, JiXia target-state extraction, an LLM equivalence judgment, and expert verification (Figure 3; Sections 2.2 and 2.2.1, pp.4–5, 11).

How to apply: (1) forbid new local definitions and notation and require a fixed MathLib header; (2) prompt GPT-5.1 with web search to choose canonical MathLib definitions; (3) compile the translation; (4) use compiler errors to repair syntax and types until it compiles; (5) extract the Tao and MathLib target proof states with JiXia; (6) ask an evaluator to judge equivalence from statements and target states; (7) discard failed candidates and regenerate; (8) have trained human judges label the final pair A (fully equivalent), B (nearly equivalent), C (minor differences), or D (major differences), correcting C/D cases. The paper warns, “Compilation alone, however, does not guarantee semantic faithfulness.” (Section 2.2, p.5)

Evidence: 150 paired problems were selected. Human annotation assigned 108 label A and 31 label B; 11 MathLib data points required correction, which the judges revised manually; three judges achieved Gwet’s AC2 of 0.89 (Appendix A.1, p.11). Each of three judges rated 70 pairs, with 30 of each judge’s 70 rated by all three (Appendix A.1, p.11). Note that the main text gives a different count: “Human annotators identified 33 often subtle issues with the MathLib translations and provided corrected versions of the problems.” (Section 2.2.1, p.5) The paper does not reconcile 33 with 11. Appendix A.1 also describes an extra GPT-5-Pro grading pass, with one annotator reviewing its grades and proposing corrections for the final version (p.11). Across translation attempts, 30/150 points encountered at least one error iteration, with 154 equivalence-check failures versus 79 compilation errors (Appendix A.4.2, p.13). The authors conclude: “This suggests that ensuring mathematical equivalence is much harder than ensuring compilability during translation.” (Appendix A.4.2, p.13) Early direct GPT-5.1 translation without web search gave roughly 60% syntactically valid outputs, and about 90% compiled with web search enabled (Section 2.2, p.4).

Verus form (inference): translate a bespoke Rust specification into a canonical Verus library version under a fixed import/header policy, then verify both with cargo verus. Compare postconditions and proof-state obligations, and require a human or independently checked equivalence relation for paired tasks. An LLM judgment alone is not evidence of Verus semantic equivalence.

technique 3: paired pass-rate evaluation under definitional shift

Run the same prover and sampling budget on both paired versions. The main measure is Pass@128 over 150 problems (Pass@8 for the three frontier general-purpose models); the paper uses default decoding, temperature 1.0, and up to 8192 reasoning tokens (Section 3.1, p.5). TaoBench problems carry their local environment in the prompt, while TaoBenchMathLib problems use the standard import Mathlib environment (Section 4.1, p.6). Public ATP results are sharply lower on TaoBench: DeepSeek-Prover-V2-7B 62/150 (41.33%) versus 104/150 (69.33%) on MathLib; Goedel-Prover-V2-32B 74/150 (49.33%) versus 109/150 (72.67%) (Table 1, p.4). GPT-5.1 is 78/150 (52.00%) versus 97/150 (64.67%) at Pass@8 (Table 3, p.6).

Context-length analysis groups problems by local-definition count. Averaged across the evaluated models, TaoBench Pass@128 falls from 67.14% at zero definitions to 6.37% at 10 or more; MathLib falls from 68.10% to 53.43% (Section 4.1, p.6; Table 4 has 35, 40, 41, and 34 problems in the four buckets). A case study gives Goedel-32B 0/128 verified proofs on bespoke Nat.backwards_induction versus 64/128 on its MathLib pair (Section 4.4, p.7). The reverse pattern also occurs: DeepSeek-Prover-V2-7B has 2/128 verified proofs on the Tao Convergesto.squeeze and 0/128 on its MathLib pair (Section 4.4, p.8). These are verified-proof counts out of 128 samples. The paper also reports that removing the context from TaoBench prompts gives only a modest drop (Table 2), and attributes the without-context successes to problems with no extra statements or only MathLib-like ones (Section 4.2, p.7).

Verus form (inference): use matched Verus specifications and report Pass@k with exact denominators, model, verifier version, and tactic/token budget. Stratify by number of local definitions and by whether a lemma is canonical or bespoke. This tests whether an agent has learned Verus reasoning or only memorized library idioms.

what remains trusted and product threat

The benchmark trusts Lean compilation, JiXia extraction, evaluator judgments, expert labels, and the correctness of Tao and MathLib formalizations. It does not prove that an ATP found the best proof, nor that a compiled translation preserves all intended mathematics beyond the stated checks. The authors conclude that “strong performance on Mathlib-formulated problems does not reliably transfer to definitionally equivalent formalizations outside the MathLib framework.” (Section 6, p.8)

Inference: this is a high threat to agent-written verified Rust when VL tasks introduce new structs, traits, and spec functions. A proof can be valid yet fail because the agent cannot connect familiar lemmas to local definitions. VL should adopt the paired-definitional evaluation and local-context extraction ideas, but it should not redo Lean’s benchmark; it needs Verus-specific equivalence checks and end-to-end proof-success measurements.

techniques for the catalog

• minimal formal context extraction — recursively retrieve only declarations needed to compile each target and repair with compiler diagnostics
• paired definitional translation — rewrite bespoke statements into a canonical library and check compilation plus semantic equivalence
• expert equivalence labels — classify pairs as fully, nearly, minor-difference, or major-difference and correct non-equivalent translations
• definitional-shift evaluation — compare Pass@k on mathematically equivalent bespoke and canonical specifications
• context-length stress test — stratify proof success by the number of locally introduced definitions Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “In the Lean formalization of Analysis I, Tao generally favors faithful translation over more idiomatic Lean formulations when the two diverge”): I read the whole paper text (main body, appendix and prompts) and checked every quotation, number, section and page reference, and the technique steps against it. I changed the Section 1 quotation (it had dropped the words “the first”), the Section 6 quotation (the paper spells it Mathlib-formulated), the section reference of the two Section 2.1 quotations (cited as Section 2), added the paper’s other count of annotator-found translation issues (33 in Section 2.2.1 versus 11 in Appendix A.1), the extraction-prompt rules (verbatim copying, proof-only by sorry), the GPT-5 agent, the reverse case study, and the paper’s own wording for the equivalence-versus-compilation comparison. I did not check the figures visually (Figures 4, 7, 8), the cited prior work, or any external link; the arXiv link matches the id 2603.12744 printed in the paper text. The Verus-form paragraphs and the VL threat assessment are my own inference, not from the paper.

Last edited: 2026-10-17