Benchmarking Testing in Automated Theorem Proving

arXiv:2604.23698 · cs.CL, cs.FL · Submitted 2026-04-26 · Read on arXiv

Listen

Radio episode about this paper

Transcript

Introduction to the show: ident: AI Radio. Generated commentary on the latest Artificial Intelligence papers.

Tom: Next we'll be talking about the paper "Benchmarking Testing in Automated Theorem Proving".

Jane: The paper was written by Jongyoon Kim, Hojae Han and Seung-won Hwang from Seoul National University and Electronics and Telecommunications Research Institute.

Tom: Stay tuned as we take you through the paper and discuss its implications.

Title: Tom: Welcome back to the show, everybody. Today we're looking at a paper that just hit arXiv called "Benchmarking Testing in Automated Theorem Proving." Jane, I have to say, the title alone got me curious.

Jane: Same here, Tom. When I first read it, I thought, okay, we already have benchmarks for theorem proving. But the word "testing" is the twist. In software, you don't just check if code compiles — you run tests to see if it actually does what it's supposed to do. This paper says, why don't we do that for math proofs?

Tom: Right. And that's a bigger deal than it sounds. For a long time, we've been checking whether an AI-generated proof compiles in Lean. If it compiles, we call it correct. But this paper points out that compiling just means the logic is internally valid. It doesn't mean the theorem actually says what the problem asked for.

Jane: Exactly. They give a great example. You ask the model to prove that addition is commutative, a plus b equals b plus a. The model instead writes a plus b equals a plus b. That's a tautology. It compiles fine. It's a true statement. But it's completely useless for the original problem.

Tom: And that's where "testing" comes in. In software, you write a function, and then you have other code that calls that function. If your function is wrong, the code that depends on it breaks. The paper applies that same logic to math theorems.

Jane: So instead of just checking the theorem in isolation, they look at all the other theorems in the repository that use this one. If the generated theorem is semantically wrong, those dependent theorems won't compile anymore.

Tom: They call it Testing Accuracy, or TA. And the numbers are pretty striking. The best model they tested, Claude-Sonnet-four point five, gets about eighty percent compilation accuracy. But its testing accuracy drops to under thirty-nine percent.

Jane: That's a huge gap. And it tells us something important — our current evaluation methods are giving us false confidence. We think these models are doing great, but they're actually missing the meaning of the problems.

Tom: I love that they're borrowing from software engineering. Integration testing has been standard practice for decades. Why shouldn't formal math verification work the same way?

Jane: Because it's harder to set up. You need a repository with real dependencies, not just isolated problems. And that's exactly what they built. We'll get into how they did it in a bit, but first — let's just appreciate the shift in thinking.

Tom: Absolutely. This could change how we evaluate every theorem-proving model from here on out.

Jane: And it might explain why some models look great on paper but fail in real mathematical work.

Tom: Stay with us — next we'll talk about the benchmark itself and how they built it.

Summary: Tom: So we're back with "Benchmarking Testing in Automated Theorem Proving." Jane, let's get into the actual benchmark. They call it T2.

Jane: Right. T2 stands for Theorem Testing. And the key thing is, they didn't create new math problems from scratch. They went to real-world Lean four repositories — actual math libraries used by researchers.

Tom: That's a big deal. Most benchmarks use isolated olympiad-style problems. This one uses real research-level math with real dependencies.

Jane: Exactly. They built a dependency graph. Each theorem is a node, and the edges show which theorems use which. Then they pick a target theorem — that's the one the AI has to generate. The theorems that depend on it become the test suite.

Tom: So if the AI generates a wrong version of the target, all those dependent theorems fail to compile. It's like breaking a chain.

Jane: And they made sure each target has at least two successor theorems. On average, there are forty-one successors per problem. That's a lot of tests.

Tom: They also created a harder subset called T2 Hard. Those are problems where the model has to generate both the proposition and the proof — not just fill in a proof for a given statement.

Jane: And the results on that hard set are brutal. The best model gets under five percent testing accuracy. GPT-five-nano compiles at over seventy-five percent but only gets one point five percent on testing.

