用形式验证工具训练推理验证器：宾夕法尼亚州立大学研究团队让AI自动检查每一步推理是否正确

在现代人工智能研究中，大型语言模型（如GPT、Llama等）已经展现出令人惊艳的推理能力，但它们仍然会犯错。就像我们做数学题时可能在某一步计算出错导致整个答案错误一样，这些AI模型也会在推理过程中的某些步骤出错。而检查每一步推理是否正确的"验证器"（也称为过程奖励模型，PRM）正变得越来越重要。

这项由宾夕法尼亚州立大学的Ryo Kamoi、Yusen Zhang、Nan Zhang、Sarkar Snigdha Sarathi Das和Rui Zhang领导的研究发表于2025年5月21日的arXiv预印本平台（arXiv:2505.15960v1），探索了一种全新方法来构建这种推理验证器。

想象一下，如果你有一位朋友正在解一道复杂的数学题，你需要检查他解题过程中的每一步是否正确。传统上，训练AI来做这种检查需要大量人类专家提供的标注数据，告诉AI哪些步骤是正确的，哪些是错误的。这个过程不仅耗时，而且成本高昂。此外，现有的方法主要集中在数学推理问题上，适用范围有限。

研究团队开发的方法名为"FOVER"（取自Formal Verification的缩写），它巧妙地解决了这两个问题。就像是教孩子学习时，我们会从简单的问题开始，然后逐渐过渡到复杂问题一样，FOVER从形式逻辑和定理证明这类可以用计算机程序（如Z3和Isabelle）自动验证的推理任务开始，然后将学到的技能应用到各种复杂的推理任务中。

简单来说，研究团队首先让AI模型（如Llama 3.1和Qwen 2.5）尝试解决一些形式逻辑和定理证明问题。然后，他们使用计算机程序自动检查每一步是否正确，并用这些自动生成的标注来训练AI验证器。令人惊喜的是，这种方法不仅省去了人工标注的环节，而且训练出来的验证器能够推广到各种不同类型的推理任务中，包括数学推理、常识推理、自然语言推理等。

这就像是教一个孩子先学会检查简单的加减法是否正确，之后他就能运用同样的技能去检查更复杂的代数或几何问题的解法。

更令人印象深刻的是，这种方法训练出的验证器在12个不同的推理基准测试上表现出色，甚至在某些任务上超过了那些使用人工标注或更强大模型标注训练出的验证器。这项研究为提高AI推理能力提供了一条成本效益高且广泛适用的新途径。

接下来，让我们深入了解这项研究的方法、实验和发现。

一、研究背景：为什么我们需要更好的AI推理验证器？

现代的大型语言模型（LLM）如ChatGPT、Claude或Llama已经能够解决复杂的推理问题，但它们仍然容易在推理过程中犯错。想象一下，你请AI解决一道数学题，比如"如果一件衣服原价100元，打75折后是多少钱？"AI可能会这样回答：

第一步：原价 = 折扣价 / 0.75（正确） 第二步：原价 = 26元（错误！应该是折扣价 / 0.75 = 100元）

即使只有一个步骤出错，最终答案也会完全错误。因此，开发能够检查推理过程中每一步是否正确的系统变得尤为重要。

研究人员称这种系统为"过程奖励模型"（Process Reward Models，PRMs）。就像是一位细心的老师，它们能够对AI模型生成的每一步推理给出反馈：这一步是正确的，那一步是错误的。

然而，训练这样的验证器面临两个主要挑战：

首先，传统方法需要大量人工标注的数据，指出推理过程中的每一步是否正确。这既费时又昂贵。想象一下，你需要雇佣数学专家来检查成千上万道题的每一个解题步骤！

其次，现有的验证器主要集中在数学推理上，难以应用到其他类型的推理任务，如逻辑推理或常识推理。

这就像我们有了一位专门教数学的老师，但没有能教语文、物理或历史的老师一样—我们需要一种更通用的方法。

二、FOVER方法：让计算机自动检查AI的推理步骤

研究团队提出了一种名为FOVER的创新方法，它巧妙地利用了形式验证工具来自动标注训练数据。形式验证工具是一种特殊的计算机程序，能够严格、精确地检查某些类型的推理是否正确。

我们可以把这个过程想象成这样：假设你有一个自动批改数学作业的机器，它能够完美地判断每一步计算是否正确。当学生提交作业时，机器会自动标记出哪些步骤是正确的，哪些是错误的。FOVER就相当于利用这样的"自动批改机器"来训练AI验证器。

具体来说，FOVER方法包括以下步骤：

首先，研究团队选择了两类可以用形式验证工具自动检查的任务：形式逻辑推理和形式定理证明。形式逻辑推理就像是判断"如果A导致B，并且A是真的，那么B也是真的"这类语句是否正确。形式定理证明则类似于数学证明，但用更严格的形式化语言表达。

