論文の概要: Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4

• arxiv url: http://arxiv.org/abs/2605.25556v2
• Date: Wed, 27 May 2026 19:06:07 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-30 02:45:54.642513
• Title: Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4
• Title（参考訳）: リーン4の効果的な戦術探索のためのスナップショッティング
• Authors: Austin Shen, Yunong Shi,
• Abstract要約: これは、一度精巧な証明状態をキャプチャし、Lean 4言語サーバーへの小さな拡張を通じてブランチ間で再利用します。 48のミニF2F-v2問題に対して,本手法は標準的なフォールバックよりも5.6～50倍の高速化を実現する。
• 参考スコア（独自算出の注目度）: 1.2816802110958607
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Automated theorem proving systems built on Lean 4 increasingly rely on parallel tactic search over partially specified proofs, such as those generated by Draft-Sketch-Prove (DSP) pipelines. In current systems, each search branch reconstructs a proof state by re-running elaboration, leading to substantial per-branch overhead. In Lean 4 with Mathlib, this cost has two components: (1) import loading, which deserializes pre-compiled libraries (~60 s per branch); and (2) theorem-body elaboration, which re-checks the theorem context up to the target goal (estimated 18-735 s depending on proof complexity). Together, these account for >99% of per-branch wall time, making portfolio-based search impractical at scale. We observe that this overhead arises from a mismatch between the structure of proof search and its execution model: branching is implemented via repeated reconstruction of proof states rather than direct reuse. To address this, we introduce proof-state snapshotting, which captures the elaborated proof state once and reuses it across branches via a small extension to the Lean 4 language server. Across 48 miniF2F-v2 problems (45 prove-phase benchmarks and 3 full end-to-end runs), our approach achieves a 5.6-50x wall-time speedup over the standard fallback (average 14x, median 9.7x). Speedup increases with the number of proof branches. Our method is orthogonal to import-level caching (e.g., Kimina Lean Server), which avoids import loading but not theorem-body elaboration. The patched Lean binary and the Snapshot-DSP pipeline will be released as open source upon publication.
• Abstract（参考訳）: Lean 4上に構築された自動定理証明システムは、Draft-Sketch-Prove(DSP)パイプラインで生成されたような、部分的に指定された証明よりも、ますます並列的な戦術探索に依存している。 現在のシステムでは、各探索枝はエラボレーションを再実行することで証明状態を再構築し、実質的なブランチ毎のオーバーヘッドをもたらす。 このコストは、(1)事前コンパイルされたライブラリ(ブランチあたり約60秒)をデシリアライズするインポートローディング(import loading)、(2)定理ボディのエラボレーション(the theorem-body elaboration)、(2)定理コンテキストを目標目標(証明の複雑さに応じて18～735秒)まで再チェックする(estimated 18～735秒)。 同時に、これらはブランチごとのウォールタイムの99%以上を占めており、ポートフォリオベースの検索を大規模に非現実的にしている。 このオーバヘッドは,証明検索の構造と実行モデルとのミスマッチから生じることを観察する。 これを解決するために、実証状態スナップショットを導入し、一度精巧な証明状態をキャプチャし、Lean 4言語サーバーへの小さな拡張を通じてブランチ間で再利用します。 48 の miniF2F-v2 問題 (45 の証明段階ベンチマークと 3 の完全なエンドツーエンド実行) に対して,本手法は標準フォールバック(平均 14 倍,中央 9.7 倍)よりも5.6-50 倍のウォールタイム高速化を実現する。 証明ブランチの数によってスピードアップが増加する。 本手法は,輸入レベルのキャッシュ(例えばKimina Lean Server)に直交する。 パッチされたLeanバイナリとSnapshot-DSPパイプラインは、公開時にオープンソースとしてリリースされる。

関連論文リスト

• OProver: A Unified Framework for Agentic Formal Theorem Proving [33.14658302112269]
  OProverは、Lean 4.0で証明された代理的な形式的な反復定理のための統一されたフレームワークである。 エージェント証明を実行し、新たに証明された証明をOProofsと検索メモリにインデックスし、修理軌跡をSFTデータとして使用し、未解決のハードケースをRLに使用する。 OProver-32BはMiniF2F (93.3%)、ProverBench (58.2%)、PutnamBench (11.3%)で最高のパス@32を獲得し、MathOlympiad (22.8%)、ProofNet (33.2%)で上位にランクインしている。
  論文  参考訳（メタデータ） (2026-05-17T06:39:05Z)
• LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving [7.326381497366569]
  リーン4の定理を証明するには、しばしば、簡潔な証明を可能にするライブラリの補題の散在を識別する必要がある。 本稿では,このタスクのための2モード検索システムであるLeanSearch v2を紹介する。
  論文  参考訳（メタデータ） (2026-05-13T08:04:57Z)
• Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification [34.98335927187393]
  大規模言語モデル(LLM)は可塑性コードを生成することができるが、正確性には限界がある。 本稿では,Lean4における自動コード検証のための階層的証明検索フレームワークを提案する。 Goedel-Code-Prover-8Bは、分解と完了の両方のための単一の統一ポリシーです。
  論文  参考訳（メタデータ） (2026-03-18T18:42:04Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。 提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
  論文  参考訳（メタデータ） (2025-11-26T06:39:19Z)
• dParallel: Learnable Parallel Decoding for dLLMs [77.24184219948337]
  拡散大言語モデル(dLLM)は並列トークン予測と低推論遅延を提供する。 既存のオープンソースモデルは、パフォーマンスを確保するためにトークン長のデコードステップをほとんど必要としています。 高速サンプリングのためにdLLMs固有の並列性を解き放つシンプルで効果的な方法であるdParallelを導入する。
  論文  参考訳（メタデータ） (2025-09-30T16:32:52Z)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  証明の進捗を予測する手法であるLeanProgressを紹介します。 実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
  論文  参考訳（メタデータ） (2025-02-25T07:46:36Z)
• ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。 本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。 また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• Proving Theorems Recursively [80.42431358105482]
  本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。 従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。 また,POETRYが検出した最大証明長は10～26。
  論文  参考訳（メタデータ） (2024-05-23T10:35:08Z)

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

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