論文の概要: Learned Interventions in Lean 4 grind

• arxiv url: http://arxiv.org/abs/2607.22972v2
• Date: Tue, 28 Jul 2026 05:10:29 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-29 14:13:57.668113
• Title: Learned Interventions in Lean 4 grind
• Title（参考訳）: Lean 4 grindで学んだ介入
• Abstract要約: Lean 4のグラインド戦術は、クロージャ、Eマッチング、ケース分割を1つの自動化されたソルバに組み合わせます。 定理証明戦術における学習は、いつ、どのように境界探索に費やすかを決定するメカニズムとして最も効果的であることを示す。
• 参考スコア（独自算出の注目度）: 1.4174475093445238
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Lean 4's grind tactic combines congruence closure, E-matching, and case-splitting into a single automated solver, and like any such solver, it relies on hand-tuned heuristics to decide what to instantiate and where to case-split. These heuristics are tempting targets for learning, but there is a catch: because grind's search is non-monotone, a learned heuristic that helps one proof can break another, and an always-on replacement usually nets out near zero. We avoid this by invoking a learned intervention only after stock grind has already failed: a failure-triggered cascade that, by construction, cannot lose a proof grind already had. We apply it to two of grind's internal decisions. A cost-aware E-matching filter solves slightly more problems and runs about 5% faster. A lookahead step proves five theorems it otherwise times out on. We also report the negative result that motivated the design: across four feature-based models, statically predicting the correct case split is no better than random, because whether a split explodes is a runtime property that the features do not capture. Our results suggest that learning within theorem-proving tactics is most effective as a mechanism for deciding when and how to spend bounded search, backed by a reliable symbolic fallback.
• Abstract（参考訳）: Lean 4のグラインド戦術は、一貫性のクロージャ、Eマッチング、ケース分割を1つの自動化されたソルバに組み合わせ、そのようなソルバと同様に、何をインスタンス化し、どこでケース分割するかを決定するために手動のヒューリスティックに依存します。 これらのヒューリスティックは学習の誘惑的なターゲットであるが、グラインドの探索は非モノトンであり、ある証明が別の証明を破るのに役立つ学習ヒューリスティックであり、常にオンの置換は通常ゼロに近い網を張る。 我々は、ストックグラインドが既に失敗した後のみ、学習した介入を呼び起こすことによって、これを回避している: 失敗に悩まされたカスケードは、建設によって、既にグラインドが持っている証拠を失うことはできない。 我々はそれをグラインドの内部決定の2つに適用する。 コスト対応のEマッチングフィルタは、より問題を少し解決し、約5%高速に動作します。 ルックアヘッドのステップは、それ以外は5つの定理を証明する。 機能ベースの4つのモデルにおいて、正しいケース分割を静的に予測することは、スプリットが爆発するかどうかは、特徴がキャプチャされない実行時プロパティであるので、ランダムにしかならない。 この結果から, 定理証明手法における学習は, 信頼性の高い記号的フォールバックを背景として, 有界探索をいつ, どのように使うかを決定するメカニズムとして最も効果的であることが示唆された。

関連論文リスト

• Prompt-Model Interaction Reaches the Fixed Points: A deterministic, task-free structural readout -- and the factorizations of it that failed [0.0]
  ショートウィンドウ argmax map x_t+1 = argmax_x p(x | x_t-1, x_t) の固定点構造は96 から始まる。 6つのモデルのうち4つは、ウィンドウ16で完全に失われている。 第一に、相互作用は全等級でこの読み出しに達する:条件付けの9つのトークンは、そのほとんどにわたって固定点分数を動かす。
  論文  参考訳（メタデータ） (2026-08-21T17:25:18Z)
• Test-Time Scaling in the Wild: Why Exploitation, Not Exploration, Is the Bottleneck [1.4991111518581999]
  テストタイムスケーリング(TTS)は、追加の推論計算を使用することで、言語モデルの出力を改善する。 5世代ベンチマークで5つのTSファミリーの計算正規化比較を行った。
  論文  参考訳（メタデータ） (2026-08-19T13:59:53Z)
