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

• arxiv url: http://arxiv.org/abs/2607.22972v1
• Date: Sat, 25 Jul 2026 00:42:04 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-28 22:34:14.952997
• Title: Learned Interventions in Lean 4 grind
• Title（参考訳）: Lean 4 grindで学んだ介入
• Authors: Evan Wang, Simon Chess, Sophie Szeto, Theodore Meek,
• Abstract要約: Lean4のグラインド戦術は、クロージャ、マーチング、ケース分割を1つの自動化されたソルバに組み合わせます。 定理証明戦術における学習は、いつ、どのように境界探索に費やすかを決定するメカニズムとして最も効果的であることを示す。
• 参考スコア（独自算出の注目度）: 1.4174475093445238
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Lean~4's \grind{} tactic combines congruence closure, \ematch{}ing, 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 \ematch{} 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's \grind{} 戦術は、コングルーエンスクロージャ、 \ematch{}ing とケーススプリットを1つの自動解法に組み合わせ、そのような解法と同様に、何のインスタンス化とケーススプリットの場所を決定するために手作業のヒューリスティックに依存する。 これらのヒューリスティックは学習の誘惑的なターゲットであるが、これは、 \grind{} の探索が非単調であるからであり、ある証明が別の証明を破る助けとなる学習ヒューリスティックであり、常にオンの置換は通常ゼロに近い網を張るからである。 我々は、ストック \grind{} が既に失敗した後のみ、学習した介入を呼び起こすことによってこれを回避している: 失敗トリガーされたカスケードは、建設によって、既にある証明 \grind{} を失うことができない。 これを \grind{} の内部決定の2つに適用する。 コストを意識した \ematch{} フィルタは,問題を少し解決し,約 5 % 高速化する。 ルックアヘッドのステップは、それ以外は5つの定理を証明します。 機能ベースの4つのモデルにおいて、正しいケース分割を静的に予測することは、スプリットが爆発するかどうかは、特徴がキャプチャされない実行時プロパティであるので、ランダムにしかならない。 この結果から, 定理証明手法における学習は, 信頼性のある記号的フォールバックを背景として, 有界探索をいつ, どのように使うかを決定するメカニズムとして最も効果的であることが示唆された。

関連論文リスト

• 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)
• Provable Scaling Laws for the Test-Time Compute of Large Language Models [84.00141420901038]
  本研究では,大規模言語モデルのテスト時間計算において,証明可能なスケーリング法則を享受する2つのアルゴリズムを提案する。 1つは2段階ノックアウト方式のアルゴリズムで、各候補は複数の相手に対して平均勝利率で評価される。 もう1つは2段階のリーグ方式のアルゴリズムで、各候補は複数の相手に対して平均勝利率で評価される。
  論文  参考訳（メタデータ） (2024-11-29T05:29:47Z)
• LegendreTron: Uprising Proper Multiclass Loss Learning [22.567234503869845]
  損失関数は教師付き学習の基盤として機能し、しばしばモデル開発の前に選択される。 最近の研究は、損失とモデルを共同で引き起こそうとしている。 sc LegendreTron は,多クラス問題に対するアンフォプロペラの正準損失と確率を共同で学習する,新規かつ実用的な方法である。
  論文  参考訳（メタデータ） (2023-01-27T13:10:45Z)
• 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)

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

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