ソルバーから研究へ：大規模言語モデルが導くフロンティア形式数学
本ポジションペーパーは、AI for Mathematics（AI4Math）分野の最近の進展、特に大規模言語モデル（LLM）駆動の定理証明器による形式証明生成の成功を概観する。しかし、既存システムは新定理の発見や未解決予想の解決など、未定義で抽象度の高い最前線の研究数学には根本的に対応できない。著者らは、AI4Mathシステムを所定の問題ソルバーから厳密な形式数学的推論が可能な研究エージェントへと転換する必要性を主張し、データセット、関係構造、数学的探索、ツールエコシステム、人間-AI協調における核心的限界を特定し、将来の戦略的ロードマップを示す。
近年、人工知能による数学（AI4Math）の分野では、大規模言語モデル（LLM）を活用した定理証明器が注目を集めている。これらのシステムは対話型定理証明（ITP）言語を用いて、明確に定義された数学問題に対する形式証明を自動生成することに成功し、大きな成果を挙げてきた。しかし、未解決の予想や新たな定理の発見といった最前線の研究数学に取り組むには、現在のシステムは根本的に不十分である。それらの課題は、しばしばオープンエンドで、仕様が不完全であり、複数の抽象化層を伴うためである。
Eric Jiangら19名の著者によるarXivプレプリントでは、AI4Mathの現状を体系的にレビューし、重要な転換点を論じている。彼らは、AI4Mathが所定の問題を解くソルバーから、厳密な形式数学的推論を通じて研究課題に取り組める「研究エージェント」へと進化すべきだと主張する。論文はまず、データセット、自動形式化、証明合成の3つの分野における既存研究を概観する。データセットに関しては、MiniF2FやProofNetなどの既存ベンチマークが既知の競技問題や教科書問題に偏っており、研究最前線をカバーしていないと指摘。自動形式化は非形式数学を検証可能なコードに変換する技術だが、複雑な文脈では信頼性に欠ける。証明合成はLLMの進歩により改善したが、生成される証明は短く、深い探索を必要とする定理には対応できない。
より重要な点として、論文は既存システムが数学研究エージェントとして機能する際の5つの核心的限界を特定している。第一にデータセットの問題：規模が小さく、数学研究の多様性と深さを反映していない。第二に関係構造の欠如：数学知識は定理間の論理的関係のネットワークで構成されるが、現在のシステムはその構造化理解を持たない。第三に数学的探索能力の不足：研究には試行錯誤や創造性が不可欠だが、システムは所定の探索経路しかたどれない。第四にツールエコシステムの未成熟：コンピュータ代数システムなどの既存数学ソフトウェアや人間との協調ワークフローとの統合が不十分。第五に人間-AI協調の脆弱さ：AIは数学者を補完すべきだが、現在の相互作用の枠組みは限定的である。
これらの分析に基づき、著者らは戦略的ロードマップを提示する。将来のAI4Mathシステムは、大規模な関係データベースの構築、抽象化と類推のメカニズムの導入、証明アシスタントや計算ツールとのシームレスな統合、そして自然言語と形式言語のハイブリッドインターフェースといった要素を備えるべきだと論じる。本論文は、AI4Math分野の現在の成果と限界を鋭く指摘し、次なる発展の方向性を示す重要なロードマップとなっている。