Step-Wise Formal Verification for LLM-Based Mathematical Problem Solving

TL;DR

This paper introduces MATH-VF, a framework combining formal verification and correction tools to improve the accuracy of LLM-generated solutions to mathematical problems, verified on standard benchmarks.

Contribution

It presents a novel step-wise verification framework for LLM-based math problem solving, integrating formal translation and external tools for correctness assessment and correction.

Findings

MATH-VF effectively verifies solutions on MATH500 and ProcessBench.

The framework improves solution accuracy over existing methods.

It enables iterative refinement of LLM solutions through formal verification.

Abstract

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.