# Step-Wise Formal Verification for LLM-Based Mathematical Problem Solving arXiv: https://arxiv.org/abs/2505.20869 ยท HTML: https://mlsanity.com/paper/2505.20869/ ## Key facts - Cited by 5 papers in the map (data through 14 Oct 2026). - Placed in Mathematical reasoning, one of 17 directions in LLM reasoning. - Builds on 27 of its 43 references that are in the map. - First posted on arXiv 27 May 2025. ## Placed in - LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/) ## Builds on (most cited first, 27 of 27) - [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023) - [Self-Consistency Improves Chain of Thought Reasoning in Language Models](https://mlsanity.com/paper/2203.11171/) (2022) - [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021) - [Let's Verify Step by Step](https://mlsanity.com/paper/2305.20050/) (2023) - [Self-Refine: Iterative Refinement with Self-Feedback](https://mlsanity.com/paper/2303.17651/) (2023) - [Math-Shepherd: Verify and Reinforce LLMs Step-by-step without Human Annotations](https://mlsanity.com/paper/2312.08935/) (2023) - [The Lessons of Developing Process Reward Models in Mathematical Reasoning](https://mlsanity.com/paper/2501.07301/) (2025) - [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023) - [ProcessBench: Identifying Process Errors in Mathematical Reasoning](https://mlsanity.com/paper/2412.06559/) (2024) - [When Can LLMs Actually Correct Their Own Mistakes? A Critical Survey of Self-Correction of LLMs](https://mlsanity.com/paper/2406.01297/) (2024) - [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024) - [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023) - [LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers](https://mlsanity.com/paper/2310.15164/) (2023) - [Monte Carlo Tree Search: A Review of Recent Modifications and Applications](https://mlsanity.com/paper/2103.04931/) (2021) - [Deductive Verification of Chain-of-Thought Reasoning](https://mlsanity.com/paper/2306.03872/) (2023) - [SatLM: Satisfiability-Aided Language Models Using Declarative Prompting](https://mlsanity.com/paper/2305.09656/) (2023) - [PRMBench: A Fine-grained and Challenging Benchmark for Process-Level Reward Models](https://mlsanity.com/paper/2501.03124/) (2025) - [Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2](https://mlsanity.com/paper/2502.03544/) (2025) - [CriticBench: Benchmarking LLMs for Critique-Correct Reasoning](https://mlsanity.com/paper/2402.14809/) (2024) - [Enhancing LLM Reasoning via Critique Models with Test-Time and Training-Time Supervision](https://mlsanity.com/paper/2411.16579/) (2024) - [Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization](https://mlsanity.com/paper/2403.18120/) (2024) - [GRACE: Discriminator-Guided Chain-of-Thought Reasoning](https://mlsanity.com/paper/2305.14934/) (2023) - [MATHSENSEI: A Tool-Augmented Large Language Model for Mathematical Reasoning](https://mlsanity.com/paper/2402.17231/) (2024) - [ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis](https://mlsanity.com/paper/2501.18310/) (2025) - [Error Classification of Large Language Models on Math Word Problems: A Dynamically Adaptive Framework](https://mlsanity.com/paper/2501.15581/) (2025) - [Not All Votes Count! Programs as Verifiers Improve Self-Consistency of Language Models for Math Reasoning](https://mlsanity.com/paper/2410.12608/) (2024) - [Instantiation-based Formalization of Logical Reasoning Tasks using Language Models and Logical Solvers](https://mlsanity.com/paper/2501.16961/) (2025) ## Built on by (most cited first, 5 of 5) - [Autoformalization in the Era of Large Language Models: A Survey](https://mlsanity.com/paper/2505.23486/) (2025) - [AgentGuard: Runtime Verification of AI Agents](https://mlsanity.com/paper/2509.23864/) (2025) - [ReProbe: Efficient Test-Time Scaling of Multi-Step Reasoning by Probing Internal States of Large Language Models](https://mlsanity.com/paper/2511.06209/) (2025) - [RMA: an Agentic System for Research-Level Mathematical Problems](https://mlsanity.com/paper/2605.22875/) (2026) - [Theoria: Rewrite-Acceptability Verification over Informal Reasoning States](https://mlsanity.com/paper/2607.01223/) (2026) ## Abstract (arXiv) Large Language Models (LLMs) have demonstrated formidable capabilities in solving mathematical problems, yet they may still commit logical reasoning and computational errors during the problem-solving process. Thus, this paper proposes a framework, MATH-VF, which includes a Formalizer and a Critic, for formally verifying the correctness of the solutions generated by large language models. Our framework first utilizes a Formalizer which employs an LLM to translate a natural language solution into a formal context. Afterward, our Critic (which integrates various external tools such as a Computer Algebra System and an SMT solver) evaluates the correctness of each statement within the formal context, and when a statement is incorrect, our Critic provides corrective feedback. We empirically investigate the effectiveness of MATH-VF in two scenarios: 1) Verification: MATH-VF is utilized to determine the correctness of a solution to a given problem. 2) Refinement: When MATH-VF identifies errors in the solution generated by an LLM-based solution generator for a given problem, it submits the corrective suggestions proposed by the Critic to the solution generator to regenerate the solution. We evaluate our framework on widely used mathematical benchmarks: MATH500 and ProcessBench, demonstrating the superiority of our approach over existing approaches.