Axiom Math、AI低品質生成を防ぐ数学検証基盤構築

数学人工知能スタートアップのアジオム・マスは、オープンソースの数学知識庫スタックス・プロジェクトを証明支援言語リーンで形式化・検証したと発表した。プロジェクトは2005年に始まった人間による体系的な数学の集成で、代数幾何を含む大学レベルから最先端までを網羅する。同社は約7654ページを約1600万行のリーンコードに翻訳し、証明支援器によって論理的整合性を確認した。定理や定義が先行する結果に依存する構造のため、多数の人工知能エージェントを並列で動かし、自律的な作業配分によって相互関係を維持しながら形式化を進めたと説明する。2025年3月設立で、メンロー・ベンチャーズ主導の2億ドル調達を背景に企業価値16億ドルとされる。最高経営責任者キャリナ・ホン氏は、検証済み数学を人工知能エージェントが再利用できる基盤にすれば、大量生成による誤りや品質劣化を防ぎ、ソフトウェア開発や科学領域へと応用を拡大できると述べている。