Tom: That's a fifty-fold gap. It really shows that compilation is not a reliable measure of semantic correctness.

Jane: And they tested eighteen models — closed-source, open-source, and specialized math models. The specialized ones, like DeepSeek-Prover and Goedel-Prover, they actually overfit to compilation.

Tom: Meaning they're really good at producing syntactically valid proofs, but they don't understand the meaning any better than general models.

Jane: Right. The paper says it bluntly — domain-specific fine-tuning improves syntactic fluency without improving semantic correctness.

Tom: That's a hard pill to swallow for the theorem-proving community.

Jane: It is. But it's also a wake-up call. We need to evaluate these models the way we evaluate software — by testing them in context, not just checking if they compile.

Tom: And the fact that they built this benchmark automatically, without human annotation, is huge. It means it can scale.

Jane: They used a strong LLM to generate natural language descriptions of the theorems. They manually verified a sample and found no errors.

Tom: So the whole pipeline is automated. Dependency graph, context extraction, natural language annotation — all of it.

Jane: Which means we can apply this to any Lean repository out there. The method is general.

Tom: And that's the exciting part. This isn't just a one-off benchmark. It's a framework.

Jane: Next, we'll talk about what the paper suggests we do differently — and what that means for the future of AI math.

Improvements: Tom: Welcome back. We're still on "Benchmarking Testing in Automated Theorem Proving." Jane, the paper doesn't just diagnose the problem — it suggests concrete improvements. Let's talk about those.

Jane: The biggest one is using successor theorems as context. When you give the model the theorems that depend on the target, it performs better on testing accuracy.

Tom: That makes sense. If you know what other theorems need to use your result, you can shape your statement to fit.

Jane: But here's the interesting part — providing the natural language proof alone doesn't help much. And providing successor theorems without the NL proof can actually hurt.

Tom: So it's the combination that matters.

Jane: Exactly. The NL proof gives the reasoning context, and the successor theorems give the semantic constraints. Together, they help the model understand what the theorem needs to say.

Tom: They also tried few-shot prompting — giving the model examples of solved problems. And that didn't help either.

Jane: Which tells us the difficulty isn't about understanding the task format. The models know what to do. They just can't do it well enough.

Tom: And iterative refinement with compiler feedback? They tried that too. The gains were minimal.

Jane: Right. Hilbert, which is a method that uses compiler errors to refine proofs, only improved from three point two to five point zero percent on the hard set. Still very low.

Tom: So the paper is saying — no amount of prompt engineering or feedback loops fixes the fundamental gap.

Jane: The fundamental gap is between syntactic validity and semantic correctness. Models can produce proofs that type-check, but they can't reliably produce theorems that mean what the problem asks.

Tom: And that's a deeper problem. It's not about better prompting. It's about better training or better architectures.

Jane: The paper also shows that BLEU score, which measures lexical similarity to a reference proof, is completely unreliable. Even at high BLEU scores, over seventy percent of samples are semantically incorrect.

Tom: So we can't use that as a proxy either.

Jane: No. The only reliable signal is whether the dependent theorems compile.

Tom: Which brings us back to testing. The more successor theorems you have, the stricter the evaluation.

Jane: And they show that. With only two successors, models get around seventy percent testing accuracy. With five or more, it drops to near zero.

Tom: So each additional test catches more semantic errors.

Jane: It's like adding more unit tests to your code. Each one catches a different bug.

Tom: The paper's message is clear — we need to move from checking whether proofs are valid to checking whether they're useful.

Jane: And useful means they work in the context of real mathematics, not just in isolation.

Tom: That's a paradigm shift.

Jane: It is. And it's one that could make AI theorem proving actually trustworthy.

Tom: Let's wrap this up in our final segment.

Conclusion: Tom: And we're back for the final stretch on "Benchmarking Testing in Automated Theorem Proving." Jane, let's pull it all together.

