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. |
Similar Papers
Improving the Language Understanding Capabilities of Large Language Models Using Reinforcement Learning (2025.findings-emnlp)
Copied to clipboard
| Challenge: | Instruction-fine-tuned large language models (LLMs) under 14B parameters underperform on NLU tasks . we explore a framework to improve the NLU capabilities of LLMs . |
| Approach: | They propose to use Proximal Policy Optimization to improve NLU capabilities . they frame NLU as a reinforcement learning environment and optimize for reward signals . |
| Outcome: | The proposed framework outperforms supervised fine-tuning on GLUE and superGLUE tasks. |
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. |
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. |
Enhancing Reinforcement Learning with Label-Sensitive Reward for Natural Language Understanding (2024.acl-long)
Copied to clipboard
| Challenge: | Recent advances in large language models (LLMs) have yielded remarkable performance, but objective mismatch issues hinder RLHF learning. |
| Approach: | They propose a Reinforcement Learning framework enhanced with Label-sensitive reward to enhance LLMs' alignment and generation capabilities. |
| Outcome: | The proposed framework improves performance on five diverse models across eight 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. |
Parsing Natural Language into Propositional and First-Order Logic with Dual Reinforcement Learning (2022.coling-1)
Copied to clipboard
Xuantao Lu, Jingping Liu, Zhouhong Gu, Hanwen Tong, Chenhao Xie, Junyang Huang, Yanghua Xiao, Wenguang Wang
| Challenge: | Existing methods to parse natural language into structured logical expressions have limitations due to paucity of labeled data. |
| Approach: | They propose a scoring model to automatically learn a model-based reward . they also propose introducing a Chinese-PL/FOL dataset to compensate for paucity of labeled data . |
| Outcome: | The proposed model outperforms competitors on several 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. |
CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization (2026.acl-long)
Copied to clipboard
Zhongyuan Peng, Yifan Yao, Kaijing Ma, Shuyue Guo, Yizhe Li, Yichi Zhang, Chenchen Zhang, Yifan Zhang, Zhouliang Yu, Luming Li, Minghao Liu, Yihang Xia, Jiawei Shen, Yuchen Wu, Yixin Cao, Zhaoxiang Zhang, Wenhao Huang, Jiaheng Liu, Ge Zhang
| Challenge: | Existing approaches to formalizing mathematical statements face limitations in accuracy, especially in the context of complex, highlevel problems that involve sophisticated mathematical reasoning. |
| Approach: | They propose a CriticLean framework that elevates the role of the critic from a passive validator to an active learning component and introduce a benchmark to measure models’ ability to distinguish semantically correct from incorrect formalizations. |
| Outcome: | The proposed framework outperforms open- and closed-source benchmarks and shows that it significantly outperformed existing models. |
DeepTrans: Deep Reasoning Translation via Reinforcement Learning (2026.tacl-1)
Copied to clipboard
| Challenge: | Recent studies have shown promising performance in various downstream tasks. |
| Approach: | They propose a deep reasoning translation model that learns free translation via reinforcement learning (RL) they build a reward model with pre-defined scoring criteria on the translation results and thought processes . |
| Outcome: | The proposed model outperforms strong deep reasoning LLMs in literature translation and outperformed other models. |
TOWER+: Bridging Generality and Translation Specialization in Multilingual LLMs (2026.acl-long)
Copied to clipboard
Ricardo Rei, Nuno M Guerreiro, José Pombal, João Alves, Amin Farajian, Pedro Teixeirinha, Andre Martins
| Challenge: | Large Language Models (LLMs) are emerging as the de facto solution for multilingual machine translation. |
| Approach: | They propose a suite of LLMs that can be fine-tuned to deliver strong performance on translation and multilingual general-purpose text capabilities. |
| Outcome: | The proposed models outperform existing models on translation and general-purpose tasks. |