Meta、数学の自動形式化AI「AutoformBot」を公開
Meta AI Research
2026年5月29日 (金)
- •Meta AIが、数学の教科書を機械検証可能なコードへ変換するマルチエージェントフレームワーク「AutoformBot」を発表した。
- •同プロジェクトは、Lean 4の宣言45,000件以上と500,000行のコードを収めたライブラリ「Atlas」を構築した。
- •AutoformBotは、解析学や代数学など26冊の大学院レベルの数学教科書を対象に自動形式化処理を完了させた。
Meta AIの研究チームは2026年5月27日、数学の教科書にある非形式的な文章を機械検証可能なコードへ変換するシステム「AutoformBot」を発表した。このフレームワークは、形式検証ツールや依存関係を考慮したタスクスケジューリング、共同バージョン管理を備えた数千ものLLMエージェントを連携させ、精度の高い自動形式化を実現する。
研究チームは、解析学、代数学、位相幾何学、組合せ論、確率論など26冊のオープンアクセス教科書を対象に本手法を適用した。その結果、Lean 4の宣言45,000件以上とコード500,000行を収録したライブラリ「Atlas」が構築された。Lean 4は、形式的な数学証明を記述するために設計された関数型プログラミング言語である。
MetaはAutoformBotとAtlasをオープンソースとして公開した。今回の成果は、大学院レベルの数学を大規模に自動形式化することが技術的かつ経済的に可能であることを示しており、将来的な数学研究の自動検証への道を拓くものとなる。