Jane: So the paper gives us two things. First, a new metric called Testing Accuracy that checks semantic correctness by seeing if dependent theorems compile. Second, a benchmark called T2 built from real Lean repositories with over two thousand two hundred problems.

Tom: And the key finding is that compilation accuracy massively overestimates model capability.

Jane: The best model gets eighty percent compilation but under thirty-nine percent testing accuracy. On the hard set, it's even worse — under five percent.

Tom: So what does this mean for the field?

Jane: It means we need to change how we evaluate theorem provers. If we keep using compilation as the gold standard, we'll keep getting models that look great but don't actually understand math.

Tom: And that's not just an academic problem. These models could be used to verify software, check financial systems, even validate safety-critical code.

Jane: Right. If a model can prove a theorem that doesn't say what it's supposed to say, that's a failure with real consequences.

Tom: The paper also shows that specialized math models don't do better on semantic correctness — they just overfit to syntax.

Jane: Which suggests that the next big breakthrough won't come from more training data or better prompting. It'll come from training models to reason about meaning, not just form.

Tom: And the benchmark itself is fully automatic. No human annotation needed. So it can scale to any Lean repository.

Jane: That's the exciting part. This isn't a one-time evaluation. It's a framework that can grow with the field.

Tom: There are limitations, of course. It only works for Lean four and it doesn't apply to standalone theorems with no dependents.

Jane: But for the vast majority of real-world math, where theorems build on each other, this is the right approach.

Tom: So what's the takeaway for our listeners?

Jane: The takeaway is that we need to test AI math the way we test software. Not just check if it compiles, but check if it works in context.

Tom: And that's a standard we should demand.

Jane: Absolutely. This paper gives us the tools to do that.

Tom: Alright, that's a wrap on "Benchmarking Testing in Automated Theorem Proving." Great discussion, Jane.

Jane: Great discussion, Tom. Thanks to everyone listening. We'll be back with the next paper soon.

Tom: Until then, keep questioning your metrics.

Jongyoon Kim, Hojae Han, Seung-won Hwang

Seoul National University · Electronics and Telecommunications Research Institute

cs.CL, cs.FL

Submitted: 2026-04-26

Updated: 2026-08-18

Comments: ACL 2026 Industry

Journal ref: The 64th Annual Meeting of the Association for Computational Linguistics -- Industry Track, 2026

Code: https://github.com/ldilab/T2

Project page: https://leanprover-community.github.io/papers

License: http://creativecommons.org/licenses/by/4.0/

Importance score: 82/100

The gist: The paper introduces T2, a framework and benchmark for evaluating the semantic correctness of formal theorems generated by large language models (LLMs) in automated theorem proving (ATP).

Key concepts

Testing Accuracy (TA)
A new metric proposed by the paper to evaluate AI-generated proofs. Instead of just checking if a proof compiles, TA measures whether the generated theorem maintains semantic correctness when used by other dependent theorems in a repository.
Compilation Accuracy
The traditional method of checking AI math proofs, which only verifies if the code compiles and is internally valid. The hosts explain that while useful, this metric often overestimates a model's ability because it ignores the theorem's actual meaning or intended use.
T2 (Theorem Testing)
The benchmark built by the researchers using real-world Lean repositories. Instead of isolated problems, T2 uses actual mathematical libraries and dependency graphs to test theorems in context, making evaluation rigorous.
Semantic Correctness
The concept that a theorem must actually mean what the problem asks for, even if it is logically valid (a tautology) and compiles correctly. The paper argues this is the critical measure of usefulness.

Terminology

Summary

The paper introduces T2, a framework and benchmark for evaluating the semantic correctness of formal theorems generated by large language models (LLMs) in automated theorem proving (ATP). The authors identify a critical limitation in existing evaluation methods: compilation-based verification only confirms logical validity, not semantic correctness. As stated in the paper, "compilation alone does not guarantee semantic correctness. As illustrated in Figure 1-(a), an NL specification may ask to prove commutativity (a b “ b a), while the generated theorem is a tautology (a b “ a b). As this tautology compiles, which only verifies its logical validity, the intended meaning may be lost."

