形式的数学記述カリキュラム学習

形式的数学に応用された言語モデルにおいて、エキスパート反復（expert iteration）の利用を検討する。同じ計算リソース（compute budget）の条件下で、学習と証明探索を交互に行うエキスパート反復は、単なる証明探索に比べて著しく優れた性能を発揮することを示した。また、難易度が多様な形式的命題の集合に対して適用した場合、エキスパート反復は、対応する真の証明（ground-truth proofs）を提供せずに、難易度が徐々に高い問題のカリキュラムを自動的に発見し、解決可能であることを観察した。さらに、手動で選定された問題セットにこのエキスパート反復を適用することで、miniF2Fベンチマークにおいて最先端の性能を達成し、高校数学オリンピックから抽出された複数の難問を自動的に解くことに成功した。