arXiv:2607.13292：理論レベルの自動形式化——孤立した命題ではなく数学理論全体を対象に（ICML 2026）

自動形式化とは何か、なぜ難しいのか？

自動形式化は、数学のテキストを自然言語から機械検証可能な形式——LeanやIsabelleのような証明アシスタントが使用する形式——に自動翻訳することです。すべての形式的な命題は曖昧さなく正確で計算的に検証可能でなければならず、学術論文のレベルをはるかに超える精度が要求されます。これまでのシステムは各命題を独立した単位として扱い、数学者が当然のこととしている文脈を無視していました。

なぜ孤立した命題では不十分なのか？

Marcus J. Min・Mike He・Zhaoyu LiとOsbert Bastaniを含む共著者たちは、形式数学には「相互依存のネットワーク」が必要だと主張しています——公理が基盤を定め、定義が抽象を構築し、補題が定理への道を準備します。そのネットワークなしに定理だけを形式化することは、前の章を知らずに小説の一文を翻訳するようなものです：形式は正しくても意味は不完全なままです。この論文はICML 2026でSpotlight発表として採択されており、これは査読委員会が会議の最高評価論文として分類することを意味します；GitHubリポジトリは再現のために公開されています。

三つの前進経路と広い文脈

研究者たちは理論レベルの形式化に向けた3つの具体的な前進経路を提供しています。比較として、miniF2Fのような以前のベンチマークは孤立したオリンピックタスクのセットでモデルをテストしていました——著者らによれば、このアプローチは理論的深さの面で機械と人間の数学的能力の差を体系的に過小評価しています。理論の完全な形式化へのシフトは、事前に指定された命題を検証するだけでなく、独自に数学的知識ベースを構築・拡張できるAIシステムへの道を開きます。