アクシオム、20年の数学百科を人工知能で形式化

人工知能数学企業アクシオム・マスは11月4日、代数幾何の参考書スタックスプロジェクトをリーンで形式化した約1575万行のコードを公開した。スタックスプロジェクトはコロンビア大学のヨハン・デ・ヨンが2005年に始め、116章、7600ページ超、650人が参加した相互参照型知識集である。アクシオムは形式化可能なラベルを網羅し、数学ライブラリマスリブの上に、人手検証済みコア層と、人工知能が作成しリーン検証済みだが人手未レビューの前沿層を作った。4人の数学者が審査を管理し、外部貢献者が前沿層を検証してコアへ昇格させる予定だ。原書側は人工知能コードの受け入れを制限しているため、当面アクシオム側で運用し、将来のマスリブ統合を目指す。 同社は素数間隔246定理や有限単純群分類定理の形式化でも実績を作り、今回は持続更新される数学知識基盤を整備した。人工知能に設計、定義、証明を分担させ、原書の局所修正や反例も発見したと説明した。アントロピックなどの形式化急増を受け、リーンコミュニティは速さより再利用性、公開審査、文献対応を重視した。だがマスリブ合流は人手レビューが壁で、リーン検証は論理的正しさのみ保証し、原書の数学的意味の忠実性は保証しない。