• One Run Is Not an Idea: The Implementation Lottery in Automated Research [27.31956713090655]
  自動研究システムは、アーティファクトの提供と、どのアイデアを保持、転送、追跡するかを決定するために、実験的なスコアを使用する。 1ランはアイデアの1つの実装をスコアする。しかし、1ランはアイデアの1つの実装をスコアする。 メカニズムに関する信念を更新するたびに、ミスマッチは構造的になります。 emphIdea Reliability Auditは、候補カードの検証と凍結、新しいセッション実装のサンプリング、結果のブラインドフィデリティラベルの使用、保存されたアーティファクトの再実行によって、インフィリアの信頼性を測定する。
  論文  参考訳（メタデータ） (2026-07-29T08:06:43Z)
• REFLECT: Intervention-Supported Error Attribution for Silent Failures in LLM Agent Traces [10.98846592145896]
  大規模言語モデル(LLM)エージェントは、長いプラン・アンド・エグゼクティブトレースを通じて複雑なタスクを解決するが、完了したトレース内のエラーを見つける能力はまだ遅れている。 本稿では,このギャップを解消する手法として,候補となるエラーステップの診断,診断固有のパッチによるリプレイによるテスト,および検証結果のフリップを比較的証拠として用いて最終帰属を洗練させる手法を提案する。
  論文  参考訳（メタデータ） (2026-06-08T06:11:57Z)
• Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement [69.77146194380488]
  私たちはGoedel-Architectを紹介します。これは、青写真の生成と洗練に焦点を当てたLean 4で証明された公式な定理のためのフレームワークです。 Goedel-ArchitectがMiniF2Fテストで99.2%パス@1、PutnamBenchで75.6%パス@1を達成した。 これは、同等のオープンソースパイプラインよりも500倍低い価格で、オープンソースパイプラインの最先端のパフォーマンスを示している。
  論文  参考訳（メタデータ） (2026-06-04T17:54:44Z)
• Efficient Test-Time Inference via Deterministic Exploration of Truncated Decoding Trees [68.04613115686509]
  自己整合性は、複数の推論トレースを並列にサンプリングし、投票することで、推論時間のパフォーマンスを向上させる。 そこで本研究では,切り落された標本を伐採木として扱う決定論的復号法であるDLE(Distinct Leafion)を提案する。 DLEは高品質な推論トレースを調査し、数学、コーディング、一般的な推論タスクのパフォーマンスを向上させる。
  論文  参考訳（メタデータ） (2026-04-22T12:42:03Z)
• Yanasse: Finding New Proofs from Deep Vision's Analogies, Part 1 [51.56484100374058]
  システムはマドリブの27の上位領域の戦術的利用分布を抽出する。 zスコアを計算して、ソースエリアで多用されるが、ターゲットエリアで稀または欠落している戦術を特定する。 これは、GPUアクセラレーションされたNPハードアナログを用いて、ソースとターゲットの証明状態と一致する。
  論文  参考訳（メタデータ） (2026-04-19T03:27:16Z)
• Test-Time Scaling with Diffusion Language Models via Reward-Guided Stitching [66.39914384073145]
  本稿では,安価な拡散サンプリング推論をステップレベル候補の再利用プールに変換する自己整合性フレームワークを提案する。 ステップレベルの再結合は、難しい問題に対して最も有益であることがわかった。 トレーニング不要のフレームワークは、6つの数学およびコーディングタスクの平均精度を最大2倍改善します。
  論文  参考訳（メタデータ） (2026-02-26T11:08:39Z)
• Answer Convergence as a Signal for Early Stopping in Reasoning [7.51755942515969]
  大型言語モデル(LLM)における思考の連鎖(CoT)の促進 提案手法は,(1)応答整合性による早期停止,(2)終末信号発生確率の向上,(3)内部アクティベーションに基づいていつ停止するかを学習する教師付き手法である。
  論文  参考訳（メタデータ） (2025-06-03T07:20:54Z)
