OptProver：連続学習によって難関算数と最適化を形式証明でつなぐ

Abstract

近年の形式的定理証明の進展は、オリンピックレベルの数学に焦点を当てることが多く、学部レベルの領域はほとんど未開拓のままです。機械学習にとって基盤である最適化は、機械学習、オペレーションズ・リサーチ、科学計算に不可欠ですが、既存の証明器による支援が十分ではありません。凸性、最適性条件、アルゴリズム解析といった領域固有の形式化への依存が大きな分布シフトを生み、単純な領域間転移では効果を得にくくなっています。私たちは、オリンピックから学部レベルの最適化への頑健な転移を実現する学習済みモデル OptProver を提示します。強力なオリンピックレベルの証明器から出発し、私たちのパイプラインは 2 つの主要な革新によって分布シフトを緩和します。第一に、専門家反復による大規模な最適化重視データのキュレーションを用います。第二に、仮定困惑度（perplexity）で重み付けされた最適化と、有効ではあるが進展しない証明ステップを罰する仕組みを統合した、特化した嗜好学習（preference learning）の目的関数を導入します。これにより分布シフトへの対処ができるだけでなく、探索を効率的な軌道へと導きます。厳密な評価を可能にするために、最適化に焦点を当てた Lean 4 の新しいベンチマークを構築します。このベンチマーク上で、OptProver は、同程度の規模のモデル群の中で Pass@1 および Pass@32 において最先端の性能を達成し、一般的な定理証明タスクでも競争力のある性能を維持することで、破滅的忘却を伴わない効果的な領域転移を示しています。