[Codex, LEAN] 簡単に作れる擬似的なAI数学者を作ってみた [AI for Math] ~ サブゴール分解 → Lean検証 → 失敗ログ → 修正 を回すデモ ~

AI数学者 Hilbertシステムとは？

AIに数学を解かせるシステムとして、Hilbertというものがあります。
今回の記事では、このシステムを、簡単に擬似的に再現できるシステムのデモを行います。

Hilbertの論文はこちら： https://arxiv.org/abs/2509.22819

Hirbertのシステムの目的は、LLMを用いて、LEANという「数学の証明を検証できるプログラム」で解き切ることです。
これにより、LLMに数学をやらせるときの、「本当は証明できてないのに、証明できたと嘘をつく」という問題を回避できます！

このシステムは、いくつかのステップのループでできています。

• 証明にトライ

• →失敗したらもう少し小さなゴール(サブゴール)を作ってトライ！

• →失敗したらもう少し小さなゴール(サブゴール)を作ってトライ！

• →・・・

そして、このループごとに、LEANでできたところまでを検証していきます。
だんだんと、サブゴールをLEANにしたものや実験結果が溜まっていきます。

簡単で擬似的なHilbertシステムの概要:CodexとLEAN

今回、このシステムを、CodexとLEANで簡単に擬似的に作れるんではないかと、試してみました。

Codexというのは、ChatGPTを作ってるOpen AI社が出しているプログラムができるAIエージェントです。
Hirbeltシステムの「検証とサブゴール分解のループ」を Codexで回します。
（Hilbert は参考にした程度で、再現ではありません。Hilbertのループ要素だけ借りました。）

初期条件は、以下の画像です。

左側のチャットGPTみたいなのが、codexです。ここにチャットを打てば、勝手にプログラムしたり、ファイルが作られます。

右側は初期設定のファイルとプログラムです。
Question.leanには、解かせたい数学の問題が書かれています。miniF2Fという数学ベンチマーク の問題の１つである mathd_algebra_69 を解かせます。
agent.mdというファイルには、AIエージェントであるcodexにやってほしいことが書いてます。

めっちゃシンプルですね！本当にこれでできるのか、、、、。

解かせてみる実験の結果

Codexさんに、「さあ！agent.mdを読んで、問題を解いて！」とお願いしました。ChatGPTと会話するのとほぼ同じです。
数回やり取りした後の結果が、こちら

agent.mdは変わってませんが。
Question.leanには、回答がずらずらと記載されています！
experiment.mdにも、色々と試行錯誤の実験結果が描かれています。

出てきたコードは、実際に、LEANでの検証をパスしてます！すごい！

※ LEANできる人からしたら、lakeとかで検証してないじゃん！ってことですが、一応、人間側が、手動でleanコードをLEAN4 webで確認し、そのスクショをcodexに返して検証させてます。簡易デモなので許してください！

考察

考察1: Hilbertシステムの再現度〜今回のデモのシステムが優秀なのは手軽さ〜

Hilbertシステム自体は、もっと洗練されたシステムです。
問題はもっと大量にテストしてます。LEANでのコードの検証も人手ではなく、自動でlakeってやつでチェックしてます。サブゴール分解ももっと洗練させたシステムです。

ですが、専門家でない人が、とりあえず、手元で簡単に試せるのが、今回の、Codex+LEANのシステムかと思います。
プログラムとかしたことない人でも、数学解かせてみるか〜とかで、すぐに試せるのが今回のデモの良いところだと思います。

考察2: 数学以外の他の自動実験の領域にも使えるのでは？

Codex + LEANは、適切な問題が作れさえすれば、理論物理や暗号理論、計算系の生物学にも応用が可能なシステムだと思います。

また、Anthropicが出してる、codexに似てるClaudeなどのAIエージェントシステムは、一般的な機械である、例えばニンテンドースイッチとか、冷蔵庫とかにも原理的には入れられるため、物理実験もそのうちこの系統のシステムで簡単にできるようになるかもしれません。

考察3: 数学はこれで攻略されるのか？

このシステムはかなり優秀で、人間の思考を使わずに、実験が進むため、確かに、良さげです。

しかし、「LEANで問題文が書かれてないと厳しい」というのがネックだと思います。
ここに関しては、GoogleのDeepMind (googleのAIを作ったりしてる部門です)がformal-conjectureというオープンソースプロジェクトで、未解決問題をLEANで書くプロジェクトをやってます。
なお、当研究所 (IMP AIセキュリティ研究所)もこのプロジェクトに、いくつか貢献をしています。

「LEANで問題文が書かれている」というのは、実は結構ハードルが高く。数学も高度な概念になると、LEANで書くための元になる定義とか条件とかを揃えたり。問題文自体の解釈を国語の読解問題みたいに精密にやらないとLEANでは書けないので頑張ったりしないとダメです。その辺りがまだクリアされていません。

考察4: 数学の研究が変質するのか？

ポジティブな数学の変質が考えられます。
Hilbertシステムは、専門家じゃないと手が出せないレベルの完成度ですが。
今回の、Codexシステムは誰でもできます。
さらに、codexに吐かせた実験ノートなんかは、かなり価値が高く、論文だけでは伝わらないニュアンスなども残せます。
これにより、これまでの数学であった、「これまでの研究をまとめたノートを作る」「研究のニュアンスの説明」といった文化がより伝わりやすく、広がりやすくなるかと考えられます。

ネガティブな変質も考えられます。
AIが出してきた「問題文のLEANコード」自体の確認が大事であり、ここが間違ってると、システムが崩壊します。
問題の取り違えで、解けたと思ったのに解けなかった！みたいな事例は、最近、数学では頻発しているため、ここへの対策は今後の課題です。

補足

補足1: 問題文

今回採用した問題文は、このようになってます

正直、「え？25って答え言ってるじゃん」って思うのですが、本当にこれが、データセットまんまです。
人間相手なら、25列か？なんて聞かないですよね。
でも、このデータセットの問題は、AI数学系のベンチマークになってるのです。本当にこんなもんでいいのかなとは思いますが。

補足2: 人間が手作業で結果検証してるからHilbertシステムじゃない。自律じゃないですよね？

その通りですが、原理的には、codexにlakeのシステムとかも作らせられるはずです。
今回は、簡易的なデモなので、そこはカットしました。