Axiom、Stacks ProjectをLeanで機械検証可能な形に

Axiom Mathは、代数幾何学の主要なオープンソース参考資料であるStacks Projectを、機械検証可能な形にしたと発表した。この形式化では、同プロジェクトの数学を約1600万行のLeanコードに変換し、証明検証プログラムが一つひとつ確認する。Axiomによると、研究者やAIエージェントは、この成果をつながりのあるライブラリとして利用し、新たな形式証明を組み立てられる。

ページ数については、出典によって若干の差がある。TechCrunchは約7,654ページと報じている一方、Axiomは約7,500ページとしている。元となる参考資料は、コロンビア大学の数学者Johan de Jongが2005年に立ち上げ、その後20年にわたって数学者たちが拡充してきた。Axiomの取り組みは既存の研究成果を形式化したものであり、AIエージェントが基礎となる数学を独自に発見したという意味ではない。

つながりのあるライブラリが重要な理由

証明ライブラリの価値は、個々の定理が検証済みであることだけではない。その後の証明で、それらの定理や依存関係を再利用できる点にもある。Axiomによると、Stacks Projectの恒久的なタグを保持し、Leanの宣言を原文の対応箇所と結びつけた。同社のウェブサイトでは、本文とコードを並べて表示し、結果同士の依存関係もたどれる。

これは特に代数幾何学で重要だ。証明が可換代数、スキーム、層、コホモロジーなど、複数分野にまたがる考え方の長い連鎖に依存することがあるためだ。Axiomによると、今回の公開以前は、現代代数幾何学を形式化するためのLeanの基盤は研究者にとってかなり限られていた。同社のライブラリは、プロジェクトごとに基礎部分を一から形式化せずに済む出発点となる。

今後の証明やソフトウェアの基盤に

Axiomによると、同社のエージェントは並行して作業し、何千もの定理を翻訳、証明、統合した。TechCrunchは、エージェントが取り組む課題を見つけられるよう、同社が大まかな枠組みを与えたと報じている。またAxiomは、数学に特化した独自モデルも訓練したという。同社は、完成したライブラリを形式化された数学の統合型・再利用可能ライブラリとしては最大だとしているが、これはAxiomによる今回の成果の位置づけだ。

同様の検証手法は、チップ設計やソフトウェア検証などの分野でも使われている。Axiomは、再利用できる検証済みの基盤があれば、AIエージェントがコードを書く量を増やすなかで、より信頼性の高いシステム構築に役立つと主張する。ただし今回検証されたのは、形式化されたStacks Projectであり、AIシステムが今後生み出すあらゆる数学的主張やソフトウェアではない。