BROWSE
Detail
Conference Paper
Benchmarking Testing in Automated Theorem Proving
- Authors
- Jongyoon Kim, Hojae Han, Seung-Won Hwang
- Issue Date
- 2026-07
- Citation
- Annual Meeting of the Association for Computational Linguistics (ACL) 2026, pp.2241-2260
- Publisher
- Association for Computational Linguistics
- Language
- English
- Type
- Conference Paper
- 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 T2, 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.
- KSP Keywords
- BEST Model, Critical gap, Language Models, Natural language, Real-world, Testing accuracy, automated theorem proving, code generation, human effort, integration testing, lexical overlap
This work is distributed under the term of Creative Commons License (CCL)
(CC BY)
(CC BY)
