論文の概要: BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints
- arxiv url: http://arxiv.org/abs/2607.28110v1
- Date: Thu, 30 Jul 2026 12:17:31 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-31 21:37:00.551271
- Title: BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints
- Title（参考訳）: BlueprintRepair: 失敗に終わったリーンプロトタイプのローカル編集
- Authors: Ruslan Khrulev,
- Abstract要約: LLMベースのリーン証明システムは、ますますブループリントとして証明を組織化しています。
BlueprintRepairは、モデルがこのグラフを10のスキーマチェックされたローカル操作で変更できる修復インターフェースです。
また、BlueprintTraceは142個の制御された障害のベンチマークで、完全に許容され、修復軌道が拒否されている。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: LLM-based Lean proving systems increasingly organize a proof as a blueprint: a dependency graph of formal statements. We introduce BlueprintRepair, a repair interface that lets a model change this graph through ten schema-checked local operations. An operation names the node it edits, so the target theorem cannot be changed. Lean checks every applied change, and an accepted repair must declare every blueprint lemma its proof uses. We also construct BlueprintTrace, a benchmark of 142 controlled failures with complete accepted and rejected repair trajectories. We compare typed edits, exact source patches, and complete module rewrites under matched source, feedback, model, and budget, one episode per state and interface. With DeepSeek-V4-Flash, the three interfaces solve almost the same number of the benchmark's localized failures. Typed repair is the cheapest per solved state (patching is 1.30x as expensive, rewriting 2.06x), and within 10,000 completion tokens per task it reaches almost all of its final coverage, while both free-form interfaces are well behind. A second model, Qwen3.6-Flash, solves fewer states but keeps typed repair cheapest, puts it ahead on the proof-authoring states, and repeats the localized pattern.
- Abstract（参考訳）: LLMベースのリーン証明システムは、ますますブループリントとして、形式的なステートメントの依存性グラフとして、証明を組織化しています。
BlueprintRepairは、モデルがこのグラフを10のスキーマチェックされたローカル操作で変更できる修復インターフェースです。
操作はそれが編集するノードを命名するので、ターゲット定理は変更できない。
リーンは適用された変更をすべてチェックし、承認された修復は、その証明が使用するブループリントの補題をすべて宣言しなければならない。
また、BlueprintTraceは142個の制御された障害のベンチマークで、完全に許容され、修復軌道が拒否されている。
タイプされた編集、正確なソースパッチ、そして、マッチしたソース、フィードバック、モデル、予算の下での完全なモジュール書き換えを比較します。
DeepSeek-V4-Flashでは、3つのインターフェースがベンチマークのローカライズされた障害のほとんど同じ数を解決している。
型付き修復は、解決された状態当たりで最も安価(パッチは1.30倍、書き換えは2.06倍)で、タスク毎の完了トークン1万個以内は最終カバレッジのほぼ全てに到達し、自由形式のインターフェースはどちらもかなり遅れている。
第2のモデルであるQwen3.6-Flashは、より少ない状態を解くが、型付き修復を最も安く保ち、証明オーサリング状態に先んじ、局所化パターンを繰り返す。
関連論文リスト
- One Rewrite to Fix Them All? Type-Aware Repair Allocation for Text-to-Image Prompt Optimization [59.164665622252016]
テキスト・トゥ・イメージ(T2I)ジェネレータは、間違ったカウント、スワップされた属性、あいまいな関係、不可解なテキストを生成し、そのプロンプトに忠実に従わないことが多い。
Prompt最適化は、ユーザプロンプトを書き換えて、ジェネレータの再トレーニングを必要としないことで、このような障害を修復する。
失敗する各命題は、結果のローカル制約が1つの実行可能なプロンプトにコンパイルされる前に、タイプ条件の修復演算子にルーティングされる。
論文 参考訳（メタデータ） (2026-07-21T05:31:43Z) - From Failing to Passing: Evolving Natural Language Prompt Optimization Rules for LLM Code Generation [11.454560846406698]
本稿では,自然言語変換ルールの集合を特定し,進化させる検索ベースアプローチを提案する。
次に、進化した変換ルールと実行フィードバックの修復を組み合わせた、段階的な修復パイプラインFIXを提案する。
以上の結果から,DualFixはベースライン障害の最大30%を回復し,SelfFixの3～5倍の障害を修正した。
論文 参考訳（メタデータ） (2026-07-06T14:10:56Z) - Can Code Specify a System Precisely Enough to Formally Verify It? [0.0]
本報告では,業務用レストラン・ポイント・オブ・セールシステムの支払ワークフローを実運用ソフトウェアで評価する。
コアプロトコルは、正確に定義された障害モデルの下で手作りのラインアクティベートされたモデルに対して正しい。
生産用サンドボックスの1つのプローブは、全リカバリはしごを到達不能にする応答形状のばらつきを露呈した。
論文 参考訳（メタデータ） (2026-07-06T13:39:00Z) - Characterizing and Bridging the Diagnostic Gap in eBPF Verifier Rejections [5.3302893005312955]
eBPFにより、開発者はLinuxカーネル内でカスタムプログラムを実行できる。
検証者がプログラムを拒否すると、不確実なエラーにより修復が困難になる。
証明が確立された場所と,検証ログから失われていた場所を再構築するbpfixを提案する。
論文 参考訳（メタデータ） (2026-07-02T20:33:32Z) - PairCoder++: Pair Programming as a Universal Paradigm for Verified Code-Driven Multimodal and Structured-Artifact Generation [51.92442051257354]
PairCoderは、実行のみではなく、完全な公式メトリックスイート上で、アーティファクトが検証可能なすべてのベンチマークを本質的に改善する。
TikZのコンパイルレートは、各モデルで10から30ポイント、シングルモデルの2.9から9.2倍である。
論文 参考訳（メタデータ） (2026-07-02T08:36:02Z) - 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) - ContraFix: Agentic Vulnerability Repair via Differential Runtime Evidence and Skill Reuse [10.503895811137095]
大規模言語モデル(LLM)エージェントは、自動脆弱性修復にますます利用されている。
最近の実証的な結果は、これらのエージェントがいまだに現実世界の脆弱性と戦っていることを示している。
ContraFixは、再利用可能な修復スキルとランタイムエビデンスを結合するエージェントフレームワークである。
論文 参考訳（メタデータ） (2026-05-17T13:48:25Z) - M2F: Automated Formalization of Mathematical Literature at Scale [24.360952996585045]
M2F(Math-to-Formal)は、リーンにおけるエンドツーエンドのプロジェクトスケールの自動形式化のための最初のエージェントフレームワークです。
約3週間で、M2Fは479ページの教科書から153,853行のリーンライブラリに変換する。
これは、通常数ヶ月または数年の専門的な努力を必要とするペースで教科書スケールの形式化を表す。
論文 参考訳（メタデータ） (2026-02-19T02:25:23Z) - PrefixNLI: Detecting Factual Inconsistencies as Soon as They Arise [60.63315470285562]
MiniTruePrefixesは、テキストプレフィックスよりも事実上の矛盾をよりよく検出する、新しい特殊モデルである。
制御されたデコードフレームワークにMiniTruePrefixesを組み込むことで,抽象的な要約における現実の一貫性が大幅に向上することを示す。
論文 参考訳（メタデータ） (2025-11-03T09:07:44Z) - Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs [79.74676890436174]
本稿では,障害の局所化と修復のためのオラクルとして形式仕様を用いたDafny用のAPRツールを提案する。
プログラム内の各ステートメントの状態を決定するために、Hoareロジックの使用を含む一連のステップを通じて、障害をローカライズします。
また, GPT-4o miniが74.18%と高い修理成功率を示した。
論文 参考訳（メタデータ） (2025-07-04T15:36:12Z) - Memory-Based Model Editing at Scale [102.28475739907498]
既存のモデルエディタは、編集対象のスコープを正確にモデル化するのに苦労する。
SERAC(Retrieval-Augmented Counterfactal Model)を用いた半パラメトリック編集を提案する。
SERACは、編集を明示的なメモリに格納し、必要に応じてベースモデルの予測を変更できるように、それらを推論することを学ぶ。
論文 参考訳（メタデータ） (2022-06-13T23:40:34Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。