| Challenge: | Existing evaluations rely on indirect proxies such as lexical overlap with human-annotated proof, or expensive manual inspection. |
| Approach: | They propose a framework that evaluates the semantic correctness of formal theorems . they use a set of problems paired with 41 successor theorels to compare them . |
| Outcome: | The proposed framework evaluates the semantic correctness of formal theorems using real-world Lean 4 repositories. |
Similar Papers
ATG: Benchmarking Automated Theorem Generation for Generative Language Models (2024.findings-naacl)
Copied to clipboard
| Challenge: | Existing generative language models (LMs) can generate new or reusable theorems, but their ability to generate new theorels is under-explored. |
| Approach: | They propose to use Metamath library to generate new theorems that can be saved as reusable knowledge for future theoretical proving. |
| Outcome: | The proposed benchmark evaluates whether an agent can generate valuable (and possibly brand new) theorems that are applicable for downstream theoretic proving as reusable knowledge. |
Theorem Prover as a Judge for Synthetic Data Generation (2025.acl-long)
Copied to clipboard
| Challenge: | Recent studies show that large language models are increasingly capable of tackling mathematical problems. |
| Approach: | They propose an approach that iteratively refines theorem prover formalisation to mitigate errors. |
| Outcome: | The proposed method increases execution rate on the Lean prover from 60% to 87%, while human annotation is replaced with theorem prover feedback. |
RLMEval: Evaluating Research-Level Neural Theorem Proving (2025.findings-emnlp)
Copied to clipboard
| Challenge: | RLMEval evaluates large language models for research-level neural theorem proving and proof autoformalization . the best model achieves only a 10.3% pass rate on existing benchmarks . |
| Approach: | They propose a new evaluation suite for large language models . it evaluates research-level theorems from real-world Lean formalization projects . |
| Outcome: | RLMEval evaluates research-level theorems from real-world Lean formalization projects. |
LLM-Powered Benchmark Factory: Reliable, Generic, and Efficient (2026.acl-long)
Copied to clipboard
Peiwen Yuan, Shaoxiong Feng, Yiwei Li, Xinglin Wang, Yueqi Zhang, Jiayi Shi, Chuyi Tan, Boyuan Pan, Yao Hu, Kan Li
| Challenge: | Using generic and efficient benchmark generators, human annotators are limited by inefficiency . current benchmark generator methods rely on seed signals, leading to long cycles and high costs . |
| Approach: | They propose a framework to evaluate LLMs as generic benchmark generators and integrate them as BenchMaker. |
| Outcome: | The proposed framework achieves comparable performance to human-annotated benchmarks on most metrics. |
Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference (2025.acl-long)
Copied to clipboard
| Challenge: | Large Language Models (LLMs) are increasingly being used to automate programming tasks. |
| Approach: | They propose a benchmark to evaluate LLMs' reasoning abilities on program semantics. |
| Outcome: | The proposed benchmark shows that LLMs perform well with simple control flows but struggle with more complex structures, especially loops, even with advanced prompting. |
Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations (2025.acl-long)
Copied to clipboard
| Challenge: | Recent work has shown that the interaction of large language models (LLMs) with theorem provers (TPs) can help verify and improve the validity of NLI explanations. |
| Approach: | They propose to use logical expressions to guide LLMs in generating structured proof sketches and to use them to improve their accuracy. |
| Outcome: | The proposed strategies improve autoformalisation, syntactic errors and explanation refinement over the state-of-the-art model. |
Selene: Pioneering Automated Proof in Software Verification (2024.acl-long)
Copied to clipboard
| Challenge: | Currently, software verification is resource-intensive and manpower-consuming. |
| Approach: | They propose a project-level automated proof benchmark based on the seL4 operating system . they propose augmentations to enhance the flexibility of the framework and lightweight verification environment . |
| Outcome: | The proposed framework provides a comprehensive framework for end-to-end proof generation and a lightweight verification environment. |
TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts (2024.emnlp-main)
Copied to clipboard
| Challenge: | a framework for formal proof writing using formal languages like Lean4 is needed to prove mathematical theorems using formal language. |
| Approach: | They propose a framework that trains a general-purpose LLM to be a Lean4 expert. |
| Outcome: | The proposed framework achieves cumulative accuracies of 36.48% and 33.61% on MiniF2F-Valid and Test datasets. |
From Informal to Formal – Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs (2025.acl-long)
Copied to clipboard
Jialun Cao, Yaojie Lu, Meiziniu Li, Haoyang Ma, Haokun Li, Mengda He, Cheng Wen, Le Sun, Hongyu Zhang, Shengchao Qin, Shing-Chi Cheung, Cong Tian
| Challenge: | Recent studies in formal mathematical reasoning have shown an unstoppable growth trend. |
| Approach: | They constructed 18k high-quality instruction-response pairs across five mainstream formal specification languages and evaluated them against ten open-sourced LLMs. |
| Outcome: | The proposed model compared instruction-response pairs across five formal specification languages and found that the LLMs were good at writing proof segments when given either the code, or the detailed description of proof steps. |
TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models (2023.emnlp-main)
Copied to clipboard
Jing Xiong, Jianhao Shen, Ye Yuan, Haiming Wang, Yichun Yin, Zhengying Liu, Lin Li, Zhijiang Guo, Qingxing Cao, Yinya Huang, Chuanyang Zheng, Xiaodan Liang, Ming Zhang, Qun Liu
| Challenge: | Automated theorem proving (ATP) benchmarks focus on symbolic inference but rarely involve understanding complex number combination reasoning. |
| Approach: | They propose a benchmark that requires a model to reduce a trigonometric expression with step-by-step proof and evaluates a generative LM’s reasoning ability on formulas and ability to manipulate, group, and factor number terms. |
| Outcome: | The proposed benchmark evaluates a generative LM’s reasoning ability on formulas and ability to manipulate, group, and factor number terms. |