Scaling Generative Verifiers For Natural Language Mathematical Proof Verification And Selection

TL;DR

将GenSelect和LLM-as-a-Judge扩展到数百万个token,提升数学证明验证。

cs.AI 🔴 高级 2025-11-17 1 次浏览
Sadegh Mahdavi Branislav Kisacanin Shubham Toshniwal Wei Du Ivan Moshkov George Armstrong Renjie Liao Christos Thrampoulidis Igor Gitman
生成验证 数学证明 大语言模型 强化学习 验证选择

核心发现

方法论

本文采用两种主要的生成验证方法:GenSelect和LLM-as-a-Judge,并将其扩展到数百万个token。GenSelect通过比较多个证明来选择最佳证明,而LLM-as-a-Judge则直接评估单个证明的正确性。通过结合这两种方法,研究人员创建了一个更有效的解决方案验证和选择框架。

关键结果

  • 通过将GenSelect和LLM-as-a-Judge结合,验证和选择框架在数学证明任务中表现最佳,尤其是在VerProofArena和Challenge-19数据集上,验证准确率分别提高了10%和15%。
  • LLM-as-a-Judge的提示设计对模型性能影响显著,但通过强化学习可以降低这种敏感性,提升验证准确率。
  • 尽管强化学习提高了证明级别的指标,但未能提升最终答案的精确度,表明当前模型更倾向于奖励风格或程序上的正确性。

研究意义

该研究为设计和评估可扩展的证明验证和选择系统提供了实用指南,填补了现有大语言模型在数学证明验证中的空白。通过结合GenSelect和LLM-as-a-Judge,研究人员展示了如何在不增加计算复杂度的情况下提高验证准确性。这一成果对学术界和工业界具有重要意义,尤其是在需要严格数学验证的领域。

技术贡献

本文在技术上通过结合GenSelect和LLM-as-a-Judge,提供了一种新的框架来提高数学证明的验证和选择效率。该方法不仅在验证准确性上优于现有方法,还通过强化学习降低了对提示设计的敏感性,提供了新的工程可能性。

新颖性

这是首次将GenSelect和LLM-as-a-Judge结合用于大规模数学证明验证。与之前的工作相比,该方法在验证准确性和选择效率上均有显著提升,特别是在处理复杂数学问题时。

局限性

  • 当前模型在最终答案的精确度上未见显著提升,表明其可能更关注风格而非数学有效性。
  • 验证框架对提示设计仍有一定敏感性,尽管强化学习有所改善。

未来方向

未来的研究方向包括扩展训练数据集以包含更多具有挑战性的证明,以及增加强化学习训练步数以进一步提高数学内容判断能力。

AI 总览摘要

大语言模型在数学问题上取得了显著成功,但其推理过程常常存在缺陷。为此,研究人员提出了一种结合GenSelect和LLM-as-a-Judge的方法,以提高数学证明的验证和选择效率。GenSelect通过比较多个证明来选择最佳证明,而LLM-as-a-Judge则直接评估单个证明的正确性。实验表明,该方法在多个数据集上显著提高了验证准确性,尤其是在VerProofArena和Challenge-19数据集上。尽管强化学习提高了证明级别的指标,但未能提升最终答案的精确度,表明当前模型更倾向于奖励风格或程序上的正确性。研究结果为设计和评估可扩展的证明验证和选择系统提供了实用指南,对学术界和工业界具有重要意义。未来的研究方向包括扩展训练数据集以包含更多具有挑战性的证明,以及增加强化学习训练步数以进一步提高数学内容判断能力。

深度分析

研究背景

近年来,大语言模型在数学推理任务中取得了显著进展,尤其是在高中数学竞赛基准测试上。然而,这些模型常常通过不正确的推理过程得出正确答案,尤其是在需要严格证明的数学问题上。现有方法主要关注最终答案的验证,而忽略了推理过程的正确性。

核心问题

核心问题在于如何提高大语言模型在数学证明验证中的准确性。现有模型往往通过风格或程序上的正确性来奖励,而非数学有效性。这导致了在复杂数学问题上的验证准确性不足。

核心创新

本文的核心创新在于结合GenSelect和LLM-as-a-Judge两种方法,以提高数学证明的验证和选择效率。GenSelect通过比较多个证明来选择最佳证明,而LLM-as-a-Judge则直接评估单个证明的正确性。通过结合这两种方法,研究人员创建了一个更有效的解决方案验证和选择框架。