The proposed approach draws inspiration from integration testing in software engineering. The paper states: "we take inspiration from integrated testing in software engineering, where a component's correctness is verified, not in isolation, but by executing the modules that depend on it. Drawing on the Curry-Howard correspondence (Curry, 1934), where proofs correspond to programs, we observe that a successor theorem that uses a generated lemma is analogous to a module that calls a function. That is, if the lemma is semantically incorrect, the successor theorem cannot be correct."

The core idea is formalized as Testing Accuracy (TA), defined as: TA “ E P „D « k ľ i“1 compilesptsucc piq tfl q ff where a generated theorem is considered correct only if all dependent successor theorems compile successfully when the generated theorem replaces the ground-truth theorem. The paper grounds this in proof theory: "In proof theory, the use of a lemma introduces a cut, and cut elimination removes the auxiliary lemma to produce a direct proof... By the cut elimination theorem, if tfl is semantically correct, this chain of cuts can be eliminated, yielding a valid proof of X Ñ W."

The T2 benchmark is constructed from 5 real-world Lean 4 repositories (adele-ring, Directed-Topology, Untangle, math2001, WhitneyGraustein), comprising 2,206 problems paired with an average of 41 successor theorems per target, automatically extracted without human effort. The authors also construct a T2 Hard subset of 389 problems requiring generation of both a proposition and its proof. The extraction pipeline involves: dependency graph construction using Lean-Dojo, context extraction of predecessor and successor theorems, target selection requiring non-triviality (depth > 1) and successor coverage (Tsucc ≥ 2), and natural language annotation generated by Claude Sonnet 4.5 (manually verified on 10 samples with no errors found).

Experiments evaluate 18 models spanning closed-source (Claude-3.7-Sonnet, Claude-4-Sonnet, Claude-Sonnet-4.5, GPT-4o-mini, GPT-5, GPT-5-mini, GPT-5-nano), open-source (DeepSeek-R1, GPT-OSS-120B, Llama-3.1-8B/70B/405B), and math-specialized models (DeepSeek-Prover-v2-7B, Goedel-Formalizer-v2-8B, Goedel-Prover-v2-32B/8B, Kimina-Autoformalizer-7B, Kimina-Prover-Distill-8B). Key findings include:

  1. High false positive rate of existing metrics: Up to 93.1% of compilable theorems are semantically incorrect, and BLEU fails to distinguish correct from incorrect outputs. The precision of compilation as a predictor of semantic correctness is only 6.89%.

  2. Overfitting to compilation: Specialized proving models overfit to syntax and score lower on semantic correctness than similarly sized general-purpose models. The best model, Claude-Sonnet-4.5, achieves only 38.9% TA on the full set and 4.5% TA on the Hard set, despite 80.3% and 46.0% compilation accuracy respectively.

  3. Dependency structure enables 1k+ test cases: TA becomes more discriminative as successor coverage grows, with the majority of problems verified at depth 7 and an average of 1.6k successor theorems per problem at that depth.

  4. Successor context improves generation: Providing successor theorems as context consistently improves semantic correctness, while NL proofs alone do not. The ablation shows that both NL proofs and successor theorems must be provided together for consistent improvements.

Additional experiments show that few-shot prompting does not improve TA on T2 Hard (e.g., Claude-4-Sonnet drops from 4.5% to 4.3%), and iterative refinement with compiler feedback (Hilbert) yields only marginal gains (5.0% vs 3.2% baseline). The paper concludes: These findings demonstrate that testing-based evaluation is essential for trustworthy assessment of formal theorem generation.

Limitations acknowledged include: TA reliability depends on successor coverage, inapplicability to standalone theorems (approximately 1.4% of theorems in collected repositories), implementation exclusively for Lean 4, and potential noise from LLM-generated natural language annotations.

Improvements for AI systems

