Safe：通过回顾式逐步感知的形式化验证增强大语言模型的数学推理能力
Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification
AI总结：
本文提出回顾式逐步形式化验证框架Safe，利用Lean 4对LLM数学推理的每一步进行形式化证明以识别幻觉，并构建FormalStep基准，显著提升推理性能与可验证性。
摘要：
思维链（Chain-of-Thought, CoT）提示已成为激发大语言模型（LLMs）推理能力的事实标准方法。然而，为了缓解CoT中难以检测的幻觉，当前的方法（如过程奖励模型PRMs或自洽性）以不透明黑箱的方式运行，无法为其判断提供可检查的证据，这可能限制了它们的有效性。为了解决这一问题，我们受到“支持数学论断的黄金标准是提供证明”这一思想的启发，提出了一个回顾式、逐步感知的形式化验证框架Safe。我们不是分配任意分数，而是在每个推理步骤中努力用形式化数学语言Lean 4表达数学论断，并提供形式化证明以识别幻觉。我们在多个语言模型和多种数学数据集上评估了框架Safe，结果表明其性能显著提升，同时提供了可解释且可验证的证据。我们还提出了FormalStep，作为一个包含30,809条形式化陈述的步骤正确性定理证明基准。据我们所知，我们的工作代表了首次利用形式化数学语言Lean 4来验证由LLMs生成的自然语言内容的尝试，这与形式化数学语言最初被创造的原因一致：为容易产生幻觉的人类书写证明提供坚实的基础。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
