論文の概要: ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization
- arxiv url: http://arxiv.org/abs/2605.22885v1
- Date: Thu, 21 May 2026 02:20:26 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-25 17:29:20.022735
- Title: ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization
- Title（参考訳）: ImProver 2: ニューロシンボリックな証明最適化のための繰り返し自己改善型LM
- Authors: Riyaz Ahuja, Tate Rowney, Jeremy Avigad, Sean Welleck,
- Abstract要約: 我々は、Lean 4.0で自動証明最適化のためのニューロシンボリックなフレームワークImProver 2を紹介します。
ImProver 2は、データ効率の高いエキスパートイテレーションパイプラインと、非公式な抽象化と並んで形式的な構造を公開する足場を組み合わせたものだ。
適切な足場とトレーニングを行うことで、小さなモデルは、複雑で多様なメトリクスに対して研究レベルの証明を効果的に再構成し、かなり大きなシステムにマッチし、証明最適化をスケーラブルで学習可能なタスクとして確立できることが示される。
- 参考スコア（独自算出の注目度）: 19.226502853809734
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Formal mathematics libraries are rapidly expanding, creating a growing need to refactor verified proofs for maintainability and to improve training data quality for neural provers. However, scalable proof optimization is hindered by heterogeneous and heuristically specified objectives, scarce data, and high training and inference costs. To overcome these challenges, we introduce ImProver 2, a neurosymbolic framework for automated proof optimization in Lean 4. ImProver 2 combines a data-efficient expert-iteration pipeline with a scaffold that exposes formal structure alongside lightweight informal abstractions. We further introduce a suite of metrics capturing structural proof properties. Using ImProver 2, we train a 7B-parameter model that outperforms orders-of-magnitude larger models within the same model family, and is competitive with mid-tier frontier models across metrics. We additionally demonstrate that our neurosymbolic scaffold significantly improves performance across both small and frontier models. We show that with proper scaffolding and training, small models can effectively restructure research-level proofs over complex and varied metrics, matching substantially larger systems and establishing proof optimization as a scalable, learnable task.
- Abstract（参考訳）: 形式数学ライブラリは急速に拡張され、保守性を証明する証明をリファクタリングし、ニューラルプローバーのトレーニングデータ品質を改善する必要性が高まっている。
しかし、スケーラブルな証明最適化は、不均一でヒューリスティックに指定された目的、不足したデータ、高いトレーニングと推論コストによって妨げられる。
これらの課題を克服するために、Lean 4.0で自動証明最適化のためのニューロシンボリックなフレームワークであるImProver 2を紹介します。
ImProver 2は、データ効率の高いエキスパートイテレーションパイプラインと、軽量な非公式抽象化とともに形式的な構造を公開する足場を組み合わせたものだ。
さらに、構造的証明特性をキャプチャする一連のメトリクスを紹介します。
ImProver 2を使用することで、7Bパラメータモデルをトレーニングし、同じモデルファミリ内のマグニチュード・オブ・マグニチュード・モデルよりも優れ、メトリクスをまたいだ中層フロンティアモデルと競合します。
また,我々の神経象徴的足場は,小型モデルとフロンティアモデルの両方で性能を著しく向上させることを示した。
適切な足場とトレーニングを行うことで、小さなモデルは、複雑で多様なメトリクスに対して研究レベルの証明を効果的に再構成し、かなり大きなシステムにマッチし、証明最適化をスケーラブルで学習可能なタスクとして確立できることが示される。
関連論文リスト
- Dual-Phase LLM Reasoning: Self-Evolved Mathematical Frameworks [48.105258051884384]
本稿では,モデルの自己補正能力を高めるための2段階トレーニングフレームワークを提案する。
最初の段階では、マルチターン対話戦略がモデルをガイドし、長いチェーン・オブ・シント(CoT)データを生成する。
第2段階では、データの分散を動的に最適化する難易度の高い拒絶サンプリング機構を採用している。
論文 参考訳（メタデータ） (2026-01-09T08:19:11Z) - How to Set the Learning Rate for Large-Scale Pre-training? [73.03133634525635]
我々はこの調査を2つの異なる研究パラダイムであるフィッティングとトランスファーに定式化する。
フィッティングパラダイムでは,探索係数のスケーリング法則を導入し,O(n3) から O(n*C_D*C_) への探索複雑性を予測モデルにより効果的に低減する。
我々は、$Transferの原則をMixture of Experts (MoE)アーキテクチャに拡張し、モデル深さ、重量減衰、トークン水平線を含む適用範囲を広げる。
論文 参考訳（メタデータ） (2026-01-08T15:55:13Z) - Motif-2-12.7B-Reasoning: A Practitioner's Guide to RL Training Recipes [7.998815625852598]
複雑な推論と長文理解において,オープンウェイトシステムとプロプライエタリフロンティアモデルのギャップを埋めるために設計された12.7Bパラメータ言語モデルを導入する。
提案手法は,ハイブリッド並列処理とカーネルレベルの最適化を用いて,64Kのコンテキストに対するメモリ効率のよいインフラストラクチャを組み合わせる。
本稿では,難易度を考慮したデータフィルタリングと混成政治軌道再利用によるトレーニングを安定化する,堅牢な強化学習ファインタニングパイプラインについて述べる。
論文 参考訳（メタデータ） (2025-12-11T00:51:18Z) - Sycophancy Mitigation Through Reinforcement Learning with Uncertainty-Aware Adaptive Reasoning Trajectories [58.988535279557546]
適応推論トラジェクトリを用いたtextbf sycophancy Mitigation を提案する。
SMARTは,分布外の入力に対して強い性能を維持しながら,サイコファンティクスの挙動を著しく低下させることを示した。
論文 参考訳（メタデータ） (2025-09-20T17:09:14Z) - LimiX: Unleashing Structured-Data Modeling Capability for Generalist Intelligence [61.46575527504109]
LimiX-16MとLimiX-2Mは、構造化されたデータを変数と欠落に対する共同分布として扱う。
サンプルサイズ,特徴次元,クラス数,カテゴリ間特徴比,欠落度,サンプル-特徴比の広い11種類の大規模構造化データベンチマークを対象としたLimiXモデルの評価を行った。
論文 参考訳（メタデータ） (2025-09-03T17:39:08Z) - Solving Formal Math Problems by Decomposition and Iterative Reflection [30.54275542622631]
textbfDelta Proverは汎用LLMとLean 4の実証環境とのインタラクションを編成します。
bftextDelta Proverは、miniF2F-testベンチマークで、最先端の95.9%の成功率を達成した。
論文 参考訳（メタデータ） (2025-07-21T03:56:35Z) - High-Fidelity Scientific Simulation Surrogates via Adaptive Implicit Neural Representations [51.90920900332569]
入射神経表現(INR)は空間的に構造化されたデータをモデリングするためのコンパクトで連続的なフレームワークを提供する。
近年のアプローチでは、剛性幾何学的構造に沿った付加的な特徴を導入することでこの問題に対処している。
機能適応型INR(FA-INR)を提案する。
論文 参考訳（メタデータ） (2025-06-07T16:45:17Z) - Ultra-Resolution Adaptation with Ease [62.56434979517156]
我々は,EmphURAEと呼ばれる超高分解能適応のための重要なガイドラインのセットを提案する。
重み行列の小さな成分のチューニングは、合成データが利用できない場合に広く使用される低ランクアダプタよりも優れていることを示す。
URAEは、FLUX1.1[Pro] Ultraのような最先端のクローズドソースモデルに匹敵する2K世代の性能を達成している。
論文 参考訳（メタデータ） (2025-03-20T16:44:43Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。