大规模验证模型提升数学证明可靠性，发现强化学习只改风格不改正确性。
Scaling Generative Verifiers For Natural Language Mathematical Proof Verification And Selection
- 用生成式验证方法组合，规模达数百万token，提升证明选择准确率。
- 强化学习可降低提示敏感性，但无法提升最终答案正确率。
- 强调多基准评估，避免单一测试导致误判，适合系统设计参考。
大型语言模型在最终答案类数学问题上表现优异，主要得益于可验证奖励的强化学习应用。然而，其推理过程常存在缺陷。要迈向严谨的证明型数学，需可靠的证明验证能力。我们分析了多种评估设置，发现单一基准可能导致脆弱或误导性结论。为此，同时评估证明过程与最终答案，获得更可靠的性能度量。将两种生成式验证方法（GenSelect 和 LLM-as-a-Judge）扩展至数百万标记，发现二者结合是解决方案验证与选择的最佳框架。进一步表明，LLM-as-a-Judge 的提示设计显著影响性能，但强化学习可缓解此敏感性。尽管提升了证明层面指标，强化学习并未改善最终答案精度，说明当前模型往往奖励形式或流程正确性而非数学有效性。研究结果为可扩展的证明验证与选择系统提供了实用设计指南。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。