用形式化方法验证大模型数学解题，自动发现并修正逻辑错误。
Step-Wise Formal Verification for LLM-Based Mathematical Problem Solving
- 将自然语言解题过程转为形式化表达，便于精确验证。
- 在MATH500和ProcessBench上验证正确率显著优于现有方法。
- 适合需要高可靠性的数学推理系统或教育评估场景。
大型语言模型在解决数学问题上展现出强大能力，但仍可能在推理与计算过程中出现错误。为此，本文提出MATH-VF框架，包含Formalizer与Critic两部分，用于形式化验证大模型生成解题过程的正确性。首先，Formalizer利用大模型将自然语言解题过程转化为形式化上下文；随后，Critic集成计算机代数系统与SMT求解器，逐条评估形式化陈述的正确性，并在发现错误时提供修正反馈。我们在两种场景下评估该框架：1）验证——判断给定解题方案的正确性；2）优化——当检测到错误时，将修正建议反馈给原解题生成器以重新生成答案。在广泛使用的数学基准MATH500与ProcessBench上，MATH-VF表现出优于现有方法的性能。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。