MIT研究者、AIで数学の発見を加速する助成金獲得

マサチューセッツ工科大学（MIT）数学科の研究者らが、AIを活用して数学の発見を加速させるプロジェクトで、初回「AI for Math」助成金の受賞者に選ばれました。このプロジェクトは、大規模数学データベースと定理証明支援ライブラリを連携させるものです。これにより、AIが数学研究を支援する新たな基盤を構築し、研究開発の効率を飛躍的に高めることを目指します。

数学研究の自動化には、知識をAIが理解できる形に「形式化」するコストが高いという壁があります。このプロジェクトは、既存の膨大な数学データベースと、証明の正しさを検証するシステムを繋ぐことでこの課題を解決します。形式化の障壁を下げ、より多くの数学者がAIの恩恵を受けられるようにすることを目指します。

具体的には、数論データベース「LMFDB」と定理証明支援ライブラリ「mathlib」を連携させます。これにより、LMFDBが持つ膨大な未証明のデータを、mathlib内で証明のターゲットとして提示可能になります。これは人間とAI双方にとって、数学的発見のプロセスを大きく変える可能性を秘めています。

このアプローチの利点は、過去の計算資産を最大限に活用できる点にあります。LMFDBの構築に費やされた膨大な計算結果を再利用することで、コストを大幅に削減します。また、事前に計算された情報があるため、新たな定理の例や反例を探す探索作業も、より効率的に行えるようになります。

AIとデータベースの連携は、既に成果を生んでいます。機械学習で「マーマレーション」という数学現象が発見された際、LMFDBの整理されたデータが決定的な役割を果たしました。専門家によって整理された高品質なデータベースが、AIによる新たな発見を促す鍵となるのです。

研究チームは今後、コミュニティと連携しながらツールの開発を本格化させます。データベースの定義を形式化し、mathlib内からLMFDBの検索を実行できる機能などを実装する計画です。この取り組みは、数学だけでなくAIが専門知識を扱う他分野への応用も期待されます。