FANS — 用于自然语言数学推理的形式化答案选择框架基于 Lean4

大型语言模型 (LLM) 在 various 任务中展现出惊人的能力，尤其是在文本生成、分类和问答等方面。然而，LLM 的推理能力仍面临诸多争议。自然语言 (NL) 的内在歧义限制了 LLM 执行可验证推理的能力，使得其答案缺乏一致性和可信的依据。为解决上述问题，本文提出一种新框架 FANS：Formal ANswer Selection for Natural Language Math Reasoning Using Lean4。据我们所知，这是首个利用 Lean4 来提升 LLM 在 NL 数学推理方面能力的框架。具体而言，给定 NL 数学问题和 LLM 生成的答案，FANS 首先将其翻译为 Lean4 定理语句。随后，它尝试使用 Lean4 证明器对其进行证明并由 Lean4 验证。最后，利用验证结果辅助答案选择。该框架增强了 LLM 在提供可计算机验证正确答案形式解方面的 NL 数学能力，并为答案选择提出了一种超越奖励模型的方法。大量实验表明，我们框架的有效性。它可使基于强奖励模型的 LLM 在 MATH-500 数据集上的准确率提高最高可达 1.91%，在 AMC-23 数据集上提高最高可达 8.33%。在 Lean4 专家较多的某些领域，如数论中，我们甚至可以选择所有正确解。定性分析还显示，我们框架能够使 NL 结果通过 Lean4 证明形式化支撑。作为该领域的开创性工作，我们将开源所有模型和数据集，以进一步推动该领域的发展。