論文の概要: Algebraic World Model: From Exploration to Proofs

• arxiv url: http://arxiv.org/abs/2610.40503v2
• Date: Fri, 30 Oct 2026 07:09:07 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-11-02 22:05:31.442131
• Title: Algebraic World Model: From Exploration to Proofs
• Title（参考訳）: 代数的世界モデル:探索から証明まで
• Abstract要約: 代数的世界モデル(Algebraic World Model)は、馴染みのない環境との相互作用を、形式的推論をサポートする明示的な数学的モデルに変える。 AWMは、探索軌道を超えても、ゴールが到達不可能であることを正式に証明することができる。 AWMは、ルールを検査し、段階的にテストできる解釈可能な数学的モデルを生成する。
• 参考スコア（独自算出の注目度）: 12.360653373668683
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: AI has made remarkable progress in mathematics, solving challenging problems with machine-checkable proofs in Lean, yet typically relying on predefined mathematical definitions and formal specifications. This raises a natural question: can it reason rigorously about an unknown world? We introduce the Algebraic World Model (AWM), a framework that turns interaction with unfamiliar environments into explicit mathematical models supporting formal reasoning. AWM explores the environment and develops executable Python hypotheses, continually testing and revising them against observations. It then structures these hypotheses into typed objects and shared rules, simplifies their structure through category-theory-guided transformations, and formalizes the resulting model in Lean 4 to prove reachability and impossibility. AWM can formally prove that a goal is unreachable, even beyond explored trajectories. On two impossible game levels, it constructs closed, kernel-checked Lean proofs excluding every legal winning sequence in all six runs, while Claude Opus 5.5 and GPT-6 Astra, equipped with coding tools, produce none in twelve baseline runs. Four of AWM's six initial bounds are correct, compared with one for Opus 5.5 and none for GPT-6 Astra; given only feedback that a cheaper win exists, AWM revises its rules and constructs new proofs, reaching six of six correct bounds. Moreover, AWM produces interpretable mathematical models whose rules can be inspected and tested step by step. Across all 25 public ARC-AGI-3 games, these models enable Lean to replay the winning trajectories of all 183 levels and generalize beyond observed play, predicting unseen transitions and detecting changes in game mechanics. With Claude Opus 5, AWM clears all levels with a score of 99.9, while its certified winning trajectories use only 43% of the human baseline's actions.
• Abstract（参考訳）: AIは、リーンのマシンチェック可能な証明で難しい問題を解くが、一般的には事前に定義された数学的定義と形式的な仕様に依存している。 これは自然の疑問を生じさせます。未知の世界について厳格に理屈を定めますか? 本稿では,代数的世界モデル(Algebraic World Model, AWM)を紹介する。 AWMは環境を調査し、実行可能なPython仮説を開発し、継続的にテストし、観察に対して修正する。 そして、これらの仮説を型付けされたオブジェクトと共有ルールに構造化し、カテゴリ理論に基づく変換を通じて構造を単純化し、結果のモデルをLean 4で形式化し、到達可能性と不可避性を証明します。 AWMは、探索軌道を超えても、ゴールが到達不可能であることを正式に証明することができる。 2つの不可能なゲームレベルでは、クロード・オプス 5.5 と GPT-6 アストラはコーディングツールを備えており、12のベースラインランに存在しない。 AWMの6つの初期限界のうちの4つはオプス 5.5 と GPT-6 アストラ に比較して正しいものであり、より安価な勝利が存在するというフィードバックしか与えられていないため、AWMはルールを変更して新しい証明を作成し、6つの正しい境界のうち6つに達する。 さらに、AWMは、段階的にルールを検査およびテストできる解釈可能な数学的モデルを生成する。 25のパブリックARC-AGI-3ゲーム全体で、これらのモデルはLeanが183レベルのすべての勝利軌跡をリプレイし、観察されたプレイを超えて一般化し、目に見えない遷移を予測し、ゲームのメカニックの変化を検出することを可能にする。 クロード・オプス5では、AWMは99.9のスコアで全てのレベルをクリアし、認定された勝利軌道は人間のベースラインの43%しか使用していない。

関連論文リスト

• Maestro: Agentic Formal Proof Development by Coordination [21.09901199432239]
  Maestroは、グローバルな調整を通じて障害を処理するリーンの証明ハーネスです。 エージェントが飽和していないすべてのベンチマークにおいて、各モデルのネイティブコーディングエージェントよりも多くのターゲットを証明している。 また、共有するベンチマークで発行されたすべての証明システムよりも優れています。
  論文  参考訳（メタデータ） (2026-10-19T07:21:10Z)
• Apodex Discovery: Reality Benchmarks and Environments for Evaluating and Building Discoverative Artificial Intelligence [86.61561123749011]
  Apodex Discovery(アポデックスディスカバリー)は、重度解法を用いて発見的AIを構築し評価するためのフレームワークである。 まず16のセクターで511の業界を調査し、423の高価値現実問題を集め、最初のリリースで20を選定した。 第二に、共通の環境-タスク-エピソード抽象化は、データ、ツール、制約、フィードバック、軌跡記録、中間成果物と最終提出物の検証を提供する。
  論文  参考訳（メタデータ） (2026-08-11T18:48:40Z)
• Can Open-Weight LLMs Produce Kernel-Verified Coq Proofs? A Pilot Study [0.20415910628419062]
  大規模言語モデル(LLM)は数学的証明に類似したテキストを生成することができるが、類似性は正確性を確立しない。 Coqのルールは、システムのどの証明ステップが受け入れられるかを定義する論理的フレームワークであるCalculus of Inductive Constructionsに基づいている。 このパイロット研究は、実際のCoqプロジェクトから派生したベンチマークであるCoqStoqから、同じ100の定理で6つのオープンウェイトLSMを評価した。
  論文  参考訳（メタデータ） (2026-08-05T21:29:12Z)
• Harnessing Code Agents for Automatic Software Verification [0.47154736035631406]
  大規模言語モデル(LLM)は、自動的に証明を生成することを約束するが、既存のアプローチは、固定された人間設計の証明戦略をシステムに結び付ける。 このような戦略を課すことは不要で制限的であることを示す。 レムマ全体を一般的なコードエージェントに手渡して、独自のアプローチを自由に選択し、検証ハーネスにラップすることは、シンプルでより効果的です。
  論文  参考訳（メタデータ） (2026-07-07T14:39:59Z)
• LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization [104.06650149974585]
  信頼性の高い研究レベルのLean AutoformalizationのためのマルチエージェントハーネスであるLeanMarathonを紹介します。 4つのコントラクトスコープエージェントがこの青写真を構築し、監査し、証明し、修復する。 我々は4つのErds問題にまたがる最近の2つの研究論文でLeanMarathonを評価した。
  論文  参考訳（メタデータ） (2026-06-03T20:09:39Z)
• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
  我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。 まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。 次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。 最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
  論文  参考訳（メタデータ） (2025-02-11T15:27:35Z)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。 この合成データセットでDeepSeekMath 7Bモデルを微調整します。 我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
  論文  参考訳（メタデータ） (2024-05-23T09:03:42Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。 本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。 我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
  論文  参考訳（メタデータ） (2020-10-06T15:47:53Z)

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

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