TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?

• URL: http://arxiv.org/abs/2603.12744v1
• Date: Fri, 13 Mar 2026 07:39:47 GMT
• Title: TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?
• Abstract summary: We evaluate the robustness of current ATP systems when applied to a novel definitional framework.<n>We introduce TaoBench, an undergraduate-level benchmark derived from Terence Tao's Analysis I.<n>For fair evaluation, we build an agentic pipeline that automatically extracts a compilable, self-contained local environment for each problem.
• Score: 104.38098884163541
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Automated theorem proving (ATP) benchmarks largely consist of problems formalized in MathLib, so current ATP training and evaluation are heavily biased toward MathLib's definitional framework. However, frontier mathematics is often exploratory and prototype-heavy, relying on bespoke constructions that deviate from standard libraries. In this work, we evaluate the robustness of current ATP systems when applied to a novel definitional framework, specifically examining the performance gap between standard library problems and bespoke mathematical constructions. We introduce TaoBench, an undergraduate-level benchmark derived from Terence Tao's Analysis I, which formalizes analysis by constructing core mathematical concepts from scratch, without relying on standard Mathlib definitions, as well as by mixing from-scratch and MathLib constructions. For fair evaluation, we build an agentic pipeline that automatically extracts a compilable, self-contained local environment for each problem. To isolate the effect of definitional frameworks, we additionally translate every problem into a mathematically equivalent Mathlib formulation, yielding paired TaoBench-Mathlib statements for direct comparison. While state-of-the-art ATP models perform capably within the MathLib framework, performance drops by an average of roughly 26% on the definitionally equivalent Tao formulation. This indicates that the main bottleneck is limited generalization across definitional frameworks rather than task difficulty. TaoBench thus highlights a gap between benchmark performance and applicability, and provides a concrete foundation for developing and testing provers better aligned with research mathematics.

Related papers

• MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement [28.062085562858098]
  We introduce MathForm, an autoformalization framework for constructing verified training data.<n>We construct FormalVerse, a Lean 4 dataset containing approximately 367K verified examples.<n>MathForm-8B achieves average Pass@8 rates of 88.06% under Syntax Check and 72.37% under Consistency Check.
  arXiv  Detail & Related papers  (2026-08-14T11:51:12Z)
• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  Large Language Models (LLMs) exhibit strong informal mathematical reasoning but struggle to generate verifiable proofs in formal languages like Lean.<n>We present LEAP, an agentic framework that enables general-purpose foundation models to achieve state-of-the-art performance on automated formal theorem proving.
  arXiv  Detail & Related papers  (2026-06-02T08:16:42Z)
• CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean [10.684401671916158]
  We introduce CAM-Bench, a Lean 4 theorem-proving benchmark of 1,000 Lean proof targets in computational and applied mathematics.<n>These problems are adapted from textbook exercises and often depend on locally introduced definitions, notation, algorithms, and elementary results.<n>We validate the resulting formal problems through Lean compilation and semantic review, checking both formal correctness and semantic alignment with the original exercises.
  arXiv  Detail & Related papers  (2026-05-17T04:53:47Z)
• LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
  We present LiveMathematicianBench, a dynamic multiple-choice benchmark for research-level mathematical reasoning.<n>By grounding evaluation in newly published theorems, it provides a realistic testbed beyond memorized patterns.<n>It employs a proof-sketchguided distractor pipeline that uses high-level proof strategies to construct plausible but invalid answer choices.
  arXiv  Detail & Related papers  (2026-04-02T08:22:17Z)
• MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics [51.65118519899584]
  We introduce MathlibLemma, the first LLM-based multi-agent system to automate the discovery and formalization of mathematical folklore lemmas.<n>We further construct the MathlibLemma benchmark, a suite of 4,028 type-checked Lean statements spanning a broad range of mathematical domains.
  arXiv  Detail & Related papers  (2026-01-30T15:24:42Z)
• LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories) [7.871706113805829]
  LeanCat is a Lean benchmark for category-theoretic formalization.<n>Part I: 1-Categories contains 100 fully formalized statement-level tasks.<n>Part II: LeanBridge uses LeanExplore to search Mathlib and observe consistent gains over single-model baselines.
  arXiv  Detail & Related papers  (2025-12-31T11:33:29Z)
• DAG-Math: Graph-Guided Mathematical Reasoning in LLMs [54.231935013127206]
  Large Language Models (LLMs) demonstrate strong performance on mathematical problems when prompted with Chain-of-Thought (CoT)<n>We propose modeling CoT as a certain rule-based process over directed acyclic graphs (DAGs)<n>We introduce logical closeness, a metric that quantifies how well a model's CoT trajectory adheres to the DAG structure.
  arXiv  Detail & Related papers  (2025-10-19T21:05:17Z)
• DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems [14.568293842955065]
  DRIFT is a framework that decomposes informal mathematical statements into smaller, more tractable ''sub-components''<n>It retrieves illustrative theorems to help models use premises more effectively in formalization tasks.<n>We evaluate DRIFT across diverse benchmarks (ProofNet, ConNF, and MiniF2F-test) and find that it consistently improves premise retrieval.
  arXiv  Detail & Related papers  (2025-10-12T21:42:04Z)
• Computational Reasoning of Large Language Models [51.629694188014064]
  We introduce textbfTuring Machine Bench, a benchmark to assess the ability of Large Language Models (LLMs) to execute reasoning processes.<n> TMBench incorporates four key features: self-contained and knowledge-agnostic reasoning, a minimalistic multi-step structure, controllable difficulty, and a theoretical foundation based on Turing machine.
  arXiv  Detail & Related papers  (2025-04-29T13:52:47Z)
• Challenging the Boundaries of Reasoning: An Olympiad-Level Math Benchmark for Large Language Models [86.45058529521258]
  OlymMATH is a novel Olympiad-level mathematical benchmark designed to rigorously test the complex reasoning capabilities of LLMs.<n>OlymMATH features 200 meticulously curated problems, each manually verified and available in parallel English and Chinese versions.
  arXiv  Detail & Related papers  (2025-03-27T11:20:17Z)
• StructTest: Benchmarking LLMs' Reasoning through Compositional Structured Outputs [78.84060166851805]
  StructTest is a novel benchmark that evaluates large language models (LLMs) on their ability to follow compositional instructions and generate structured outputs.<n> Assessments are conducted deterministically using a rule-based evaluator, which can be easily extended to new tasks and datasets.<n>We demonstrate that StructTest remains challenging even for top-performing models like Deepseek-V3/R1 and GPT-4o.
  arXiv  Detail & Related papers  (2024-12-23T22:08:40Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.