🤖 machine learning

OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving

本論文は、オリンピアード数学レベルの証明モデルに対し、専門的なデータキュレーションと独自の嗜好学習（preference learning）を導入することで、分布の異なる大学レベルの最適化問題への効果的なドメイン転移を実現した「OptProver」を提案しています。

原著者： Chenyi Li, Yanchen Nie, Zhengyu Ming, Gong Zhang, Kun Yuan, Zaiwen Wen

公開日 2026-04-28

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： Chenyi Li, Yanchen Nie, Zhengyu Ming, Gong Zhang, Kun Yuan, Zaiwen Wen

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

タイトル：数学の「天才」を「専門家」へ育てる：OptProverの挑戦

1. 背景：数学界の「万能な天才」が抱える悩み

想像してみてください。ここに、オリンピック数学オリンピックの問題をスラスラ解いてしまう、ものすごく頭の良い**「万能な天才少年」**がいます。彼は、パズルや論理クイズ、一般的な数学のルールには完璧に精通しています。

しかし、彼には一つ弱点がありました。それは、**「専門的な仕事」**です。
例えば、彼に「最新のAI開発に不可欠な『最適化理論（Optimization）』という、非常に高度で特殊なルールに基づいた計算」を頼むと、彼は途端に混乱してしまいます。

なぜか？彼は「一般的な数学のルール」は知っていますが、「最適化」という分野特有の**「専門用語」や「独特の作法（書き方）」**をまだ学んでいないからです。無理に新しいことを教えようとすると、彼は混乱してしまい、せっかく持っていた「一般的な数学の能力」まで忘れてしまう（これを専門用語で「破滅的忘却」と言います）という問題がありました。

2. 課題：新しいことを学ぶと、前のことを忘れてしまう？

これまでのAI（数学プロバー）は、新しい分野を学ばせようとすると、まるで**「新しい言語を猛勉強しすぎて、母国語を忘れてしまう学生」**のような状態になっていました。

また、新しい分野の教科書をただ読ませるだけでは、AIは「見た目はそれっぽいけれど、中身がスカスカな解答」を書き始めてしまいます。これは、**「専門用語は知っているけれど、使いどころを間違えて、結局答えにたどり着けない迷子」**のような状態です。

3. 解決策：OptProverの「魔法のトレーニング・プログラム」

研究チームは、この天才少年を「最適化の専門家」に育てるために、**『OptProver』**という新しいトレーニング方法を開発しました。そのポイントは3つあります。

① 「自習」と「教科書」のハイブリッド学習（Expert Iteration）
ただ教科書を読ませるのではなく、AI自身に「自分で問題を解いて、正解にたどり着くまでのプロセスを記録させる」という自習をさせました。これに、厳選された専門教科書の内容を組み合わせることで、効率よく「専門家の作法」を身につけさせました。
② 「無駄な動き」を厳しく指導する（Utility-Aware Preference）
ここが一番の工夫です。数学の証明では、「文法としては正しいけれど、全然ゴールに近づかない、回りくどい手順」というものがあります。これは、**「目的地に向かっているようで、実は同じ場所をぐるぐる回っている迷子」**のようなものです。
OptProverは、この「正解だけど、無駄な動き」を「これはダメな動きだよ！」と厳しく指摘される仕組み（報酬の調整）を取り入れました。これにより、最短ルートで答えにたどり着く「効率的な思考」を身につけました。
③ 「混乱」を防ぐブレーキ（Perplexity-Weighted DPO）
新しいことを学ぶとき、あまりに難しすぎる（未知すぎる）情報にぶつかると、AIの脳はパニックを起こして学習が不安定になります。そこで、**「あまりに難しすぎる情報は、少しずつ、慎重に学習する」**というブレーキ機能を付けました。これにより、新しい知識を取り入れつつ、もともと持っていた「天才的な数学能力」を壊さずに守ることができたのです。

4. 結果：最強の「数学専門家」の誕生

このトレーニングの結果、OptProverは驚くべき成果を出しました。

専門分野で圧倒的な強さ： 「最適化」という難しい分野のテストにおいて、これまでのAIを大きく引き離し、トップクラスの成績を収めました。
「忘れない」強さ： 新しいことを学んだ後でも、もともと得意だった「オリンピックレベルの数学」や「大学数学」の能力を落とすことなく、むしろ向上させることさえできました。

まとめ

この研究は、**「広く浅い知識を持つAI」を、いかにして「元の能力を保ったまま、特定の分野のプロフェッショナルに変身させるか」**という問いに対する、非常にスマートな答えを出したものです。

