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. |
Similar Papers
Let’s Reason Formally: Natural-Formal Hybrid Reasoning Enhances LLM’s Math Capability (2025.emnlp-main)
Copied to clipboard
| Challenge: | Recent work has focused on improving the mathematical reasoning capabilities of Large Language Models (LLMs). |
| Approach: | They propose an end-to-end framework to integrate FL into NL math reasoning . they propose a problem alignment method that reformulates QA and existence problems . |
| Outcome: | The proposed framework achieves 89.80% and 84.34% accuracy rates on the MATH-500 and the AMC benchmarks. |
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. |
CHAMP: A Competition-level Dataset for Fine-Grained Analyses of LLMs’ Mathematical Reasoning Capabilities (2024.findings-acl)
Copied to clipboard
| Challenge: | Recent large language models have shown indications of mathematical reasoning ability on competition-level problems. |
| Approach: | They propose a benchmark dataset to enable such analyses using large language models. |
| Outcome: | The proposed model performs better with concepts and hints than with the best model, but it is difficult to verify. |
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. |
GSM-Plus: A Comprehensive Benchmark for Evaluating the Robustness of LLMs as Mathematical Problem Solvers (2024.acl-long)
Copied to clipboard
| Challenge: | Large language models (LLMs) have demonstrated impressive performance across various mathematical reasoning benchmarks. |
| Approach: | They introduce an adversarial grade school math dataset and explore whether LLMs can be more robust when questions are slightly changed. |
| Outcome: | The proposed method generates and verifies each intermediate thought based on its reasoning goal and calculation result. |
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. |
Not All Options Are Created Equal: Textual Option Weighting for Token-Efficient LLM-Based Knowledge Tracing (2025.findings-emnlp)
Copied to clipboard
| Challenge: | Large Language Models (LLMs) have strong reasoning and generalization abilities, but they struggle to reflect the histories of example learners within a single prompt during in-context learning. |
| Approach: | They propose a LLM-based option weighted knowledge tracing framework that encodes the interaction histories of example learners in context as textual categorical option weights. |
| Outcome: | The proposed framework outperforms existing LLM-based KT models in warm-start and few-shot settings. |
LLMs for Mathematical Modeling: Towards Bridging the Gap between Natural and Mathematical Languages (2025.findings-naacl)
Copied to clipboard
| Challenge: | Large Language Models (LLMs) have demonstrated strong performance across various natural language processing tasks, but their proficiency in mathematical reasoning remains a key challenge. |
| Approach: | They propose a process-oriented framework to evaluate LLMs' ability to construct mathematical models, using solvers to compare outputs with ground truth. |
| Outcome: | The proposed framework evaluates LLMs' ability to construct mathematical models, using solvers to compare outputs with ground truth. |
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. |