清華大学チーム、AIの推論を検証可能にする代数世界モデルを提案

導入

AIが科学者のように推論するには、データを大量に集めるだけでは不十分だ。観測された現象から一般的な規則を抽出し、その規則が本当に成り立つのかを検証しなければならない。清華大学の姚期智氏と袁洋氏が率いる研究チームが提案した代数世界モデル（Algebraic World Model、AWM）は、インタラクティブな環境でこの流れを実現しようとする試みである。

現象の記録から世界のモデル化へ

ARC-AGI-3のようなベンチマークでは、AIに明確なルールや目標が与えられない。エージェントは実際に操作しながら、環境の仕組みを推測する。素材によれば、最先端モデルは観測結果を大量の記号的ルールに整理し、高いスコアを出せる場合がある。しかし、それは観測ノートに近い。何が起きたかは記録できても、背後にある仕組みを十分に説明できるとは限らない。

この違いは、タスクが不可能かどうかを判断するときに表れる。必要な最小手数より少ない手数しか与えられないステージでは、モデルが試行を続けたり、必要手数を誤って推定したりすることがある。ゲームなら効率の問題で済むが、現実の作業では、実行可能性や失敗理由の誤判定がより大きな問題につながる可能性がある。

AWMの仕組み

AWMは、環境内の対象、関係、操作を計算可能な代数世界として扱う。報告されている処理は、主に三段階からなる。

• 探索：環境を操作し、観測した規則を実行可能なPythonの仮説として表す。
• 洗練：新しい実験で仮説を検証、修正、統合し、より一般的な対象と規則にまとめる。
• 証明：重要な規則をLean 4の形式命題へ変換し、論理的に成立するかを機械的に確認する。

重要なのは、単に試行回数を増やすのではなく、世界のモデルを作り、そのモデルを検証する点だ。素材では、ある解なしステージについて、Opus 5.5を用いたAWMが二回の試行で現在の手数では解けないことを証明し、あと一手あれば成功できると判断したと説明されている。また、ARC-AGI-3の183ステージをすべてクリアし、平均行動数が人間ベースラインの43％だったとも報告されている。形式化されたモデルが、効率と説明可能性の双方を高める可能性を示す結果だが、評価条件を踏まえて解釈する必要がある。

抽象化を支える圏論

AWMは圏論、とりわけ極限と余極限から着想を得ている。簡単に言えば、一方は既存の概念と関係を組み合わせ、もう一方は異なる観測から共通する構造を見つける考え方だ。これらを反復することで、ばらばらなプログラム上の仮説を、より簡潔で一貫した推論可能なモデルへと整えられる。

意義と限界

AWMの意義は、AIにニュートンを模倣させることではない。「観測、仮説、実験、抽象化、証明」という科学的なループを、エージェントの設計に取り込もうとしている点にある。ゲーム、計画、実世界のインタラクションなど、なぜ成功し、なぜ失敗するのかを説明する必要がある課題で活用が期待できる。

ただし、形式的な証明が保証するのは、モデル内部での論理的一貫性である。探索で重要な規則を見落とせば、得られるのは局所的に正しい不完全な真理にとどまる。広い探索と継続的なモデル更新が、今後も不可欠になる。

出典：量子位