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. |
Similar Papers
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. |
NL2Lean: Translating Natural Language into Lean 4 through Multi-Aspect Reinforcement Learning (2025.emnlp-main)
Copied to clipboard
Yue Fang, Shaohan Huang, Xin Yu, Haizhen Huang, Zihan Zhang, Weiwei Deng, Furu Wei, Feng Sun, Qi Zhang, Zhi Jin
| Challenge: | Existing formal proof assistants rely on instruction tuning and lack fine-grained structural and semantic alignment. |
| Approach: | They propose a reinforcement learning framework that enables LLMs to translate natural language into formal language such as Lean 4 . they use a model with basic translation ability to refine the model's reinforcement learning . |
| Outcome: | The proposed method outperforms baseline models on NL-to-Lean 4 tasks. |
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. |
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. |
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. |
Harnessing the Power of Large Language Models for Natural Language to First-Order Logic Translation (2024.acl-long)
Copied to clipboard
| Challenge: | Logic-based approaches to reasoning have lost popularity due to limited scalability and coverage. |
| Approach: | They present a dataset of 28K sentence-level NL-FOL pairs from GPT4 and a LogicLLaMA2-7B/13B fine-tuned on MALLS for NL translation. |
| Outcome: | The proposed model can be used standalone or to correct previously generated rules by GPT3.5. |
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. |
FANS: Formal Answer Selection for LLM Natural Language Math Reasoning Using Lean4 (2025.emnlp-main)
Copied to clipboard
| Challenge: | Existing frameworks that use Lean4 to enhance LLMs' NL reasoning abilities have been controversial in the field of math reasoning. |
| Approach: | They propose a framework that utilizes Lean4 to enhance LLMs’ NL math reasoning ability by generating a Lean 4 theorem statement and a proof-generating LLM. |
| Outcome: | The proposed framework improves LLMs' NL math reasoning ability by 2% across several math benchmarks and higher further based on reward models or in subfields such as algebra and number theory. |
LLM-powered Data Augmentation for Enhanced Cross-lingual Performance (2023.emnlp-main)
Copied to clipboard
| Challenge: | Existing training data for multilingual commonsense reasoning datasets is limited. |
| Approach: | They propose to use large language models for data augmentation in multilingual datasets . they use Dolly-v2, StableVicuna, ChatGPT, and GPT-4 to augment three datasets. |
| Outcome: | The proposed model outperforms larger general-purpose, zero-shot models when training in smaller models. |