論文の概要: LeanPolish: Verified Supervision for Lean Proof Compression
- arxiv url: http://arxiv.org/abs/2609.38384v1
- Date: Tue, 29 Sep 2026 18:40:00 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-01 18:57:26.596676
- Title: LeanPolish: Verified Supervision for Lean Proof Compression
- Title（参考訳）: LeanPolish: リーンの証明圧縮のための検証済みのスーパービジョン
- Abstract要約: これは、33,402件の承認されたローカル編集と65,596件の同じ状態の試行をリリースする象徴的なLean 4パイプラインです。
First-success Searchは、完全なランキング精度でゴールに依存しないルールを認めており、教師が選択した評価サイトは、自明な削除を報いる。
圧縮のために、シンボリックパスを繰り返すと、ミニF2Fの節約率は19.7%から27.5%に上昇する。
- 参考スコア（独自算出の注目度）: 4.272652712282259
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Verified proof edits offer a natural source of supervision for improving language-model-generated Lean proofs. Yet verification establishes that an edit is correct, not that its training signal is free of search artifacts. We introduce LeanPolish, a symbolic Lean 4 pipeline that releases 33,402 accepted local edits and 65,596 same-state failed attempts, and use it to study what models learn from this supervision. First-success search admits a goal-independent rule with perfect ranking accuracy; teacher-selected evaluation sites also reward trivial deletions. Continuing menu evaluation beyond the first success removes the ordering shortcut: a trained ranker selects the best candidate on 70.1% of evaluated held-out states, versus 36.9% for the strongest frozen baseline. For compression, iterating the symbolic pass raises miniF2F savings from 19.7% to 27.5%, exceeding the neural hybrids we test there. Verified neural editing helps on other proof sources, but matched frozen-model controls show that its gains need not come from training. The supervision does improve whole-proof rewriting: fine-tuning raises verified token reduction from 2.8% to 5.5% on 19 PutnamBench proofs. Together, the released edits, complete candidate pools, and controlled evaluations separate learning to imitate a search policy from improving on that search. They provide a reproducible basis for studying proof improvement while keeping correctness, compression, and edit policy distinct.
- Abstract（参考訳）: 検証済みの証明編集は、言語モデル生成のリーン証明を改善するための、自然な監督源を提供する。
しかし、検証は、そのトレーニング信号が検索アーティファクトを含まないことではなく、編集が正しいことを証明している。
我々はLeanPolishという,33,402件の承認されたローカル編集と65,596件の同じ状態の試みをリリースした象徴的なLean 4パイプラインを紹介します。
First-success Searchは、完全なランキング精度でゴールに依存しないルールを認めており、教師が選択した評価サイトは、自明な削除を報いる。
訓練されたランク付け者は、評価された保留状態の70.1%で最高の候補を選ぶが、最強の凍結ベースラインでは36.9%である。
圧縮のために、シンボリックパスを反復すると、ミニF2Fの節約率は19.7%から27.5%に上昇し、そこでテストしたニューラルハイブリッドを上回ります。
検証済みのニューラル編集は、他の証明ソースに役立つが、凍ったモデル制御は、トレーニングから得られるものではないことを示している。
微調整は、19のパットナムベンチ証明において、認証トークンの減少を2.8%から5.5%に引き上げる。
同時に、リリースされた編集、完全な候補プール、および制御された評価は、検索ポリシーをその検索の改善から模倣するために別々に学習される。
正確性、圧縮性、編集ポリシーを明確に保ちながら、検証改善を研究するための再現可能な基盤を提供する。
関連論文リスト
- Reward Hacking Challenges Oversight of Autonomous Research Agents [104.38175629103235]
自律的な研究エージェントは実験を設計し、結果を評価し、レポートを書き、科学的結果とそれを支持する証拠の両方を制御できる。
これは、意図した目標を達成することなく、報酬基準を満たす、報酬ハックのリスクを生み出す。
そこで本研究では,ハッキングが許可された場合,その方法がいかに効果的かつ検出可能か,LCMレビューパネルが意思決定と理由を返却した場合にどのように適応するか,などについて検討する。
論文 参考訳（メタデータ） (2026-09-23T17:54:01Z) - FADE: From Passive Verification to Active Discovery in Counterfactual Video Understanding [19.559643217912114]
既存のMultiple-choice question (MCQ)ベンチマークは、質問や候補オプションを通じて、意図的にターゲットイベントをリークする。
本稿では, 対実的発見と説明のための効果的なトレーニングフレームワークであるFADEを紹介する。
FADEは、DualityVidQA-test と IPV-Bench の3つのタスクにまたがる、最先端の厳密なペアスコアを達成し、GPT-5.6を上回った。
論文 参考訳（メタデータ） (2026-08-11T10:22:08Z) - Looping Is Not Reliability: State-Bound Evidence and Typed Revision Contracts for Agentic Code Repair [36.56438114281786]
正しいパッチの発見と保持、検証、提出のギャップについて検討する。
我々はエビデンスバウンド型ループ契約を導出し、その機械的に強制可能なサブセットを参照実装でインスタンス化する。
論文 参考訳（メタデータ） (2026-07-27T16:05:23Z) - Reinforcement Learning for Large Language Model Selective Evidence Adoption from Contaminated Retrieval Results [3.9964880913101677]
検索可能な拡張された大きな言語モデルは、誤解を招くステートメントや命令ライクなコンテンツと有用なエビデンスをインターリーブするコンテキストに直面します。
本稿では,選択的エビデンス導入のためのベンチマークとトレーニングセットであるSelectBenchと,DAPOを直接使用したQwen3.5-4Bについて紹介する。
修正された325例のSelectBench-v2テストセットでは、オリジナルのチェックポイントで22.46%から、DAPO-Ruleで25.54%、DAPO-DeepSeekで26.46%に厳格な成功を収めた。
論文 参考訳（メタデータ） (2026-07-22T12:45:04Z) - Automating Formal Verification with Reinforcement Learning and Recursive Inference [0.0]
我々はダフニーで検証可能な報酬(RLVR)と検証者誘導推論時間探索を用いてオープンソースモデルを訓練する。
固定ベースモデルでは、証明修正器を備えた完全な足場は、直接修理中の初期VeriCodingパイロットセットのパスレートを46.2%から69.2%に改善する。
Rust $texttcurve25519-dalek$検証プロジェクトから派生した,レポジトリスケールのLeanベンチマークであるDalek-Benchについても紹介します。
論文 参考訳（メタデータ） (2026-05-29T06:59:28Z) - Understanding and Mitigating Premature Confidence for Better LLM Reasoning [76.16007941549857]
現在の言語モデルからの思考の長い連鎖(CoT)は、しばしば論理的ギャップと不正な跳躍を含んでいる。
このような信号は、モデルの信頼性が推論中にどのように進化するかを示す。
これは、モデルを早期にコミットするのではなく、理由によってモデルの信頼性を更新するように訓練する強化学習の目標です。
論文 参考訳（メタデータ） (2026-05-23T04:42:45Z) - Correct Answers from Sound Reasoning: Verifiable Process Supervision for Language Models [94.68358825189738]
本稿では,予測精度と推論品質を協調的に最適化する検証済み領域の学習後フレームワークを提案する。
我々は,エンジン信号に対して推論ステップを確定的に検証できる制御テストベッドであるチェスのVPSを評価する。
VPSは、推論品質を著しく向上させながら精度を保ち、勝利率エラーを最大30%削減し、一貫性をほぼ飽和状態に回復する。
論文 参考訳（メタデータ） (2026-04-03T15:19:46Z) - CoVerRL: Breaking the Consensus Trap in Label-Free Reasoning via Generator-Verifier Co-Evolution [52.691495954442985]
CoVerRLは1つのモデルがジェネレータと検証ロールを交換するフレームワークで、各機能が他方をブートストラップする。
Qwen と Llama のモデルファミリーでの実験では、CoVerRL は数理推論のベンチマークで4.7-5.9% でラベルなしのベースラインを上回っている。
自己検証の精度は55%から85%以上改善され、両方の能力が真に共存することを確認した。
論文 参考訳（メタデータ） (2026-03-18T14:38:55Z) - GATES: Self-Distillation under Privileged Context with Consensus Gating [89.62339954332248]
我々は、監督が信頼できない環境で自己蒸留を研究する。
非対称な文脈で回答する文書に焦点をあてる。
複数の文書ベース推論トレースをサンプリングすることにより、教師のコンセンサスからオンラインでの監督を導出する。
論文 参考訳（メタデータ） (2026-02-24T05:56:20Z) - PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。
本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。
我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
論文 参考訳（メタデータ） (2020-10-06T15:47:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。