Axiom Math、数学にAIスロップを入れないことを目指す

評価額16億ドルのスタートアップAxiom Mathは、人間が書いた最大級の数学ライブラリの一つであるStacksプロジェクトを形式的に検証した。AIエージェントを用いて7,654ページを約1,600万行のコンピュータ検証可能なLeanコードに翻訳した。形式的検証はチップ設計やソフトウェアデバッグと同様の手法で、証明アシスタントが各行をチェックすることで論理的健全性を保証する。2005年にJohan de Jongが開始したStacksプロジェクトは代数・幾何・数論を網羅し、その相互接続された定理はAxiomのエージェントにとって大きな課題であった。エージェントは緩やかな階層の下で並行作業し、数学的センスを訓練された。この成果は形式化された代数幾何学の大きな空白を埋め、将来の証明やAI生成ソフトウェアに再利用可能な検証済み基盤を提供し、信頼できる数学の上に構築することで「AIスロップ」への懸念に対処する。

(出典：TechCrunch)