PhysProver: Advancing Automatic Theorem Proving for Physics
本文介绍了 PhysProver，这是首个通过使用带有可验证奖励的强化学习在专用数据集上训练 DeepSeek-Prover-V2 模型，从而增强物理领域形式化定理证明的框架，并在物理和通用数学领域均实现了显著的性能提升。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你拥有一个才华横溢、超高智商的机器人，它是解决用一种非常严格、计算机可读的语言——Lean 所编写的数学谜题的大师。这个机器人可以被称为“MathBot”，它在证明关于数字、形状和逻辑的定理方面极其出色。它阅读了数百万本数学书籍，并能解决奥林匹克级别的难题。
然而，有一个问题：MathBot 非常不擅长物理。
如果你要求它证明一个关于重力如何运作或粒子如何碰撞的定理，它会感到困惑。它试图使用它的数学技巧，但物理学有它自己的特殊规则、词汇和“风格”，而机器人并没有学习过这些。这就像是要求一位世界级的国际象棋选手突然去玩围棋；他们知道策略的规则，但他们并不了解这项新游戏的具体棋子或棋盘布局。
问题所在：缺失的字典
这篇论文的作者意识到，虽然我们已经构建了如此出色的数学机器人，但我们还没有教会它们如何使用“正式的物理语言”。物理学高度依赖数学，但它是一种不同的方言。机器人需要一本新的字典和一套专门针对物理的练习题。
解决方案：PhysProver（物理专家机器人）
团队创建了一个名为 PhysProver 的新系统。你可以把它想象成把 MathBot 拿过来，给它进行了一场极其严格的物理速成班。
他们是如何做到的，以下是分解后的简单步骤：
1. 构建教科书（数据集）
首先，他们需要一本教科书。他们不仅仅是编写新问题；他们从一个名为 PhysLean 的库中挖掘出了旧的、真实的物理证明。
- 种子（The Seed）： 他们从大约 3,000 个已经用 Lean 编写的真实物理定理开始。
- 扩张（The Expansion）： 为了获得足够的练习材料，他们使用了一个超级聪明的 AI（Claude）基于旧有的问题发明了新的物理问题。这就像一位老师看着一道数学题并问道：“如果我们改变这个数字会怎样？如果我们更换这个变量会怎样？”
- 过滤（The Filter）： 并非所有发明的题目都是好的。有些是胡言乱语。他们使用了一个“语法检查器”（Lean 编译器）来剔除任何在语法上错误的题目。然后，他们使用其他 AI 机器人尝试去解决这些题目。如果一个机器人无法证明它，说明这个问题太难或者本身有误，所以他们也将这些题目丢弃了。
- 结果： 他们最终得到了一本包含约 5,500 个高质量物理问题 的精简“教科书”。
2. 训练方法（“尝试、失败、学习”循环）
通常，要教一个机器人，你会展示答案并说：“记住这个。”作者尝试了这种方法（称为监督微调/Supervised Fine-Tuning），但实际上这让机器人的表现变得更差了。这就像是强迫机器人死记硬背一本字典，却不理解如何使用其中的单词。
相反，他们使用了一种叫做 带有可验证奖励的强化学习（RLVR） 的方法。
- 游戏： 他们给机器人一个物理问题。
- 尝试： 机器人尝试编写一个证明过程。
- 判定： Lean 计算机检查该证明。
- 如果证明是正确的，机器人会获得一个 金星 (+1)。
- 如果证明是错误的，它会得到 零 (0)。
- 学习： 机器人不仅仅是死记硬背答案。它学会了将“金星”与导致正确证明的具体步骤联系起来。它学会了避开那些导致“零”的步骤。这就像一只狗学习到坐下可以得到零食，而跳跃则什么也得不到。
3. 结果：物理专家
经过这种训练，这个机器人（现在被称为 PhysProver）接受了测试。
- 在物理方面： 它在解决物理问题方面比原始的 MathBot 有了显著进步。它在不同物理主题（如量子力学和相对论）上提升了约 2.4%。
- 在数学方面（惊喜）： 尽管它只接受了物理训练，但它在数学方面也变得稍微好了一点！它在标准数学测试中提升了 1.3%。作者认为，学习物理严密的结构帮助机器人更好地理解了数学的整体结构。
核心启示
这篇论文表明，你不需要一个庞大、昂贵的超级计算机来教机器人一个新的科学领域。你只需要一小组高质量的示例和一个严格的检查答案的方法。
通过将物理视为一个具有明确规则的游戏（计算机会对每一个动作给出“是”或“否”的反馈），他们教会了一个通用的数学机器人如何成为一名物理专家。这证明了我们可以教 AI 处理复杂的科学推理，不仅是通过喂给它更多的数据，更是通过教它如何验证自己的工作。
简而言之： 他们把一个数学天才带到了物理特训营，并配了一位严格的裁判，最后把它变成了一个物理专家，而且比以前更擅长数学了。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。