接着，他们让AI模型（如Llama 3.1和Qwen 2.5）尝试解决这些任务，生成包含多个推理步骤的解答。

然后，他们使用形式验证工具（Z3用于形式逻辑，Isabelle用于定理证明）自动检查每一步推理是否正确，从而创建包含精确标注的训练数据。

最后，他们使用这些自动标注的数据来训练AI验证器，教会它识别正确和错误的推理步骤。

这就像是我们先让学生尝试解答一些有标准答案的题目，然后用自动批改系统标记出每一步是否正确，最后用这些带有标记的作业来训练一个新的AI助教，让它学会如何判断推理步骤的正确性。

FOVER的关键创新在于，它不需要人工标注数据，而是利用计算机程序自动生成精确的标注。更令人惊喜的是，尽管它仅在形式逻辑和定理证明这两类任务上训练，但训练出来的验证器却能够推广到各种不同类型的推理任务上。

三、数据集创建：如何自动标注推理步骤的正确性

研究团队为FOVER构建了一个全新的数据集，包含来自形式逻辑和形式定理证明两类任务的推理步骤，并使用形式验证工具自动标注每一步是否正确。

对于形式逻辑任务，他们使用了FLDx2数据集，这是一个专门用于多步骤一阶逻辑推理的数据集。在这类任务中，AI需要判断给定一组前提（例如"如果下雨，地面会湿"和"现在下雨了"），某个结论（"地面是湿的"）是否成立。研究团队使用Z3验证器自动检查每一步推理是否正确。

Z3验证器就像是一个超级严格的逻辑老师，它会精确地检查每一个推理步骤是否符合逻辑规则。例如，当AI模型从"A蕴含B"和"A为真"推导出"B为真"时，Z3会确认这一步是合法的；而当AI从"A蕴含B"错误地推导出"B蕴含A"时，Z3会标记这一步为错误。

对于形式定理证明任务，研究团队基于GSM8K等数学词问题数据集创建了形式化的证明任务。他们首先让AI模型生成非形式化的解答，然后使用更强大的模型（Llama 3.3 70B）将这些解答转换为Isabelle证明助手能够理解的形式化证明语言。最后，他们使用Isabelle自动检查每一步证明是否正确。

这个过程就像是先让学生用日常语言解答数学问题（"首先，我计算打折后的价格：100 × 0.75 = 75元"），然后将这些解答翻译成严格的数学符号语言（"设p为原价，d为折扣率，则折扣价为p×d"），最后用计算机程序检查每一步推导是否符合数学规则。

研究团队使用这种方法创建了一个包含超过20万个带有自动标注的推理步骤的数据集。这个数据集的特殊之处在于，所有标注都是由计算机程序自动生成的，不需要人工参与，且标注的准确性由形式验证工具保证。

四、实验设计：验证器能否泛化到不同类型的推理任务？

研究团队设计了一系列实验来评估FOVER方法的有效性。他们的主要目标是检验在形式逻辑和定理证明任务上训练的验证器是否能够泛化到其他类型的推理任务上。

他们使用两个基础模型作为验证器：Llama 3.1 8B和Qwen 2.5 7B。这些模型首先在FOVER数据集上进行训练，然后在各种推理任务上进行测试。

评估采用了两种主要方法：

第一种方法是"Best-of-K"，即从多个候选解答中选择最佳的一个。想象一下，当我们让AI解决一个问题时，可以让它生成5个不同的解答，然后使用验证器为每个解答打分，选择得分最高的那个。一个好的验证器应该能够选出正确的解答。

研究团队在12个不同的推理基准测试上评估了这种方法，包括：

数学推理任务：GSM8K（小学数学问题）、MATH（高中和大学数学问题）、AQuA-RAT（代数问题）和AIME（美国数学竞赛）。 逻辑推理任务：FOLIO和LogicNLI（逻辑推理问题）。 自然语言推理任务：ANLI和HANS（判断一个句子是否从另一个句子中推导出）。 常识推理任务：MMLU-Pro-NoMath（多领域知识问题，不包括数学）。 BBH任务：包括时序序列、物体追踪和单词排序等挑战性推理任务。

第二种方法是在ProcessBench上评估步骤级别的验证性能。ProcessBench是一个专门用于评估验证器在数学推理任务中检查每一步正确性的基准测试。

研究团队还将FOVER训练的验证器与现有的最先进验证器进行比较，包括那些使用人工标注或更强大模型标注训练的验证器。

五、实验结果：从简单推理到复杂任务的惊人泛化能力

实验结果令人印象深刻，FOVER方法训练的验证器展现出强大的泛化能力，能够有效应用于各种不同类型的推理任务。

在Best-of-K评估中，FOVER验证器明显优于基线模型（即未经额外训练的原始语言模型）。特别是，尽管FOVER验证器仅在形式逻辑和定理证明任务上训练，但它在数学推理、逻辑推理、自然语言推理和常识推理等各种任务上都表现出色。

