# Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification

arXiv: https://arxiv.org/abs/2506.04592 · HTML: https://mlsanity.com/paper/2506.04592/

## Key facts

- Cited by 17 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 24 of its 67 references that are in the map.
- First posted on arXiv 5 Jun 2025.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

## Builds on (most cited first, 24 of 24)

- [The Llama 3 Herd of Models](https://mlsanity.com/paper/2407.21783/) (2024)
- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [GPT-4o System Card](https://mlsanity.com/paper/2410.21276/) (2024)
- [GPQA: A Graduate-Level Google-Proof Q&A Benchmark](https://mlsanity.com/paper/2311.12022/) (2023)
- [MetaMath: Bootstrap Your Own Mathematical Questions for Large Language Models](https://mlsanity.com/paper/2309.12284/) (2023)
- [BigCodeBench: Benchmarking Code Generation with Diverse Function Calls and Complex Instructions](https://mlsanity.com/paper/2406.15877/) (2024)
- [RewardBench: Evaluating Reward Models for Language Modeling](https://mlsanity.com/paper/2403.13787/) (2024)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Skywork-Reward: Bag of Tricks for Reward Modeling in LLMs](https://mlsanity.com/paper/2410.18451/) (2024)
- [Large Language Models for Mathematical Reasoning: Progresses and Challenges](https://mlsanity.com/paper/2402.00157/) (2024)
- [SciBench: Evaluating College-Level Scientific Problem-Solving Abilities of Large Language Models](https://mlsanity.com/paper/2307.10635/) (2023)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning](https://mlsanity.com/paper/2402.06332/) (2024)
- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [EvoCodeBench: An Evolving Code Generation Benchmark Aligned with Real-World Code Repositories](https://mlsanity.com/paper/2404.00599/) (2024)
- [FIMO: A Challenge Formal Dataset for Automated Theorem Proving](https://mlsanity.com/paper/2309.04295/) (2023)
- [Process-Driven Autoformalization in Lean 4](https://mlsanity.com/paper/2406.01940/) (2024)
- [Can LLMs Solve longer Math Word Problems Better?](https://mlsanity.com/paper/2405.14804/) (2024)
- [S^3cMath: Spontaneous Step-level Self-correction Makes Large Language Models Better Mathematical Reasoners](https://mlsanity.com/paper/2409.01524/) (2024)
- [Can We Verify Step by Step for Incorrect Answer Detection?](https://mlsanity.com/paper/2402.10528/) (2024)
- [UGMathBench: A Diverse and Dynamic Benchmark for Undergraduate-Level Mathematical Reasoning with Large Language Models](https://mlsanity.com/paper/2501.13766/) (2025)

## Built on by (most cited first, 17 of 17)

- [AgentGuard: Runtime Verification of AI Agents](https://mlsanity.com/paper/2509.23864/) (2025)
- [Towards a Common Framework for Autoformalization](https://mlsanity.com/paper/2509.09810/) (2025)
- [Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification](https://mlsanity.com/paper/2601.22642/) (2026)
- [FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation](https://mlsanity.com/paper/2608.10916/) (2026)
- [FMC: Formalization of Natural Language Mathematical Competition Problems](https://mlsanity.com/paper/2507.11275/) (2025)
- [From Static to Dynamic: Adaptive Monte Carlo Search for Mathematical Process Supervision](https://mlsanity.com/paper/2509.24351/) (2025)
- [Mathematics with large language models as provers and verifiers](https://mlsanity.com/paper/2510.12829/) (2025)
- [SciHorizon-GENE: Benchmarking LLM for Life Sciences Inference from Gene Knowledge to Functional Understanding](https://mlsanity.com/paper/2601.12805/) (2026)
- [Beyond Length Scaling: Synergizing Breadth and Depth for Generative Reward Models](https://mlsanity.com/paper/2603.01571/) (2026)
- [Where Reasoning Breaks: Logic-Aware Path Selection by Controlling Logical Connectives in LLMs Reasoning Chains](https://mlsanity.com/paper/2604.20564/) (2026)
- [VeriBound: PAC-Bayesian Generalization Bounds for Process Reward Models Trained with Formal Verification Tools](https://mlsanity.com/paper/2606.20740/) (2026)
- [VeryTrace: Verifying Reasoning Traces through Compilable Formalism and Structured Verification](https://mlsanity.com/paper/2606.24124/) (2026)
- [Evaluating the Robustness of Proof Autoformalization in Lean 4](https://mlsanity.com/paper/2606.14867/) (2026)
- [LAVA: Logic-Aware Validation and Augmentation Framework for Large-Scale Financial Document Auditing](https://mlsanity.com/paper/2608.16763/) (2026)
- [When Tokenization is Secretly Output Supervision](https://mlsanity.com/paper/2609.01386/) (2026)
- [Learning to Prove, Not Just to Answer: Reinforcement Learning from Formal Verification for Natural-Language Logical Reasoning](https://mlsanity.com/paper/2609.37203/) (2026)
- [LeanPRM: Lean-Grounded Process Supervision for Natural Language Proof Verification](https://mlsanity.com/paper/2610.17697/) (2026)

## Abstract (arXiv)

Chain-of-Thought (CoT) prompting has become the de facto method to elicit reasoning capabilities from large language models (LLMs). However, to mitigate hallucinations in CoT that are notoriously difficult to detect, current methods such as process reward models (PRMs) or self-consistency operate as opaque boxes and do not provide checkable evidence for their judgments, possibly limiting their effectiveness. To address this issue, we draw inspiration from the idea that "the gold standard for supporting a mathematical claim is to provide a proof". We propose a retrospective, step-aware formal verification framework Safe. Rather than assigning arbitrary scores, we strive to articulate mathematical claims in formal mathematical language Lean 4 at each reasoning step and provide formal proofs to identify hallucinations. We evaluate our framework Safe across multiple language models and various mathematical datasets, demonstrating a significant performance improvement while offering interpretable and verifiable evidence. We also propose FormalStep as a benchmark for step correctness theorem proving with 30,809 formal statements. To the best of our knowledge, our work represents the first endeavor to utilize formal mathematical language Lean 4 for verifying natural language content generated by LLMs, aligning with the reason why formal mathematical languages were created in the first place: to provide a robust foundation for hallucination-prone human-written proofs.