論文の概要: Sound Debloating of Redundant Checks in Zero-Knowledge Machine-Learning Circuits
- arxiv url: http://arxiv.org/abs/2609.10149v1
- Date: Wed, 09 Sep 2026 13:27:25 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-10 19:44:09.034946
- Title: Sound Debloating of Redundant Checks in Zero-Knowledge Machine-Learning Circuits
- Title（参考訳）: ゼロ知識機械学習回路における冗長チェックの音響デブロ
- Abstract要約: 音質を確実に保ちながら冗長チェックを除去する自動フレームワークを提案する。
我々のツールは最大48.7%の制約を排除し、セキュリティを弱めることなく証明時間を72.8%まで短縮する。
- 参考スコア（独自算出の注目度）: 8.87115326771099
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Zero-knowledge (ZK) proof systems for neural-network inference compile the model into a system of arithmetic constraints. Many of these constraints are redundant checks: range proofs, sign lookups, and bit decompositions who are globally entailed by the rest of the circuit through chains of reasoning that span distant gadgets. Removing them shrinks the circuit and accelerates proving, but the removal must be carefully justified: an unsoundly debloated circuit becomes forgeable, accepting witnesses the original would have rejected and so allowing a prover to claim, for example, that a neural network produced an output it never actually computed. Such soundness vulnerabilities are not hypothetical: under-constrained circuits in deployed ZK systems have enabled attackers to forge transactions and bypass verification entirely. We present an automated framework that removes redundant checks while provably preserving soundness. For each candidate removal, our tool first checks whether the rest of the circuit, on its own, can still rule out every value the removed check was excluding. Using whole-circuit abstract interpretation, the analysis searches for such alternative justifications and records them in a provenance graph; a check is then removed only when an alternative path through the graph still derives the facts that it is checking. This ensures that the debloated circuit opens no new forging strategy to an adversary. We evaluate circuits spanning MLP, CNN, RNN, and transformer architectures generated by two production frameworks (ezkl and zkml), with up to 25.3 million constraints. Our tool removes up to 48.7\% of constraints and reduces prover time by up to 72.8\%, without weakening security.
- Abstract（参考訳）: ニューラルネットワーク推論のためのゼロ知識証明システム(ZK)は、モデルを算術的制約のシステムにコンパイルする。
これらの制約の多くは冗長なチェックである:レンジ証明、サインルックアップ、ビット分解は、遠くのガジェットにまたがる推論の連鎖を通じて、回路の残りの部分によって世界中に関係している。
取り外しは回路を縮小し、証明を加速させるが、除去は慎重に正当化されなければならない: 正当にデブロされた回路は偽造され、元の証人が拒否したであろう証人を受け入れ、例えば、ニューラルネットワークが実際に計算されていない出力を生成したと主張する。
デプロイされたZKシステム内の制約の少ない回路は、攻撃者がトランザクションを偽造し、検証を完全にバイパスすることを可能にする。
音質を確実に保ちながら冗長チェックを除去する自動フレームワークを提案する。
それぞれの候補の除去について、我々のツールはまず、残りの回路がそれ自体で、削除されたチェックが除外されたすべての値を除外できるかどうかをチェックします。
解析は全回路抽象解釈を用いて、そのような代替正当性を探索し、証明グラフに記録する。
これにより、デ肥大回路は敵に新たな鍛造戦略を開かない。
MLP, CNN, RNN, および2つの生産フレームワーク(ezklとzkml)が生成するトランスフォーマーアーキテクチャにまたがる回路を最大2530万の制約で評価する。
我々のツールは最大48.7\%の制約を排除し、セキュリティを弱めることなく、証明時間を最大72.8\%まで短縮する。
関連論文リスト
- Formal Verification of Quantum Ancilla Safety [3.5368690233168114]
クリーンで汚いアンシラ安全のためのエンドツーエンドの検証・修復フレームワークを提案する。
まず、$m$-qubitの汚いアンシラレジスタの検証が、独立したクリーンなアンシラ安全性チェックに分解されることを証明します。
次に、各クリーンアンシラ安全インスタンスを、パウリ-$Z$およびパウリ-$X$作用素に対する代数的可換性チェックに還元する。
論文 参考訳（メタデータ） (2026-08-13T11:20:06Z) - 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) - Demystifying Variance in Circuit Discovery of LLMs [51.97489679448601]
我々は,再サンプリングのばらつきを大幅に軽減する新しい回路探索法を開発した。
テンプレートの異なるプロンプトは、モデル内の異なる回路を活性化する傾向があるため、リフレージングのばらつきが生じることを示す。
我々は、よりコンパクトで解釈可能なタスク回路を形成すると主張されている空間性は、この問題の解決に失敗すると主張している。
論文 参考訳（メタデータ） (2026-06-15T16:25:07Z) - Certified Circuits: Stability Guarantees for Mechanistic Circuits [80.30622018787835]
Certified Circuitsは、回路発見のための証明可能な安定性を保証する。
ImageNetとOODデータセットでは、認定回路は91%高い精度を達成する。
論文 参考訳（メタデータ） (2026-02-26T13:07:31Z) - 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) - Reinforcement Learning with Verifiable yet Noisy Rewards under Imperfect Verifiers [90.50039419576807]
RLVR(Reinforcement Learning with Verifiable Rewards)は、人為的なラベル付けを避けるために、自動検証に対するポリシーを訓練する。
認証ハッキングの脆弱性を軽減するため、多くのRLVRシステムはトレーニング中にバイナリ$0,1$の報酬を破棄する。
この選択にはコストがかかる:textitfalse negatives(正しい回答、FNを拒絶)とtextitfalse positives(間違った回答、FPを受け入れる)を導入する。
論文 参考訳（メタデータ） (2025-10-01T13:56:44Z) - Bisimulation Learning [55.859538562698496]
我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。
提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
論文 参考訳（メタデータ） (2024-05-24T17:11:27Z) - AC4: Algebraic Computation Checker for Circuit Constraints in ZKPs [4.810904298160317]
過度に制約された回路や過度に制約された回路はバグを引き起こす可能性がある。
提案手法の実装を表すためにAC4というツールが提案されている。
解決可能な範囲内では、チェック時間も顕著に改善されている。
論文 参考訳（メタデータ） (2024-03-23T01:44:57Z) - The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural
Networks [94.63547069706459]
#DNN-Verification問題は、DNNの入力構成の数を数えることによって安全性に反する結果となる。
違反の正確な数を返す新しい手法を提案する。
安全クリティカルなベンチマークのセットに関する実験結果を示す。
論文 参考訳（メタデータ） (2023-01-17T18:32:01Z) - Quantum Error Mitigation by Pauli Check Sandwiching [4.419800664096479]
複数対のパリティチェックを用いて誤りの有無を検知する誤差軽減手法を記述・解析する。
私たちは、拡張フラグガジェットの成果の上に構築し、しっかりとした理論的基礎の上に置きます。
論文 参考訳（メタデータ） (2022-06-01T03:48:50Z) - Neuro-Symbolic Entropy Regularization [78.16196949641079]
構造化予測では、目的は構造化されたオブジェクトをエンコードする多くの出力変数を共同で予測することである。
エントロピー正則化(Entropy regularization)という1つのアプローチは、決定境界が低確率領域にあるべきであることを示唆している。
我々は、モデルが有効対象を確実に予測することを奨励する損失、ニューロシンボリックエントロピー正規化を提案する。
論文 参考訳（メタデータ） (2022-01-25T06:23:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。