形式数学のライブラリは急速に拡大しており、検証済み証明を保守性の観点からリファクタリングする必要性と、ニューラル証明器の訓練データ品質を高める必要性が同時に増している。しかし、スケーラブルな証明最適化は、目的関数が異質でヒューリスティックに指定されがちであること、データが乏しいこと、そして訓練と推論のコストが高いことによって妨げられてきた。
こうした課題に対処するため、著者らは Lean 4 における自動証明最適化のための神経記号フレームワーク ImProver 2 を提案する。ImProver 2 は、データ効率の高いエキスパート反復パイプラインと、形式構造を軽量な非形式的抽象と並べて提示するスキャフォールドを組み合わせた点に特徴がある。これによりモデルは、厳密な形式記述と直感的な理解の両方を手がかりに証明を再構成できる。研究チームはさらに、証明の構造的性質を捉える一連の評価指標を導入し、最適化の目標を散発的なヒューリスティックに依存させない枠組みを整えた。
実験では、ImProver 2 を用いて70億パラメータのモデルを訓練した。このモデルは同一モデルファミリー内でパラメータ数が桁違いに大きいモデルを上回る性能を示し、複数の指標において中位のフロンティアモデルと競合する。また、この神経記号スキャフォールドが小規模モデルとフロンティアモデルの双方で性能を有意に改善することも示され、構造化された足場が幅広いシステムに有効であることが確認された。
論文の中心的な主張は、適切なスキャフォールドと訓練があれば、小規模なモデルでも研究レベルの証明を効果的に再構成でき、複雑で多様な指標においてはるかに大きなシステムに匹敵し得るという点にある。これにより証明最適化は、人手やヒューリスティックに依存する工学作業ではなく、スケーラブルで学習可能なタスクとして位置づけられる。
本論文は2026年5月21日に投稿され、著者は Riyaz Ahuja ら4名である。arXiv の cs.AI 分類に掲載され、cs.CL、cs.LG、cs.LO にも関連し、論文番号は arXiv:2605.22885 である。