論文の概要: Lean4Physics: Comprehensive Reasoning Framework for College-level Physics in Lean4
- arxiv url: http://arxiv.org/abs/2510.26094v1
- Date: Thu, 30 Oct 2025 03:09:40 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-10-31 16:05:09.637806
- Title: Lean4Physics: Comprehensive Reasoning Framework for College-level Physics in Lean4
- Title（参考訳）: Lean4Physics: Lean4におけるカレッジレベルの物理学のための総合的な推論フレームワーク
- Authors: Yuxin Li, Minghao Liu, Ruida Wang, Wenzhao Ji, Zhitao He, Rui Pan, Junming Huang, Tong Zhang, Yi R. Fung,
- Abstract要約: 大学レベルの物理学問題に対する包括的な推論フレームワークである**Lean4PHYS*をLean4で紹介する。
**Lean4PHYS*には、Lean4の正式な物理推論のためのカレッジレベルのベンチマークである*LeanPhysBench*が含まれている。
コミュニティ主導のレポジトリである*PhysLib*も紹介する。
- 参考スコア（独自算出の注目度）: 17.8194025216225
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We present **Lean4PHYS**, a comprehensive reasoning framework for college-level physics problems in Lean4. **Lean4PHYS** includes *LeanPhysBench*, a college-level benchmark for formal physics reasoning in Lean4, which contains 200 hand-crafted and peer-reviewed statements derived from university textbooks and physics competition problems. To establish a solid foundation for formal reasoning in physics, we also introduce *PhysLib*, a community-driven repository containing fundamental unit systems and theorems essential for formal physics reasoning. Based on the benchmark and Lean4 repository we composed in **Lean4PHYS**, we report baseline results using major expert Math Lean4 provers and state-of-the-art closed-source models, with the best performance of DeepSeek-Prover-V2-7B achieving only 16% and Claude-Sonnet-4 achieving 35%. We also conduct a detailed analysis showing that our *PhysLib* can achieve an average improvement of 11.75% in model performance. This demonstrates the challenging nature of our *LeanPhysBench* and the effectiveness of *PhysLib*. To the best of our knowledge, this is the first study to provide a physics benchmark in Lean4.
- Abstract（参考訳）: 大学レベルの物理学問題に対する包括的な推論フレームワークである**Lean4PHYS*をLean4で紹介する。
関連スポンサーコンテンツ * *Lean4PHYS* には、Lean4の正式な物理学推論のための大学レベルのベンチマークである *LeanPhysBench* が含まれている。
物理学における形式的推論のための確固たる基盤を確立するために、基礎単位系と公式な物理学的推論に不可欠な定理を含むコミュニティ主導のリポジトリである *PhysLib* も導入する。
我々は、**Lean4PHYS*で作成したベンチマークとLean4リポジトリに基づいて、主要なエキスパートであるMath Lean4 Proversと最先端のクローズドソースモデルを使用してベースライン結果を報告し、DeepSeek-Prover-V2-7Bのパフォーマンスはわずか16%、Claude-Sonnet-4は35%に過ぎなかった。
また、我々の*PhysLib*はモデル性能の11.75%の平均的な改善を達成できることを示す詳細な分析も行います。
これは、我々の*LeanPhysBench*と*PhysLib*の有効性の難しさを示しています。
私たちの知る限りでは、Lean4で物理学ベンチマークを提供する最初の研究です。
関連論文リスト
- PhysProver: Advancing Automatic Theorem Proving for Physics [17.074001092418793]
本稿では、物理学領域における形式定理の証明を強化するための最初のアプローチを提案する。
PhysLeanからサンプリングされた定理と、予想に基づく形式データ生成パイプラインによって生成されるデータで構成されている。
トレーニングパイプラインでは、強力なオープンソースの数学的定理証明器であるDeepSeek-Prover-V2-7Bを活用し、RLVR(Reinforcement Learning with Verifiable Rewards)を使用して、モデルのPhysProverをトレーニングします。
論文 参考訳（メタデータ） (2026-01-22T08:05:32Z) - 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) - PhysUniBench: An Undergraduate-Level Physics Reasoning Benchmark for Multimodal Models [69.73115077227969]
大規模言語モデル(MLLM)の推論能力の評価と改善を目的とした大規模ベンチマークであるPhysUniBenchを提案する。
PhysUniBenchは、3,304の物理問題から成っている。
ベンチマークの構成には、複数のロールアウト、専門家レベルの評価、解決が容易な問題の自動フィルタリング、そして5段階の難易度グレーディングシステムを含む、厳格な多段階プロセスが含まれていた。
論文 参考訳（メタデータ） (2025-06-21T09:55:42Z) - SeePhys: Does Seeing Help Thinking? -- Benchmarking Vision-Based Physics Reasoning [95.2886065291234]
物理問題に基づく推論のための大規模マルチモーダルベンチマークである SeePhys を提示する。
このベンチマークは、物理学の分野にまたがる7つの基本的な領域をカバーし、21のカテゴリの非常に異質なダイアグラムを取り入れている。
最も先進的な視覚推論モデル(例えばGemini-2.5-proやo4-mini)でさえ、ベンチマークで60%未満の精度を実現している。
論文 参考訳（メタデータ） (2025-05-25T11:28:34Z) - PhyX: Does Your Model Have the "Wits" for Physical Reasoning? [49.083544963243206]
既存のベンチマークでは、物理的な推論という、インテリジェンスの重要な側面を捉えられません。
視覚シナリオにおける物理基底推論のモデルキャパシティを評価するために設計された,最初の大規模ベンチマークであるPhyXを紹介する。
論文 参考訳（メタデータ） (2025-05-21T18:33:50Z) - PhysReason: A Comprehensive Benchmark towards Physics-Based Reasoning [36.193595420239845]
1200プロブレムの大規模言語モデル評価ベンチマークであるPhysReasonを提案する。
問題は平均8.1の解ステップが必要で、ハードは15.6である。
Deepseek-R1、Gemini-2.0-Flash-Thinking、o3-mini-highといったトップパフォーマンスモデルは、回答レベルの評価で60%以下を実現している。
論文 参考訳（メタデータ） (2025-02-17T17:24:14Z) - UGPhysics: A Comprehensive Benchmark for Undergraduate Physics Reasoning with Large Language Models [39.917074900737575]
大規模言語モデル(LLM)は、複雑な推論タスクを解く際、顕著な能力を示した。
物理学の推論の領域は、非常に少ない注意を払われたユニークな課題を提示する。
既存のベンチマークは、学部レベルの物理学の広さと深さでLLMの能力を評価するのに不足することが多い。
論文 参考訳（メタデータ） (2025-02-01T06:42:02Z) - Physics Reasoner: Knowledge-Augmented Reasoning for Solving Physics Problems with Large Language Models [41.88825441287559]
既存の大規模言語モデル(LLM)は、知識の不足や誤った知識アプリケーションのために頻繁に失敗する。
LLMを用いて物理問題を解くための知識強化フレームワークである物理推論器を提案する。
物理学的な問題を考えると、物理学的推論は問題解析、公式検索、ガイド付き推論という3つの段階を通して解決する。
経験的に、物理推論器は知識不足と不正確な応用の問題を緩和し、SciBenchの最先端性能を平均精度5.8%で達成した。
論文 参考訳（メタデータ） (2024-12-18T12:33:50Z) - PhysGame: Uncovering Physical Commonsense Violations in Gameplay Videos [66.09921831504238]
ゲームプレイビデオにおける物理コモンセンス違反を評価するための先駆的ベンチマークとしてPhysGameを提案する。
以上の結果から,現在のオープンソースビデオLLMのパフォーマンスは,プロプライエタリビデオよりも大幅に遅れていることが明らかとなった。
このデータセットに基づいて,PhysVLMを物理知識強化ビデオLLMとして提案する。
論文 参考訳（メタデータ） (2024-12-02T18:47:25Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。