最新の数学界を揺るがすニュースとして、清華大学の卒業生グループがAIを活用し、これまで解かれていなかった162個の数学定理の証明に成功しました。さらに驚くべきことに、LeanAgentと名付けられたこのAIは、陶哲軒氏が多項式Freiman-Ruzsa予想に対して提示した形式化問題も解決しました！基礎科学研究の方法がAIによって完全に変革されたと言えるでしょう。
現在、話題の言語モデル（LLM）は、多くの場合静的なものであり、オンラインで新しい知識を学習することができず、高等数学の定理を証明することは非常に困難です。しかし、カリフォルニア工科大学、スタンフォード大学、ワシントン大学の研究チームが共同開発したLeanAgentは、生涯学習能力を備えたAIアシスタントであり、定理を継続的に学習し証明することができます。
LeanAgentは、精巧に設計された学習経路によって様々な数学的難易度に対応し、動的なデータベースを用いて絶え間なく数学知識を取り込み、新しい知識を学習する際に既に習得したスキルを忘れないようにします。実験によると、23個もの異なるLeanコードライブラリから、これまで解かれていなかった162個の数学定理を証明し、従来の大規模モデルと比較して性能が11倍も向上しました！これは驚くべき成果です。
これらの定理は、抽象代数や代数トポロジーなど、高等数学の多くの分野における難しい問題を網羅しています。LeanAgentは、単純な概念から始めて複雑なテーマを徐々に克服するだけでなく、安定性と逆転移転においても優れた性能を示しました。
しかし、陶哲軒氏の提示した課題は、AIにとっても依然として難しいものでした。Leanのような対話型定理証明器（ITP）は、数学的証明の形式化と検証において重要な役割を果たしていますが、このような証明過程を構築することは複雑で時間がかかり、細心の注意を払った手順と大量の数学コードライブラリが必要です。o1やClaudeのような高度な大規模モデルは、非形式的な証明に直面すると誤りを犯しやすい傾向があり、LLMにおける数学的証明の正確性と信頼性の欠点を浮き彫りにしています。
これまでの研究では、LLMを用いて完全な証明手順を生成する試みがなされてきました。例えば、LeanDojoは、大規模モデルを特定のデータセットで訓練することで作成された定理証明器です。しかし、形式的な定理証明のデータは非常に不足しており、この方法の広範な適用を制限しています。別のプロジェクトであるReProverは、Lean定理証明コードライブラリmathlib4に最適化されたモデルですが、10万を超える形式化された数学定理と定義を網羅しているものの、学部レベルの数学の範囲に限定されているため、より複雑な問題に直面すると性能が低下します。
注目すべきは、数学研究の動的な性質がAIに大きな課題をもたらしていることです。数学者は通常、複数のプロジェクトを同時または交互に処理します。例えば、陶哲軒氏はPFR予想と実数の対称平均など、複数の研究分野を同時に進めています。これらの例は、現在のAI定理証明方法の重要な欠点、つまり、特にLeanデータが限られている状況において、異なる数学分野で適応的に学習し向上できるAIシステムが不足していることを示しています。
そのため、LeanDojoのチームは、上記の課題を解決することを目的とした、新しい生涯学習フレームワークであるLeanAgentを作成しました。LeanAgentのワークフローには、定理の複雑さを推定して学習カリキュラムを作成すること、漸進的な訓練を通じて学習過程における安定性と柔軟性のバランスを取る、そして未証明の定理を探すために最良優先探索を使用することが含まれます。
LeanAgentは、任意の大規模モデルと組み合わせて使用され、「検索」によって汎化能力を高めます。その革新的な点は、絶え間なく拡大する数学知識を管理するためのカスタム動的データベースと、Lean証明構造に基づいたカリキュラム学習戦略を使用することで、より複雑な数学的コンテンツの学習を支援することです。
AIにおける壊滅的な忘却問題に対処するために、研究者たちは漸進的な訓練方法を採用し、LeanAgentが新しい数学知識に継続的に適応しながら、以前の学習を忘れないようにしました。この過程には、各新しいデータセットで増分トレーニングを行い、安定性と柔軟性の最適なバランスを確保することが含まれます。
この漸進的な訓練により、LeanAgentは定理証明において優れた性能を示し、162個の人間が解いていない問題を解決しました。特に、抽象代数と代数トポロジーにおける困難な定理においてその能力を発揮しました。新しい定理を証明する能力は、静的なReProverと比較して11倍高く、既知の定理の証明能力も維持しています。
LeanAgentは、定理証明において漸進的な学習の特徴を示し、単純な定理から徐々に複雑な定理へと移行することで、数学的知識の習得の深さを証明しました。例えば、群論や環論に関連する基礎的な代数構造の定理を証明し、数学に対する深い理解を示しました。全体的に見て、LeanAgentは強力な継続学習と改善能力により、数学界にエキサイティングな展望をもたらしています！
