論文の概要: Efficient Branch-and-Bound Testing and Verification of zkVMs
- arxiv url: http://arxiv.org/abs/2609.15020v1
- Date: Mon, 14 Sep 2026 04:35:11 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-16 07:15:06.072718
- Title: Efficient Branch-and-Bound Testing and Verification of zkVMs
- Title（参考訳）: 分岐境界試験の効率化とzkVMの検証
- Abstract要約: 完全自動検証およびバグ検出フレームワークであるZEBRAを提案する。
ZEBRAは、zkVM検証を標準トレース空間上の解集合濃度問題に還元する。
ZEBRAは11のゼロデイバグを発見した。
- 参考スコア（独自算出の注目度）: 26.60003840008197
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Zero-knowledge virtual machines (zkVMs) enable verifiable execution of general-purpose programs by translating virtual machine semantics into algebraic constraints over execution traces. The correctness of these constraints is critical: a single incorrect constraint can admit forged proofs (under-constrained) or reject valid executions (over-constrained). Existing approaches do not provide meaningful guarantees at production scale: fuzzers and unit tests often miss bugs, SMT solvers struggle with the size and nonlinearity of constraints, and theorem provers require substantial manual effort. We present ZEBRA, a fully automated verification and bug-detection framework: for a given program and input, the constraint must admit exactly one valid execution trace - no more and no fewer. This reduces zkVM verification to a solution-set cardinality problem over a canonical trace space, where redundancies such as null-row padding and non-deterministic permutations are eliminated prior to counting. To compute cardinality tractably, ZEBRA lifts analysis from finite-field witnesses to an integer interval lattice, exploiting a structural sparsity property of zkVM constraints: across 5 real-world zkVMs, constraints utilize only 14.0% of their theoretical connectivity capacity on average. This sparsity enables tight interval propagation with limited approximation error. ZEBRA performs a parallel branch-and-bound search that either produces a concrete counter-example or certifies the absence of violations within a bounded region. We evaluate ZEBRA on five real-world zkVMs. ZEBRA discovers 11 zero-day bugs; 6 have already been independently confirmed and 3 have been fixed by developers. Compared to SMT-based verification, ZEBRA is 51.5x faster, verifies 16.5 percentage point more instances, and its range verification provides up to 63x efficiency gain over repeated single-input verification.
- Abstract（参考訳）: Zero-knowledge Virtual Machine (zkVMs) は、仮想マシンのセマンティクスを実行トレース上の代数的制約に変換することによって、汎用プログラムの検証を可能にする。
単一の誤った制約は、偽の証明(制約下)を受け入れたり、有効な実行(制約過剰)を拒否することができる。
ファジッターと単体テストはしばしばバグを見逃し、SMTソルバは制約の大きさと非線形性に苦しむ。
私たちは、完全に自動化された検証とバグ検出のフレームワークであるZEBRAを紹介します。
これにより、zkVM検証は標準トレース空間上の解集合濃度問題に還元され、ヌルローパディングや非決定論的置換といった冗長性はカウント前に排除される。
濃度を計算するために、ZEBRAは有限場証人から整数間隔格子への解析を引き上げ、zkVMの制約の構造的空間性を利用する:5つの実世界のzkVMにおいて、平均で理論接続能力の14.0%しか利用しない。
この間隔は、近似誤差を限定した狭い間隔の伝搬を可能にする。
ZEBRAは、具体的な反例を生成するか、境界領域内で違反がないことを証明した並列分岐境界探索を実行する。
実世界の5つのzkVM上でZEBRAを評価する。
ZEBRAは11のゼロデイバグを発見した。
SMTベースの検証と比較して、ZEBRAは51.5倍高速で、16.5ポイント以上のインスタンスを検証し、その範囲検証は、繰り返しシングルインプットの検証よりも最大63倍の効率向上をもたらす。
関連論文リスト
- Constraint-Aware Synthetic Tabular Data Generation via Inter-Column Constraint Discovery with LLM Agents [3.7680093320209553]
本研究では,3つのカラム間制約家族の発見と実施について検討する。
私たちの統合ツール・グラウンドド・ワークフローは、3つ全てをマシン実行可能な仮説として表現しています。
論文 参考訳（メタデータ） (2026-08-15T08:19:54Z) - Constraint-Anchored Reasoning Traces [9.39195684989942]
MLLM(Autoregressive Multimodal Large Language Model)は、ミススノーボールに悩まされる。
最先端のオープンソースMLLMでは、最初のエラーが発生すると、これらのケースの65%で、残りのステップすべてにわたって推論カスケードが失敗する。
本稿では,MLLMを学習し,言語推論のステップを記号的制約アサーションでインターリーブする,ニューロシンボリック・シンボリック・フレームワークであるConstraint-Anchored Reasoning Traces (CART)を提案する。
論文 参考訳（メタデータ） (2026-07-18T09:24:45Z) - LinAlg-Bench: A Forensic Benchmark Revealing Structural Failure Modes in LLM Mathematical Reasoning [0.0]
LinAlg-Benchは、構造化線形代数計算における10のフロンティア大言語モデルを評価する診断ベンチマークである。
ベンチマークは、6600モデルのアウトプットを徹底的に評価する。
論文 参考訳（メタデータ） (2026-05-15T22:30:57Z) - CCTU: A Benchmark for Tool Use under Complex Constraints [66.87622847854337]
複雑な制約下での大規模言語モデル(LLM)を評価するためのベンチマークであるCCTUを紹介する。
ベンチマークは、さまざまなツール使用シナリオに対して、慎重にキュレートされ、挑戦的なテストケースが200から成っている。
ステップレベルの検証を行い、コンプライアンスを強制する実行可能な制約検証モジュールを開発する。
論文 参考訳（メタデータ） (2026-03-16T14:05:13Z) - 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) - CARE What Fails: Contrastive Anchored-REflection for Verifiable Multimodal [84.71254539482369]
検証可能な報酬を伴うグループ相対的強化学習(RLVR)は、しばしば、すでに失敗している最も情報に富むデータを浪費する。
エラーを監督するマルチモーダル推論のための,障害中心のポストトレーニングフレームワークであるCAREを提案する。
CAREは正確さを改善し、スムーズさをトレーニングすると同時に、障害からの学習信号のシェアを明示的に増やします。
論文 参考訳（メタデータ） (2025-12-22T16:34:21Z) - Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification [9.733843486234878]
最先端ニューラルネットワーク(NN)検証は、分岐とバウンド(BaB)の手順を高速なバウンディング技術で適用することが、多くの挑戦的な検証特性に対処する上で重要な役割を果たしていることを示す。
本稿では,NN検証の有効性を高めるために,スケーラブルで効率的な手法のクラスである線形制約駆動型クリッピングフレームワークを紹介する。
論文 参考訳（メタデータ） (2025-12-11T19:59:37Z) - Unsupervised Conformal Inference: Bootstrapping and Alignment to Control LLM Uncertainty [49.19257648205146]
生成のための教師なし共形推論フレームワークを提案する。
我々のゲートは、分断されたUPPよりも厳密で安定した閾値を提供する。
その結果は、ラベルのない、API互換の、テスト時間フィルタリングのゲートになる。
論文 参考訳（メタデータ） (2025-09-26T23:40:47Z) - Latent Veracity Inference for Identifying Errors in Stepwise Reasoning [78.29317733206643]
本稿では、精度割当てに対する離散探索アルゴリズムであるVeracity Search(VS)を紹介する。
その他の方法では、後続の精度値よりも後続の分布において難解な推論を行う。
VSを一般化し、新しいコンテキストで正確なゼロショットの精度推論を可能にする。
論文 参考訳（メタデータ） (2025-05-17T04:16:36Z) - Fast Controlled Generation from Language Models with Adaptive Weighted Rejection Sampling [90.86991492288487]
トークンの制約を評価するのは 違法にコストがかかる
LCDは文字列上のグローバル分布を歪め、ローカル情報のみに基づいてトークンをサンプリングすることができる。
我々のアプローチは最先端のベースラインよりも優れていることを示す。
論文 参考訳（メタデータ） (2025-04-07T18:30:18Z) - SEAL: Steerable Reasoning Calibration of Large Language Models for Free [58.931194824519935]
大規模言語モデル(LLM)は、拡張チェーン・オブ・ソート(CoT)推論機構を通じて複雑な推論タスクに魅力的な機能を示した。
最近の研究では、CoT推論トレースにかなりの冗長性が示されており、これはモデル性能に悪影響を及ぼす。
我々は,CoTプロセスをシームレスに校正し,高い効率性を示しながら精度を向上する,トレーニング不要なアプローチであるSEALを紹介した。
論文 参考訳（メタデータ） (2025-04-07T02:42:07Z) - RAYEN: Imposition of Hard Convex Constraints on Neural Networks [47.494620411594624]
RAYENは、ニューラルネットワークにハード凸制約を課すフレームワークである。
最先端のアルゴリズムの20倍から7468倍の高速化を実現している。
論文 参考訳（メタデータ） (2023-07-17T09:12:05Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。