QDTSynth: Quality-Driven Formal Theorem Synthesis for Enhancing Proving Performance of LLMs (2025.acl-long)
Copied to clipboard
| Challenge: | Existing formal languages such as Lean, Coq and Metamath are proving to be useful in formal theorem proving . however, there is a scarcity of high-quality supervised fine-tuning data for formal proofs . |
| Approach: | They propose a Q**uality-**D**riven **T**heorem **S**ynthesis method in Lean4 . they propose diversity screening and the self-assessment method to select theoremas that exhibit diversity and high quality from the initial synthetic statements. |
| Outcome: | The proposed method significantly improves performance of open-source LLMs in theorem proving tasks. |
Similar Papers
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. |
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. |
KodCode: A Diverse, Challenging, and Verifiable Synthetic Dataset for Coding (2025.findings-acl)
Copied to clipboard
| Challenge: | Existing code-focused resources typically fail to ensure either the breadth of coverage or verifiable correctness. |
| Approach: | They propose a synthetic dataset that provides high-quality, verifiable training data for Large Language Models for coding. |
| Outcome: | The proposed dataset surpasses Qwen2.5-Coder-32B-Instruct and DeepSeek-R1-Distill-Llama-70B in performance on coding benchmarks. |
ResearchBench: Benchmarking LLMs in Scientific Discovery via Inspiration-Based Task Decomposition (2026.findings-acl)
Copied to clipboard
Yujie Liu, Zonglin Yang, Tong Xie, Jinjie Ni, Ben Gao, Yuqiang Li, Shixiang Tang, Wanli Ouyang, Erik Cambria, Dongzhan Zhou
| Challenge: | Large language models have shown potential in assisting scientific research, yet their ability to discover high-quality research hypotheses remains unexamined due to the lack of a dedicated benchmark. |
| Approach: | They propose a benchmark for evaluating large language models on a sufficient set of scientific discovery sub-tasks. |
| Outcome: | The proposed framework extracts critical components from papers across 12 disciplines with expert validation confirming its accuracy. |
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. |
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. |
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. |
LeanReasoner: Boosting Complex Logical Reasoning with Lean (2024.naacl-long)
Copied to clipboard
| Challenge: | Large language models (LLMs) often struggle with complex logical reasoning due to logical inconsistencies and the inherent difficulty of such reasoning. |
| Approach: | They propose a method that formalizes logical reasoning problems into theorems within Lean and then proves or disproving the corresponding theorels. |
| Outcome: | The proposed method achieves state-of-the-art performance on the FOLIO dataset and near this level on ProofWriter. |
QEFT: Quantization for Efficient Fine-Tuning of LLMs (2024.findings-emnlp)
Copied to clipboard
| Challenge: | Existing methods to optimize inference and fine-tuning for large language models have failed to improve all aspects of the process. |
| Approach: | They propose a new technique that accelerates both inference and fine-tuning while using fewer resources. |
| Outcome: | The proposed technique accelerates both inference and fine-tuning while using fewer resources. |
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. |