Based on the paper, here are the specific improvements I can implement and the resulting capabilities of the improved AI system:

  1. Implement Testing Accuracy (TA) as a core evaluation metric

  • Replace compilation-only checks with a dependency-aware test suite that recompiles all successor theorems after substituting the generated theorem.

  • Automatically extract dependency graphs from Lean 4 repositories (using Lean-Dojo) to identify predecessors and successors for each target theorem.

  • Compute TA as the probability that all successor theorems compile successfully, providing a direct semantic correctness signal without human annotation or reference proofs.

  1. Add successor theorem context to generation prompts

  • Modify the autoformalization prompt to include the successor theorems (Code After) as explicit context, not just the target theorem and predecessors.

  • This consistently improves TA across models (e.g., Claude-Sonnet-4.5 improves from 34.0% to 38.9% on the full set when successor theorems are provided alongside NL proofs).

  1. Integrate iterative refinement with compiler feedback (Hilbert-style)

  • Use the Lean compiler's error messages from successor theorem compilation failures as feedback to iteratively refine the generated theorem.

  • This raises TA on the Hard subset from 3.2% to 5.0% for DeepSeek-Prover-v2-7B, demonstrating that testing-based feedback is more effective than compilation-only feedback.

  1. Implement a graded TA variant for partial credit

  • Instead of binary pass/fail, compute the fraction of successor theorems that compile successfully.

  • This provides a more nuanced signal for model development, especially for problems with many successors (e.g., 41 on average in T2), where partial success is informative.

  1. Add a Hard subset filter for benchmark construction

  • Automatically identify target theorems whose declarations have a body of type Prop, requiring generation of both the proposition and its proof.

  • This subset (389 problems in T2) exposes the largest gap between compilation and TA (up to 50×), making it a more discriminative evaluation set.

  1. Detect semantically incorrect but compilable theorems

  • The system will reject tautologies like a + b = a + b when the NL specification asks for commutativity a + b = b + a, because successor theorems that depend on the correct statement will fail to compile.

  • This catches errors that compilation alone misses, reducing false positives by up to 93.1%.

  1. Evaluate theorem generation without human annotation

  • The system automatically extracts test suites from real-world Lean repositories, eliminating the need for manual inspection or ground-truth reference proofs.

  • This enables scalable evaluation of any new model or prompting strategy.

  1. Provide actionable feedback for model improvement

  • The system reports which successor theorems fail and why, allowing developers to identify specific semantic gaps (e.g., missing hypotheses, incorrect variable bindings, or wrong logical structure).

  • This is more informative than a single compilation pass/fail signal.

  1. Rank models by semantic correctness rather than syntactic fluency
  • The system will expose that specialized provers (e.g., Goedel-Prover-v2-32B) overfit to syntax and score lower on TA than general-purpose models of similar size (e.g., Llama-3.1-70B), guiding architecture and training data decisions.
  1. Support iterative development loops
  • The system can be used in a feedback loop where generated theorems are tested, failures are analyzed, and the model is retrained or prompted with targeted examples, leading to measurable TA improvements over successive iterations.
  1. Extend to other proof assistants
  • The dependency-graph extraction and testing methodology is language-agnostic, so the improved system can be adapted to Coq (using coq-dpdgraph) and Isabelle (using the Archive of Formal Proofs) with minimal changes.

Abstract

Recent advances in large language models (LLMs) have shown promise in formal theorem proving, yet evaluating semantic correctness remains challenging. Existing evaluations rely on indirect proxies such as lexical overlap with human-annotated proof, or expensive manual inspection. Inspired by the shift from lexical comparison to test-based evaluation in code generation, we propose T, a framework that evaluates the semantic correctness of formal theorems: a generated theorem is considered correct only if all dependent successor theorems compile successfully, analogous to integration testing. We construct a benchmark from 5 real-world Lean 4 repositories, comprising 2,206 problems paired with 41 successor theorems on average, automatically extracted without human effort. Experiments demonstrate that while state-of-the-art models achieve high compilation success, they perform significantly worse under our semantic metric. The best model, Claude-Sonnet-4.5, achieves only 38.9% Testing Accuracy on the full set, given both natural language proof and successor theorems as context, revealing a critical gap in current theorem generation capabilities.

Sources

Related papers