これは、将来的にAIが「数学の専門家」として、科学研究や高度なエンジニアリングの現場で、人間と一緒に複雑な問題を解いていくための大きな一歩となります。

技術要約：OptProver

1. 背景と問題意識 (Problem)

現在の形式定理証明（Formal Theorem Proving）における大規模言語モデル（LLM）の研究は、主に数学オリンピックレベルの難問（MiniF2Fなど）に焦点を当ててきました。しかし、機械学習や最適化理論の基盤となる**「最適化（Optimization）」**領域は、既存の証明モデルでは十分にカバーされていません。

最適化領域への適応には、以下の2つの大きな課題（Interactive Distribution Shift）が存在します：

分布の乖離と破滅的忘却: 最適化特有の記法（凸性、最適性条件、アルゴリズム解析など）を学習させようとすると、モデルがそれまで持っていた一般的な数学的推論能力を失ってしまう（破滅的忘却）。
「有効だが進展しない」ステップの存在: 形式証明の検証器（Lean 4など）は、構文的に正しくても、証明をゴールに導かない「停滞した（stagnant）」タクティクス（操作）を許容してしまいます。これらは探索ツリーにおいて計算資源を浪費する「探索の罠」となり、推論効率を著しく低下させます。

2. 提案手法 (Methodology)

本論文では、オリンピックレベルの推論能力を維持しつつ、最適化領域へ効果的に転移させるための継続学習パイプライン OptProver を提案しています。

A. 大規模自己蒸留 (Large-Scale Self-Distillation via Expert Iteration)

単なる教科書のデータ学習ではなく、Expert Iteration (EI) を用いて、モデル自身がMathlib（数学ライブラリ）内の定理を探索し、成功した軌跡を学習データとして蓄積します。これにより、静的な知識をモデルが扱える「タクティクス言語」へと変換します。

B. ユーティリティを考慮した選好学習 (Utility-Aware Preference Optimization: UAPO)

従来のDPO（Direct Preference Optimization）では、単に「正しいか否か」を学習しますが、OptProverは**「証明の進展度（Utility）」**を導入します。

Utilityの定義: 成功した経路（ $u=2$ ）、エラー（ $u=0$ ）に加え、構文的には正しいがゴールに到達できなかった「停滞したステップ（ $u=1$ ）」を区別します。
目的: 停滞したステップを「好ましくない（rejected）」ものとして明示的にペナルティを与えることで、探索を効率的な軌跡へと導きます。

C. Perplexity加重DPO (Perplexity-Weighted DPO: PW-DPO)

参照モデル（学習前のモデル）にとって予測困難な（Perplexityが高い）トークンは、勾配の分散を大きくし、学習を不安定にする原因となります。

手法: トークンレベルのPerplexityに基づき、学習時の重みを調整します。これにより、参照モデルがサポートしていない未知すぎるデータによる悪影響を抑え、学習の安定化と破滅的忘却の防止を図ります。

3. 主な貢献 (Key Contributions)

新しい問題設定の定式化: 形式証明における継続学習を、オリンピック数学から最適化への「インタラクティブな分布シフト」として定義しました。
高度な学習アルゴリズム: 停滞したステップを排除する UAPO と、学習を安定させる PW-DPO を組み合わせた、新しい学習フレームワークを開発しました。
新ベンチマーク「OptBench」の構築: 最適化理論（基礎、凸解析、アルゴリズム解析）に特化した400問のLean 4形式ベンチマークを構築しました。

4. 実験結果 (Results)

OptBenchでの性能: OptProverは、同規模のモデルの中で最高水準（SOTA）を達成しました。最終的な Pass@32で55.25% という高い成功率を記録しました。
汎用性の維持: 最適化への特化を行っても、MiniF2F（オリンピック数学）やProofNet（学部数学）における性能を低下させることなく、むしろ向上させることに成功しました（破滅的忘却の回避）。
手法の有効性: Ablation Studyにより、EI（Expert Iteration）単体よりも、UAPOやPW-DPOを組み合わせた方が、探索効率と精度が大幅に向上することが示されました。

5. 意義 (Significance)

本研究は、特定の専門領域（最適化）へのドメイン適応において、単に「正しいデータ」を教えるだけでなく、**「推論の効率性（Utility）」と「学習の安定性（Perplexity weighting）」**を制御することが極めて重要であることを示しました。これは、形式的な数学証明だけでなく、他の専門的な形式言語や高度な推論タスクへのLLM適応における重要な指針となります。