論文の概要: PhysProver: Advancing Automatic Theorem Proving for Physics

• arxiv url: http://arxiv.org/abs/2601.15737v1
• Date: Thu, 22 Jan 2026 08:05:32 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-01-23 21:37:20.537744
• Title: PhysProver: Advancing Automatic Theorem Proving for Physics
• Title（参考訳）: PhysProver:物理のための自動理論証明の強化
• Authors: Hanning Zhang, Ruida Wang, Rui Pan, Wenyuan Wang, Bingxu Meng, Tong Zhang,
• Abstract要約: 本稿では、物理学領域における形式定理の証明を強化するための最初のアプローチを提案する。 PhysLeanからサンプリングされた定理と、予想に基づく形式データ生成パイプラインによって生成されるデータで構成されている。 トレーニングパイプラインでは、強力なオープンソースの数学的定理証明器であるDeepSeek-Prover-V2-7Bを活用し、RLVR(Reinforcement Learning with Verifiable Rewards)を使用して、モデルのPhysProverをトレーニングします。
• 参考スコア（独自算出の注目度）: 17.074001092418793
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.
• Abstract（参考訳）: 検証可能な言語とLLMの組み合わせは、定理証明のための厳密な基礎を提供するため、数学的および計算機科学のコミュニティに大きな影響を与えている。 この分野の最近の進歩は、LLMの自然言語能力にアプローチするために形式的数学的推論の境界を推し進める基礎モデルと洗練されたエージェントシステムを提供する。 しかし、公式な物理学の推論にはほとんど注意が向けられておらず、同様の問題解決や定理証明のフレームワークにも大きく依存している。 この問題を解決するために,本論文では,物理学領域における形式的定理の証明を促進するための最初のアプローチとして,我々の知識を最大限に活用する。 タスクのために専用のデータセットPhysLeanDataを作成します。 PhysLeanからサンプリングされた定理と、予想に基づく形式データ生成パイプラインによって生成されたデータで構成されている。 トレーニングパイプラインでは、強力なオープンソースの数学的定理証明器であるDeepSeek-Prover-V2-7Bを活用し、RLVR(Reinforcement Learning with Verifiable Rewards)を使用して、モデルのPhysProverをトレーニングします。 総合的な実験では、$\sim$5Kのトレーニングサンプルだけで、PhysProverは複数のサブドメインで2.4.%の改善を実現している。 さらに, 物理領域を超えた非自明な一般化と公式数学能力の向上を示すMiniF2F-Testベンチマークでは, 1.3 %のゲインを観測した。 その結果,本手法の有効性と有効性を強調し,数学的領域以外の形式的プロバーを拡張するためのパラダイムを提供する。 さらなる研究を促進するため、私たちはデータセットとモデルの両方をコミュニティにリリースします。

関連論文リスト

• Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience [38.07918040429112]
  大規模エージェント強化学習を用いて学習した公式な定理証明モデルである textbfSeed-Prover 1.5 を提案する。 本システムを用いて,Patnam 2025の12問題のうち,textbf11を9時間以内に解決した。
  論文  参考訳（メタデータ） (2025-12-19T06:19:55Z)
• Evaluating Frontier LLMs on PhD-Level Mathematical Reasoning: A Benchmark on a Textbook in Theoretical Computer Science about Randomized Algorithms [14.853721511192736]
  大規模言語モデル(LLM)は、自動数学的推論と科学的発見の突破口となった。 GP-5-Thinking、Gemini-3-Pro、Claude-Sonnet-4.5-Thinking、Grok-4の4つのフロンティアモデルのベンチマークを示す。 上位モデルの精度は高いが,他のモデルでは一貫性が著しく低下していることがわかった。
  論文  参考訳（メタデータ） (2025-12-16T00:34:55Z)
• CMPhysBench: A Benchmark for Evaluating Large Language Models in Condensed Matter Physics [71.42168240638462]
  CMPhysBenchは、凝縮物質物理学における大規模言語モデルの習熟度を評価するように設計されている。 以上の結果から,最高モデルであるGrok-4でさえ,CMPhysBench上での平均SEEDスコアが36点,精度が28%であった。
  論文  参考訳（メタデータ） (2025-08-25T15:32:22Z)
• Can Theoretical Physics Research Benefit from Language Agents? [50.57057488167844]
  大規模言語モデル(LLM)は、様々な領域にわたって急速に進歩しているが、理論物理学研究への応用はまだ成熟していない。 このポジションペーパーは、LLMエージェントが、ドメイン知識やツールボックスと適切に統合された場合、理論的、計算的、応用物理学を加速するのに役立つと主張している。 マルチモーダルデータを処理し、検証可能な仮説を提案し、設計実験を行う物理特殊化LSMを構想する。
  論文  参考訳（メタデータ） (2025-06-06T16:20:06Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。 DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。 我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
  論文  参考訳（メタデータ） (2025-05-29T17:59:39Z)
• LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
  フォーマルな定理証明のための新しい生涯学習フレームワークであるLeanAgentを紹介する。 LeanAgentは継続的に一般化し、拡張可能な数学的知識を改善します。 これは23のリーンリポジトリにわたる155の定理の正式な証明を生成する。
  論文  参考訳（メタデータ） (2024-10-08T17:11:24Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。