人工知能はほぼ毎週、新しい数学の難問を解決しているように感じる。先月だけで、OpenAIは719本の原稿を発表し、その分野で最も難しい問題のいくつかを解決したと主張した。コンピュータによる検査ですら誤りを犯す可能性がある。長年にわたりAIによるゴミコンテンツを経験した後、数学が次に影響を受ける分野になるのではないかと疑問を抱かずにはいられない。
AxiomMathは、速度を落とすのではなく、より堅固な基盤を構築することで、このような運命を回避できる。この16億ドルの評価額を持つスタートアップは、AIエージェントがソフトウェアを記述し、最終的には科学研究に従事できるよう、検証済みの基盤層を構築することを目指している。
水曜日、同社は、Stacks Projectを正式に検証したことを発表しました。これは人間が書き下ろした最大級の数学的成果の一つです。数学者たちは通常、Stacksを非常に高く評価しています。コロンビア大学の数学者ピーター・ウォイトは、これを「他に類を見ない」と評し、このプロジェクトを20世紀に数学の基礎から再構築した有名なBourbakiシリーズに例えました。
Woitのコロンビアの同僚であるJohan de Jongは2005年、オープンソースの参照資料としてStacks Projectを開始しました。以来、数学者たちは大学レベルの代数から、代数、幾何、数論などの分野における最先端の思想に至るまで、このプロジェクトに貢献し続けています。
同社のAIエージェント群は、約7,654ページのデータベースを、コンピューターで検査可能な約1,600万行のコードに翻訳しました。
形式化数学の目的は、その基盤構造が信頼できるようにすることです。数学者は、証明をLeanというプログラミング言語でコードに書き直し、proof assistantと呼ばれるプログラムによって一行ずつチェックします。証明が通過すれば、数学者はその証明が論理的に成立していると信頼できます。
エンジニアも、チップ設計の妥当性を確認するために同じ考え方、つまり形式的検証を使用している。フランスの研究者は、これを用いて家庭補助金の計算ソフトウェアのバグを発見した。
Stacks Projectのようなプロジェクトでは、定理を一つずつ確認することは仕事の一部にすぎません。Stacks内の定理と定義は互いに結びついており、それぞれが以前の内容を基に構築されています。家系図のように、Stacks内の多くの結果はより前の結果に遡ることができます。
この相互関連性により、Axiomは当初、このプロジェクトが実現可能かどうかを確信できませんでした。チームは約1,600万行のLeanコードにおいて、すべての接続を完全に維持しなければなりませんでした。
AxiomのCEOであるカリナ・ホンはTechCrunchに次のように語った。「規模が大きく、かつ精密であるという二つは現実には通常、両立しない。［Stacks］は数学的基盤を構成する数学的成果の集合である。あなたは［定理］同士が一貫していることを望むべきであり、パラドックスのようにはならないようにするべきだ。また、これらの定義同士も互いに矛盾しないようにすべきだ。」
この25歳のCEOは、スタンフォード大学の数学博士課程を中退し、2025年3月に同社を設立しました。今年3月、AxiomはMenlo Venturesが主導する2億ドルのAラウンド資金調達を実施しました。
ホンは「当時、vibe codingがStacksの美しさを維持できるかどうかは確信がありませんでした。」
このプロジェクトを完了するために、チームはエージェントに柔軟な構造を設定し、それらを並列で実行しました。Axiom テクノロジーチームのアシュヴィン・スワミナサンは、「Stacks の場合、私たちは階層を設定しましたが、各エージェントが具体的に何をすべきかを完全に規定するような階層ではありません。エージェントは自らタスクを見つけ出し、並列処理可能なものを識別します。」
Axiom は独自のモデルを訓練し、数学に強くなるようにしました。Hong は、このアプローチが他のほとんどの検証型スタートアップが取っていない方法であると述べました。当初、チームは内部の Lean 専門家に頼って、エージェントが人間のような判断基準を形成するよう教えました。しかし時間の経過とともに、Hong によると、これらのエージェントは自らその判断力を身につけました。
この成果は、形式化数学における最大の空白の一つを埋めました。スワミナサンは、「すでに形式化された数学の内容を見ると、巨大なブラックホールが存在することがわかります。そのブラックホールは代数幾何をカバーしています。」
スワミナタンは、これまで代数幾何の新しい作業をLeanで検証したい研究者は、ほとんど利用可能な基盤がなかったと述べた。「今や、彼らにはそれがある。」
Axiomは、検証されたすべての結果が積み木となり、未来の証明が数学をゼロから再構築するのではなく、すでに検証された数学の上に構築できると主張している。UCLAの数学者でフィールズ賞受賞者であるTerence Taoは、これをより簡潔に「形式化された証明を多く持てば、より多くの形式化証明を生み出せる」と要約している。
Axiomのターゲットは数学者だけではありません。開発者は長年にわたり、自分のコードにバグやセキュリティ上の脆弱性が含まれていないことを確保しようと努力してきました。AIエージェントがますます多くのソフトウェアを書くようになるにつれて、この問題はさらに大きくなります。
Axiomにベットする。将来のソフトウェアは、現在のStacksのように検証された基盤の上に構築される必要がある。
スワミナタンは、「数学はこうしたものを構築し始める分野であり、移転可能なスキルであると考えています。エージェントは私たちのコードを読み取り、理解し、その上に新しいインフラを構築できます。Leanを用いて形式化したものが、今やエージェントが基盤として構築できる基礎となっています。」
AxiomがStacksを構築する方法——並列で作業し、自らタスクを選択する——は、Hongが将来の多くのAI作業のあり方として予想するものである。彼女は、AIエージェントがゴミコンテンツを生成しないように、構造化され再利用可能な知識ベースが必要だと考えている。
ホンは次のように述べています。「エージェントには、継続的に構築し、最先端を押し広げられる再利用可能なリポジトリを用意してほしい。最初から劣悪なエンジニアリング選択によってゴミを詰め込んでしまうと、その境界を拡張するのは難しくなる。」
ホンはこの方法に非常に自信を持っており、公開で挑戦状を叩きつけた。「私はあらゆるプログラミング企業に、この規模の形式化作業をやってみるよう公開で挑戦します。」