例如，基于Llama 3.1 8B的FOVER验证器在BBH任务中的表现显著优于基线模型，准确率从55.9%提高到58.8%。同样，基于Qwen 2.5 7B的FOVER验证器在所有评估任务的平均性能从61.6%提高到63.3%。

更令人惊讶的是，FOVER验证器在许多任务上的表现甚至超过了那些使用人工标注或更强大模型标注训练的验证器。尤其是在数学推理以外的任务上，FOVER验证器经常优于专门为这些任务训练的验证器。

这就像是一个学会了检查简单逻辑和数学证明的学生，突然发现自己也能够判断复杂的物理问题、文学分析甚至是历史论证是否正确—这种泛化能力是令人惊讶的。

在ProcessBench上的评估也显示，FOVER验证器在数学推理任务的步骤级别验证上表现出色。例如，基于Llama 3.1 8B的FOVER验证器在步骤级别验证的平均AUROC（一种评估分类器性能的指标）从66.5%提高到75.9%，而基于Qwen 2.5 7B的验证器则从75.6%提高到87.6%。

研究团队还进行了深入的手动分析，确认FOVER确实提高了步骤级别的验证性能，而很少导致性能下降。

六、FOVER的泛化机制：从简单到复杂的迁移学习

FOVER验证器展现出惊人的泛化能力，能够从形式逻辑和定理证明这样的符号任务迁移到各种不同类型的推理任务。研究团队分析了这种泛化机制，发现它体现在多个层面。

首先是从符号到文本的泛化。FOVER数据集包含符号化的推理步骤（如形式逻辑中的"{A} -> {B}"或Isabelle中的形式化证明），但训练出的验证器能够应用于自然语言表达的推理步骤（如"既然艾丽卡今年30岁，而贝丝比艾丽卡大5岁，那么贝丝今年就是35岁"）。

其次是从简单到复杂的泛化。尽管FOVER数据集主要包含GSM8K级别的数学问题（大约小学到初中难度），但训练出的验证器能够有效验证更复杂的MATH数据集（高中到大学难度）中的推理步骤。

最后是跨任务的泛化。训练数据只包含形式逻辑和定理证明这两类任务，但验证器能够应用于各种不同类型的推理任务，如自然语言推理、常识推理等。

这种泛化能力的一个具体例子是FOVER验证器在MMLU-Pro-NoMath数据集上的表现。这个数据集包含各种领域的知识性问题，例如关于哲学概念"绝对主义"的问题。FOVER验证器能够正确理解这个概念并准确识别出推理中的错误，尽管训练数据中并不包含这类知识性问题。

研究团队认为，这种强大的泛化能力源于基础语言模型本身的跨任务迁移学习能力，而FOVER方法通过形式验证工具提供的精确标注进一步增强了这种能力。

七、研究局限性与未来方向

尽管FOVER展现出令人印象深刻的结果，但研究团队也坦率地指出了一些局限性和未来可能的改进方向。

首先，由于计算资源限制，本研究仅评估了8B级别的语言模型作为验证器。未来的研究可以探索更大规模模型的表现，以及FOVER方法的可扩展性。

其次，当前的数据合成方法仅适用于可以用形式验证工具检查的任务。对于更复杂或更主观的推理任务，可能需要其他方法来生成标注。

第三，训练数据中的源任务难度可能不足以充分挑战更强大的模型。当应用FOVER方法于更强大的模型时，可能需要使用更困难的任务来生成有意义的错误样本。

最后，研究团队建议未来工作可以探索更多的迁移学习方法，进一步增强验证器的跨任务泛化能力。例如，使用预训练数据与微调数据的混合、避免灾难性遗忘的技术等。

八、结论：用形式验证工具构建更强大的AI推理验证器

这项研究提出的FOVER方法为构建高效、准确的AI推理验证器提供了一个新途径。通过利用形式验证工具自动标注训练数据，FOVER解决了传统方法中数据标注成本高和适用范围有限的两个关键问题。

研究结果显示，在形式逻辑和定理证明任务上训练的验证器能够泛化到各种不同类型的推理任务，甚至在某些任务上超过了使用人工标注或更强大模型标注训练的验证器。

这项工作的意义不仅在于提供了一种成本效益高的训练方法，更重要的是展示了从简单、可形式化的推理任务到复杂、多样化推理任务的迁移学习能力。这种能力对于构建通用的AI推理系统至关重要。

未来，FOVER方法可能会被应用于更多领域，帮助AI系统在各种推理任务中减少错误，提高可靠性。研究团队也公开了他们的数据集、模型和代码，以促进这一领域的进一步研究。

就像人类学习先掌握基础逻辑和数学原理，然后将这些能力应用到各种复杂问题上一样，FOVER方法训练的AI验证器也展现出类似的学习路径—从基础的形式推理到各种复杂的推理任务，这或许正是构建真正智能系统的一个重要步骤。