• Provable Scaling Laws for the Test-Time Compute of Large Language Models [84.00141420901038]
  本研究では,大規模言語モデルのテスト時間計算において,証明可能なスケーリング法則を享受する2つのアルゴリズムを提案する。 1つは2段階ノックアウト方式のアルゴリズムで、各候補は複数の相手に対して平均勝利率で評価される。 もう1つは2段階のリーグ方式のアルゴリズムで、各候補は複数の相手に対して平均勝利率で評価される。
  論文  参考訳（メタデータ） (2024-11-29T05:29:47Z)
• Finding Transformer Circuits with Edge Pruning [71.12127707678961]
  自動回路発見の効率的かつスケーラブルなソリューションとしてエッジプルーニングを提案する。 本手法は,従来の手法に比べてエッジ数の半分未満のGPT-2の回路を探索する。 その効率のおかげで、Edge PruningをCodeLlama-13Bにスケールしました。
  論文  参考訳（メタデータ） (2024-06-24T16:40:54Z)
• How to Construct Perfect and Worse-than-Coin-Flip Spoofing Countermeasures: A Word of Warning on Shortcut Learning [20.486639064376014]
  ショートカット学習(英: Shortcut learning、またはClever Hans effect)とは、学習エージェントがデータに存在する急激な相関を学習し、バイアスのあるモデルをもたらす状況を指す。 本研究では, 深層学習に基づくスプーフィング対策(CM)において, ある発話がスプーフィングされているか否かを予測するショートカットの発見に焦点をあてる。
  論文  参考訳（メタデータ） (2023-05-31T15:58:37Z)
• LegendreTron: Uprising Proper Multiclass Loss Learning [22.567234503869845]
  損失関数は教師付き学習の基盤として機能し、しばしばモデル開発の前に選択される。 最近の研究は、損失とモデルを共同で引き起こそうとしている。 sc LegendreTron は,多クラス問題に対するアンフォプロペラの正準損失と確率を共同で学習する,新規かつ実用的な方法である。
  論文  参考訳（メタデータ） (2023-01-27T13:10:45Z)
• Don't Explain Noise: Robust Counterfactuals for Randomized Ensembles [50.81061839052459]
  我々は確率論的問題として、堅牢な対実的説明の生成を定式化する。 アンサンブルモデルのロバスト性とベース学習者のロバスト性との関係を示す。 本手法は, 反実的説明から初期観測までの距離をわずかに増加させるだけで, 高いロバスト性を実現する。
  論文  参考訳（メタデータ） (2022-05-27T17:28:54Z)
• Search Methods for Sufficient, Socially-Aligned Feature Importance Explanations with In-Distribution Counterfactuals [72.00815192668193]
  特徴重要度(FI)推定は一般的な説明形式であり、テスト時に特定の入力特徴を除去することによって生じるモデル信頼度の変化を計算し、評価することが一般的である。 FIに基づく説明の未探索次元についていくつかの考察を行い、この説明形式に対する概念的および実証的な改善を提供する。
  論文  参考訳（メタデータ） (2021-06-01T20:36:48Z)
• Taking a hint: How to leverage loss predictors in contextual bandits? [63.546913998407405]
  我々は,損失予測の助けを借りて,文脈的包帯における学習を研究する。 最適な後悔は$mathcalO(minsqrtT, sqrtmathcalETfrac13)$である。
  論文  参考訳（メタデータ） (2020-03-04T07:36:38Z)
• Supervised Learning: No Loss No Cry [51.07683542418145]
  教師付き学習は最小化するために損失関数の仕様を必要とする。 本稿では,Kakade et al. (2011)のSLIsotronアルゴリズムを新しいレンズで再検討する。 損失を学習するための原則的な手順をいかに提供するかを示す。
  論文  参考訳（メタデータ） (2020-02-10T05:30:52Z)

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

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