arXiv:2504.10337v2 宣布类型: 替换 摘要: 一个AI系统只能在其能够验证知识本身的情况下创建和维护知识。最近关于长链推理(Long Chain-of-Thought reasoning)的研究已经展示了大规模语言模型(LLMs)在解决竞争性问题方面巨大的潜力，但它们的验证能力仍然很弱且尚未得到充分研究。在本文中，我们提出了Heimdall，这是一种长链推理验证的LLM，能够准确判断解决方案的正确性。通过纯粹的强化学习，我们在竞争性数学问题上的验证准确性从62.5%提升到了94.5%。通过重复采样的扩展，准确性进一步提高到97.5%。通过人工评估，Heimdall展示了令人印象深刻的泛化能力，成功检测了大多数具有挑战性的数学证明中的问题，而这些问题是训练期间未包含在内的。此外，我们提出了悲观验证(Pessimistic Verification)，以扩展Heimdall的功能，使其能够解决更大规模的问题。它会调用Heimdall来判断求解器模型的解决方案，并基于悲观原则，选择具有最少不确定性的最可能正确的解决方案。使用DeepSeek-R1-Distill-Qwen-32B作为求解器模型，悲观验证在AIME2025上的解题准确性在16倍计算预算下从54.2%提升到了70.0%，在更多计算预算下提升到了83.3%。使用更强的求解器Gemini 2.5 Pro，得分达到了93.0%。最后，我们构建了一个自动知识发现系统，这是一个三元系统，一个人提出问题，另一个提供解决方案，第三个验证解决方案。使用NuminaMath的数据合成工作为前两个组件，Heimdall有效地在数据集中识别出了有问题的记录，并揭示了几乎一半的数据存在缺陷，这有趣地与NuminaMath的最近消融研究结果相吻合。