論文の概要: OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving

• arxiv url: http://arxiv.org/abs/2604.23712v1
• Date: Sun, 26 Apr 2026 13:54:28 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-28 17:12:07.51588
• Title: OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving
• Title（参考訳）: OptProver: 形式的理論証明における継続トレーニングによるオリンピアドのブリッジと最適化
• Authors: Chenyi Li, Yanchen Nie, Zhengyu Ming, Gong Zhang, Kun Yuan, Zaiwen Wen,
• Abstract要約: 正式なオリンピアド級数学の最近の進歩は、大半が単純ドメイン領域を残している。 本稿では,証明手順の検証を行うためのメカニズムを取り入れた特殊パーリティ重み付き最適化を導入する。 このベンチマークでは、最先端のドメイン知識を実証することで、ステート・オブ・ワンかつ比較可能な大きさのドメインが達成される。
• 参考スコア（独自算出の注目度）: 11.256978472844786
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Recent advances in formal theorem proving have focused on Olympiad-level mathematics, leaving undergraduate domains largely unexplored. Optimization, fundamental to machine learning, operations research, and scientific computing, remains underserved by existing provers. Its reliance on domain-specific formalisms (convexity, optimality conditions, and algorithmic analysis) creates significant distribution shift, making naive domain transfer ineffective. We present OptProver, a trained model that achieves robust transfer from Olympiad to undergraduate optimization. Starting from a strong Olympiad-level prover, our pipeline mitigates distribution shift through two key innovations. First, we employ large-scale optimization-focused data curation via expert iteration. Second, we introduce a specialized preference learning objective that integrates perplexity-weighted optimization with a mechanism to penalize valid but non-progressing proof steps. This not only addresses distribution shifts but also guides the search toward efficient trajectories. To enable rigorous evaluation, we construct a novel benchmark in Lean 4 focused on optimization. On this benchmark, OptProver achieves state-of-the-art Pass@1 and Pass@32 among comparably sized models while maintaining competitive performance on general theorem-proving tasks, demonstrating effective domain transfer without catastrophic forgetting.
• Abstract（参考訳）: 形式定理の証明の最近の進歩は、オリンピアード級数学に焦点を合わせており、学部の領域はほとんど探索されていない。 機械学習、オペレーションリサーチ、科学コンピューティングの基本となる最適化は、まだ既存の証明者によって守られていない。 ドメイン固有の形式(凸性、最適性条件、アルゴリズム解析)に依存しているため、大きな分布シフトが生じ、単純で効率的なドメイン転送が不可能となる。 Olympiadから学部最適化への堅牢な移行を実現するためのトレーニングモデルであるOpsProverを提案する。 強力なOlympiadレベルの証明から始めて、パイプラインは2つの重要なイノベーションを通じて分散シフトを緩和します。 まず、専門家の反復による大規模最適化に焦点を当てたデータキュレーションを用いる。 第2に、複雑度重み付け最適化と、有効だが非進行的な証明ステップをペナルティ化するためのメカニズムを統合する、特殊選好学習の目的を導入する。 これは分布シフトに対処するだけでなく、効率的な軌跡への探索も導く。 厳格な評価を可能にするため、最適化にフォーカスした新しいベンチマークをLean 4で構築する。 このベンチマークでは、OptProverは、一般的な定理証明タスクにおける競合性能を維持しながら、比較可能なサイズのモデルの中で最先端のPass@1とPass@32を達成する。

関連論文リスト

• A Novel Unified Parametric Assumption for Nonconvex Optimization [53.943470475510196]
  非最適化は機械学習の中心であるが、一般の非凸性は弱い収束を保証するため、他方に比べて悲観的すぎる。 非凸アルゴリズムに新しい統一仮定を導入する。
  論文  参考訳（メタデータ） (2025-02-17T21:25:31Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Discovering Preference Optimization Algorithms with and for Large Language Models [50.843710797024805]
  オフライン優先最適化は、LLM(Large Language Model)出力の品質を向上・制御するための重要な手法である。 我々は、人間の介入なしに、新しい最先端の選好最適化アルゴリズムを自動で発見する客観的発見を行う。 実験は、ロジスティックと指数的損失を適応的にブレンドする新しいアルゴリズムであるDiscoPOPの最先端性能を示す。
  論文  参考訳（メタデータ） (2024-06-12T16:58:41Z)
• ENOT: Expectile Regularization for Fast and Accurate Training of Neural Optimal Transport [3.0237149871998095]
  最適な輸送計画の正確かつ効率的に推定する新しい手法を提案する。 expectile Regularized Neural Transport Optimal (ENOT) と呼ばれる。 ENOTは二重ポテンシャルの学習過程に結合条件を強制する。
  論文  参考訳（メタデータ） (2024-03-06T15:15:42Z)
• Pseudo-Bayesian Optimization [7.556071491014536]
  ブラックボックス最適化の収束を保証するために最小限の要件を課す公理的枠組みについて検討する。 我々は、単純な局所回帰と、不確実性を定量化するために適切な「ランダム化事前」構造を用いることが、収束を保証するだけでなく、常に最先端のベンチマークよりも優れていることを示す。
  論文  参考訳（メタデータ） (2023-10-15T07:55:28Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。