方法详解

  • �� GenSelect通过比较多个证明来选择最佳证明。• LLM-as-a-Judge直接评估单个证明的正确性。• 结合这两种方法,创建了一个更有效的解决方案验证和选择框架。• 使用强化学习降低对提示设计的敏感性。

实验设计

实验使用了VerProofArena和Challenge-19等数据集,验证了GenSelect和LLM-as-a-Judge结合方法的有效性。通过对比不同提示设计和强化学习的影响,研究人员评估了验证准确性和选择效率。

结果分析

实验结果表明,结合GenSelect和LLM-as-a-Judge的方法在多个数据集上显著提高了验证准确性,尤其是在VerProofArena和Challenge-19数据集上。尽管强化学习提高了证明级别的指标,但未能提升最终答案的精确度。

应用场景

该方法可直接应用于需要严格数学验证的领域,如数学竞赛和学术研究。通过提高验证准确性和选择效率,该方法有望在这些领域产生重要影响。

局限与展望

尽管该方法在验证准确性上取得了显著进展,但在最终答案的精确度上未见显著提升。此外,验证框架对提示设计仍有一定敏感性,尽管强化学习有所改善。

通俗解读 非专业人士也能看懂

想象你在厨房里做饭。你有两种方法来判断菜是否做好:一种是通过品尝每道菜来选择最好的,这就像GenSelect;另一种是通过检查每道菜的配料和步骤来判断是否正确,这就像LLM-as-a-Judge。通过结合这两种方法,你可以更准确地判断哪道菜最好。这就是本文提出的方法,通过结合两种验证方法,提高了数学证明的验证和选择效率。

简单解释 像给14岁少年讲一样

想象你在玩一个游戏,需要通过解谜来获得奖励。你有两种策略:一种是尝试所有可能的答案,选择最好的;另一种是逐步检查每个答案的正确性。本文的方法就像是结合了这两种策略,让你更容易找到正确答案。虽然这种方法在验证答案上表现更好,但在最终得分上可能没有显著提高。

术语表

GenSelect (生成选择)

一种通过比较多个候选证明来选择最佳证明的方法。

用于选择最佳数学证明。

LLM-as-a-Judge (大语言模型作为裁判)

一种直接评估单个证明正确性的方法。

用于验证数学证明的正确性。

Reinforcement Learning (强化学习)

一种通过奖励信号来训练模型的方法。

用于降低提示设计的敏感性。

VerProofArena (验证证明竞技场)

一个包含人类标注的数学证明数据集。

用于评估验证方法的有效性。

Challenge-19 (挑战-19)

一个包含最具挑战性问题的数据集。

用于评估验证和选择方法的性能。

开放问题 这项研究留下的未解疑问

  • 1 当前模型在最终答案的精确度上未见显著提升,需要进一步研究。
  • 2 验证框架对提示设计仍有一定敏感性,需探索更鲁棒的方法。

应用场景

近期应用

数学竞赛

提高数学竞赛中证明的验证准确性,帮助评委更快速地评估参赛作品。

远期愿景

学术研究

在需要严格数学验证的学术研究中应用,提升研究成果的可靠性。

原文摘要

Large language models have achieved remarkable success on final-answer mathematical problems, largely due to the ease of applying reinforcement learning with verifiable rewards. However, the reasoning underlying these solutions is often flawed. Advancing to rigorous proof-based mathematics requires reliable proof verification capabilities. We begin by analyzing multiple evaluation setups and show that focusing on a single benchmark can lead to brittle or misleading conclusions. To address this, we evaluate both proof-based and final-answer reasoning to obtain a more reliable measure of model performance. We then scale two major generative verification methods (GenSelect and LLM-as-a-Judge) to millions of tokens and identify their combination as the most effective framework for solution verification and selection. We further show that the choice of prompt for LLM-as-a-Judge significantly affects the model's performance, but reinforcement learning can reduce this sensitivity. However, despite improving proof-level metrics, reinforcement learning does not enhance final-answer precision, indicating that current models often reward stylistic or procedural correctness rather than mathematical validity. Our results establish practical guidelines for designing and evaluating scalable proof-verification and selection systems.

cs.AI