論文の概要: Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis
- arxiv url: http://arxiv.org/abs/2607.19795v1
- Date: Wed, 22 Jul 2026 06:20:36 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-23 18:51:37.991482
- Title: Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis
- Title（参考訳）: LLM誘導制約合成を用いたzkEVMの自動形式検証に向けて
- Abstract要約: ZkEVMは、オフチェーン実行の正しさを保証するゼロ知識を生成する。
微妙な実装上のバグは、意味的に欠陥のある状態を証明する有効な証明につながる可能性がある。
SMTソルバによる形式検証は、これを防止できるが、仕様によってボトルネックとなる。
Rustから実行可能なPython/Z3検証モデルを合成するフレームワークであるVeri Synthを提案する。
- 参考スコア（独自算出の注目度）: 14.825615940318038
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Zero-Knowledge Ethereum Virtual Machines (zkEVMs) secure Ethereum rollups by generating zero-knowledge proofs that guarantee off-chain execution correctness. However, subtle implementation bugs (e.g., incorrect gas accounting) can lead to valid proofs certifying semantically faulty states, thereby silently defeating cryptographic guarantees. Formal verification via SMT solvers can prevent this, but is bottlenecked by specification: current zkEVM development practice lacks automated methods to translate Rust opcode handlers into verification models. Current practices rely on unsustainable manual specifications, while LLM-based approaches suffer from hallucination and lack formal guarantees. To address this, we propose VeriSynth, a framework that synthesizes executable Python/Z3 verification models from Rust zkEVM code. VeriSynth enforces a hybrid paradigm: an LLM acts strictly as a formalization frontend to translate code into symbolic constraints, while an SMT solver serves as the correctness arbiter. To handle complex multi-component state transitions, VeriSynth integrates semantic decomposition, retrieval-grounded prompting, and verification-guided auto-repair into a closed-loop pipeline. We evaluate VeriSynth on the first source-level zkEVM verification benchmark, encompassing both correct and faulty opcode implementations. VeriSynth achieves a bug detection rate of over 90%, substantially outperforming direct and conversational LLM baselines, as well as a production-grade handwritten mutation-testing suite. Ablation studies confirm that each pipeline component is critical to the framework's overall effectiveness.
- Abstract（参考訳）: Zero-Knowledge Ethereum Virtual Machines (zkEVMs)は、オフチェーン実行の正しさを保証するゼロ知識証明を生成することでEthereumのロールアップを保証する。
しかし、微妙な実装バグ(例えば、不正なガス会計)は、意味的に欠陥のある状態を証明する有効な証明につながる可能性があるため、暗号的な保証を静かに破る。
現在のzkEVM開発プラクティスでは、Rustオペコードハンドラを検証モデルに変換する自動メソッドが欠如しています。
現在のプラクティスは持続不可能なマニュアル仕様に依存しているが、LCMベースのアプローチは幻覚に悩まされ、正式な保証が欠如している。
これを解決するために、Rust zkEVMコードから実行可能なPython/Z3検証モデルを合成するフレームワークであるVeriSynthを提案する。
VeriSynthはハイブリッドパラダイムを強制する: LLMは形式化フロントエンドとして厳密に機能し、SMTソルバは正当性アービタとして機能する。
複雑な多成分状態遷移を処理するために、VeriSynthはセマンティック分解、検索基底プロンプト、検証誘導オートリペアをクローズドループパイプラインに統合する。
We evaluate VeriSynth on the first source-level zkEVM benchmark, including a correct and faulty opcode implementation。
VeriSynthは90%以上のバグ検出率を達成し、直接的および会話的なLLMベースラインと、プロダクショングレードの手書き変異テストスイートを著しく上回っている。
アブレーション調査では、各パイプラインコンポーネントがフレームワーク全体の有効性に重要であることが確認されている。
関連論文リスト
- Weave of Formal Thought [51.56484100374058]
WoFT(Weave of Formal Thought)は、厳密な構文的検証と学習された構造的表現を結合したパラダイムである。
本稿では,非終端文法記号を直接生成にインターリーブするために,言語モデルを訓練する潜時可変微調整法を提案する。
Pythonでは、RWS目的のStarCoder2-3Bを微調整することで、テキストのみのSFTベースラインと比較して、トーケン毎のクロスエントロピーが14.3%削減される。
論文 参考訳（メタデータ） (2026-06-24T15:58:11Z) - Formal-Method-Guided Vibe Coding: Closing the Verification Loop on AI-Generated Safety-Critical Software Through Model-Driven Engineering [40.048798975817924]
バイブコーディングは高速で、低臨界のコンシューマソフトウェアには適しています。
DO-178C、IEC 61508、ISO 26262によって管理される安全クリティカルなシステムでは、認証への道は提供されない。
フォーマルな検証を通じてビブコーディングをガイドするクローズドループパイプラインであるForgeを紹介します。
論文 参考訳（メタデータ） (2026-06-21T10:01:45Z) - SimSD: Simple Speculative Decoding in Diffusion Language Models [61.33773959352141]
拡散大言語モデル (dLLMs) は、並列またはブロックワイド復号による高速な推論を提供する。
彼らのマスク付き言語モデリングの定式化は、標準的なトークンレベルの投機的復号法とは相容れないままである。
我々は,dLLMに時間的に有効なトークンレベルのコンテキストを付与する,SimSDと呼ばれるdLLMの投機的復号アルゴリズムを提案する。
提案手法は,平均生成品質を維持しつつ,最大7.46倍高い復号スループットを実現する。
論文 参考訳（メタデータ） (2026-06-01T17:46:46Z) - Towards Human-Like Interactive Speech Recognition With Agentic Correction and Semantic Evaluation [53.844308305341166]
単一パスのASRフロントエンドと意味的訂正,意図のルーティング,推論に基づく編集を組み合わせた閉ループフレームワークである textbfAgentic ASR を提案する。
複数言語、名前付き集中型、コードスイッチングベンチマークの実験は、反復的相互作用が意味的誤りを一貫して減少させることを示している。
論文 参考訳（メタデータ） (2026-05-28T06:23:31Z) - Agentic Model Checking [12.832868209928039]
本稿では,LLMエージェントと境界モデルチェックバックエンドを結合するパラダイムを提案する。
我々は、BMC-Agentのアプローチをインスタンス化し、CとRustのLLM生成カーネルおよびコンパイラコード上で評価する。
論文 参考訳（メタデータ） (2026-05-20T17:25:52Z) - LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。
CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
論文 参考訳（メタデータ） (2026-05-02T11:31:33Z) - Certified Program Synthesis with a Multi-Modal Verifier [5.998029529040967]
LeetProofは、Leanに埋め込まれたマルチモーダル検証ツールであるVelvet上に構築されたエージェントパイプラインである。
動的検証、自動証明、インタラクティブな証明スクリプティングを1つの基礎フレームワークで組み合わせる。
我々は、認定合成に関する先行研究から得られたベンチマークに基づいてLeetProofを評価する。
論文 参考訳（メタデータ） (2026-04-17T14:56:45Z) - SEVerA: Verified Synthesis of Self-Evolving Agents [12.9624447364193]
自己進化型エージェントフレームワークは、安全性や正確性の正式な保証を提供しない。
エージェントコード生成を制約付き学習問題として定式化し、ハードな形式仕様とソフトな目的とを組み合わせてタスクユーティリティをキャプチャする。
探索はFGGMコールを含む候補パラメトリックプログラムを合成し、検証は全てのパラメータ値に対する厳しい制約に関して正当性を証明し、制約のない学習に還元する。
論文 参考訳（メタデータ） (2026-03-26T07:32:20Z) - zkCraft: Prompt-Guided LLM as a Zero-Shot Mutation Pattern Oracle for TCCT-Powered ZK Fuzzing [7.274627641804014]
zkCraftは決定論的、R1CS対応のローカライゼーションと証明付き検索を組み合わせて意味的不整合を検出するフレームワークである。
証明付きローカライゼーションは, 偽陽性が低い多彩な下限および過制約の断層を検出し, コストのかかるソルバ相互作用を低減できることを示す。
論文 参考訳（メタデータ） (2026-01-31T11:31:00Z) - From Completion to Editing: Unlocking Context-Aware Code Infilling via Search-and-Replace Instruction Tuning [81.97788535387286]
本稿では,エージェントによる検証・編集機構を統一された単一パス推論プロセスに内部化するフレームワークを提案する。
最小限のデータで、SRI-Coderは、ChatモデルがBaseモデルの完了性能を上回ることができる。
FIMスタイルのチューニングとは異なり、SRIは一般的なコーディング能力を保持し、標準のFIMに匹敵する推論遅延を維持する。
論文 参考訳（メタデータ） (2026-01-19T20:33:53Z) - $\ exttt{SEM-CTRL}$: Semantically Controlled Decoding [53.86639808659575]
$texttSEM-CTRL$は、LLMデコーダに直接、リッチなコンテキスト依存制約とタスクおよびインスタンス固有のセマンティクスを強制する統一的なアプローチである。
texttSEM-CTRL$は、小さな訓練済みのLLMがより大きな変種や最先端の推論モデルよりも効率的に性能を向上することを可能にする。
論文 参考訳（メタデータ） (2025-03-03T18:33:46Z) - Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。
SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。
我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
論文 参考訳（メタデータ） (2024-10-21T08:15:45Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。