核心发现
方法论
本文提出了PhysProver，结合了强化学习与可验证奖励（RLVR）和专门为物理定理证明设计的数据集PhysLeanData。使用DeepSeek-Prover-V2-7B作为基础模型，通过RLVR进行训练，显著提升了物理领域的定理证明能力。
关键结果
- PhysProver在多个物理子领域实现了2.4%的整体提升，使用约5K的训练样本，展示了其在物理定理证明中的有效性。
- 在MiniF2F-Test基准测试中，经过物理训练后，模型在非物理领域也获得了1.3%的提升，显示出跨领域的泛化能力。
- 通过实验验证，PhysProver在粒子与弦理论等复杂领域中表现出色，超越了现有的数学定理证明模型。
研究意义
PhysProver的提出填补了物理定理证明领域的空白，为物理学的形式化推理提供了新的工具。其方法不仅提升了物理领域的定理证明能力，还在数学推理中展示了潜在的应用价值，推动了跨领域的研究进展。
技术贡献
PhysProver通过结合RLVR和物理专用数据集，首次在物理定理证明中应用了强化学习方法，提供了新的理论保证和工程可能性。与现有数学定理证明方法相比，PhysProver展示了在物理领域的独特优势。
新颖性
PhysProver是首个专注于物理定理证明的模型，利用RLVR和PhysLeanData，突破了传统数学定理证明的局限，首次实现了物理领域的形式化推理。
局限性
- PhysProver在处理复杂物理定理时仍然面临挑战，尤其是在数据集规模有限的情况下。
- 模型在某些特定领域的泛化能力可能不足，需要进一步优化。
未来方向
未来的研究方向包括扩展数据集规模，优化模型的泛化能力，以及探索更多物理领域的应用。社区可以基于此模型进行更广泛的研究和应用。
AI 总览摘要
物理定理证明长期以来一直是一个未被充分探索的领域，尽管其在物理学中的重要性不言而喻。现有的方法主要集中在数学定理证明上，缺乏对物理领域的专门关注。PhysProver的出现填补了这一空白，通过结合RLVR和专用数据集PhysLeanData，显著提升了物理定理证明的能力。
PhysProver利用DeepSeek-Prover-V2-7B作为基础模型，通过RLVR进行训练，展示了在多个物理子领域的出色表现。实验结果显示，PhysProver在物理领域的定理证明中实现了2.4%的提升，并在MiniF2F-Test基准测试中获得了1.3%的跨领域提升。
尽管PhysProver在物理定理证明中取得了显著进展，但仍然面临数据集规模和模型泛化能力的挑战。未来的研究将致力于扩展数据集和优化模型，以进一步提升其在物理和数学领域的应用潜力。
深度分析
研究背景
近年来，形式化推理在数学和计算机科学领域取得了显著进展，尤其是在大语言模型（LLMs）的推动下。尽管如此，物理领域的形式化推理仍然是一个未被充分探索的领域。物理学依赖于严谨的数学基础和形式化推导，这为形式化推理提供了一个自然的扩展方向。
核心问题
物理定理证明面临的核心问题是缺乏专用的数据集和方法，导致现有的数学定理证明模型在物理任务中表现不佳。物理学的复杂性和多样性使得形式化推理变得更加困难。
核心创新
PhysProver的核心创新在于首次将RLVR应用于物理定理证明，结合专用数据集PhysLeanData，提升了物理领域的推理能力。与传统数学定理证明方法相比，PhysProver展示了在物理领域的独特优势。
方法详解
- �� 使用PhysLeanData构建训练集，包含物理定理和合成引理。
- �� 采用DeepSeek-Prover-V2-7B作为基础模型。
- �� 通过RLVR进行训练，利用Lean验证器提供的奖励信号。
- �� 进行自我进化训练，提升模型的物理推理能力。
实验设计
实验设计包括使用PhysLeanData作为训练集，并在MiniF2F-Test基准测试上进行评估。比较基线包括现有的数学定理证明模型和专有系统。使用pass@16作为主要评估指标。
结果分析
PhysProver在多个物理子领域实现了2.4%的提升，并在MiniF2F-Test基准测试中获得了1.3%的跨领域提升。实验结果显示，PhysProver在粒子与弦理论等复杂领域中表现出色。
应用场景
PhysProver可用于物理学的形式化推理，尤其是在复杂物理定理的自动证明中。其方法也可应用于数学推理，展示了跨领域的应用潜力。
局限与展望
尽管PhysProver在物理定理证明中取得了显著进展，但仍然面临数据集规模和模型泛化能力的挑战。未来的研究将致力于扩展数据集和优化模型。
通俗解读 非专业人士也能看懂
想象你在厨房里做饭。你有一个食谱（PhysLeanData），这就像是你的数据集。你有一个厨师助手（PhysProver），他会根据食谱来帮助你做饭。这个助手非常聪明，他会根据你的指示（RLVR）来调整他的做法，以确保每道菜都完美无缺。通过不断练习，他不仅能做出美味的菜肴，还能在其他厨房（数学领域）中展示他的厨艺。
简单解释 像给14岁少年讲一样
想象一下，你在玩一个关于物理的电子游戏。这个游戏有很多关卡，每个关卡都有不同的物理难题。PhysProver就像是你的游戏角色，他有一个特别的技能，可以通过学习和训练来解决这些难题。每当他解决一个难题，他就会变得更强大，不仅能在物理关卡中表现出色，还能在数学关卡中大显身手。是不是很酷？
术语表
PhysProver (物理证明者)
一个专注于物理定理证明的模型，结合了RLVR和PhysLeanData。
用于提升物理领域的定理证明能力。
RLVR (强化学习与可验证奖励)
一种结合强化学习和可验证奖励信号的方法，用于训练模型。
在PhysProver中用于提升物理推理能力。
PhysLeanData (物理精简数据集)
专为物理定理证明设计的数据集，包含物理定理和合成引理。
作为PhysProver的训练数据。
DeepSeek-Prover-V2-7B (深度搜索证明者)
一个强大的开源数学定理证明模型，用于物理定理证明的基础。
作为PhysProver的基础模型。
MiniF2F-Test (小型面对面测试)
一个用于评估形式化数学推理能力的基准测试。
用于评估PhysProver的跨领域泛化能力。
开放问题 这项研究留下的未解疑问
- 1 如何在有限的数据集上进一步提升物理定理证明的准确性？现有方法在数据集规模有限时表现不佳，需要更有效的数据增强策略。
- 2 如何优化模型的泛化能力，使其在更多物理领域中表现出色？现有方法在某些领域的泛化能力不足。
应用场景
近期应用
物理定理自动证明
PhysProver可用于自动化物理定理证明，帮助研究人员验证复杂物理理论。
远期愿景
跨领域形式化推理
PhysProver的技术可应用于其他科学领域的形式化推理，推动跨学科研究。
原文摘要
The combination of verifiable languages and LLMs has significantly influenced both the mathematical and computer science communities because it provides a rigorous foundation for theorem proving. Recent advancements in the field provide foundation models and sophisticated agentic systems pushing the boundaries of formal mathematical reasoning to approach the natural language capability of LLMs. However, little attention has been given to the formal physics reasoning, which also heavily relies on similar problem-solving and theorem-proving frameworks. To solve this problem, this paper presents, to the best of our knowledge, the first approach to enhance formal theorem proving in the physics domain. We compose a dedicated dataset PhysLeanData for the task. It is composed of theorems sampled from PhysLean and data generated by a conjecture-based formal data generation pipeline. In the training pipeline, we leverage DeepSeek-Prover-V2-7B, a strong open-source mathematical theorem prover, and apply Reinforcement Learning with Verifiable Rewards (RLVR) to train our model PhysProver. Comprehensive experiments demonstrate that, using only $\sim$5K training samples, PhysProver achieves an overall 2.4\% improvement in multiple sub-domains. Furthermore, after formal physics training, we observe 1.3\% gains on the MiniF2F-Test benchmark, which indicates non-trivial generalization beyond physics domains and enhancement for formal math capability as well. The results highlight the effectiveness and efficiency of our approach, which provides a paradigm for extending formal provers outside mathematical domains. To foster further research, we will release both our dataset and model to the community.