論文の概要: Scaling Zero Knowledge UNSAT Verification via Normalized Chaining

• arxiv url: http://arxiv.org/abs/2609.19353v1
• Date: Wed, 16 Sep 2026 19:28:06 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-20 08:55:53.986777
• Title: Scaling Zero Knowledge UNSAT Verification via Normalized Chaining
• Title（参考訳）: 正規化連鎖によるゼロ知識UNSAT検証のスケーリング
• Abstract要約: ZkUnsatはゼロ知識における弱化解決証明の有効性を証明するプロトコルである。 本稿では,ZkUnsatの処理効率を向上させるための前処理手法を提案する。
• 参考スコア（独自算出の注目度）: 25.24756503681496
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Proofs of UNSAT are a standard primitive in formal verification and software assurance. In many real-world settings, the proof itself encodes proprietary or security-sensitive information, making public disclosure undesirable. Zero-knowledge certification of UNSAT addresses this tension: it enables a prover to convince a verifier that no satisfying assignment exists, without revealing anything about the underlying proof beyond its validity. Luo et al. recently introduced ZkUnsat, a protocol that achieves this goal by proving the validity of a weakened resolution proof in zero knowledge. ZkUnsat demonstrates the feasibility of zero-knowledge certification; however, its scalability to larger, real-world instances is constrained by substantial prover memory overhead, limiting its real-world applicability. Motivated by advances in UNSAT proof formats such as LRAT, which enable efficient plain-text verification, we present a preprocessing technique that improves the efficiency of ZkUnsat without introducing additional leakage. Our approach normalizes the proof so that each derived clause is justified by a resolution chain of fixed public length k. This eliminates chain-length leakage and reduces prover memory usage. With k = 16, our method certifies roughly 62% more instances than baseline ZkUnsat on the SAT 2002 competition benchmarks. Furthermore, for an equivalent number of certified instances, the memory footprint drops to under 25% of that required by the baseline.
• Abstract（参考訳）: UNSATの証明は、形式的検証とソフトウェア保証における標準的なプリミティブである。 多くの現実世界では、証明そのものがプロプライエタリまたはセキュリティに敏感な情報をエンコードしているため、公開の開示は望ましくない。 UNSATのゼロ知識証明は、この緊張に対処する: 証明者は、その妥当性を越えて、基礎となる証明について何も明らかにすることなく、証明者が満足できる課題が存在しないことを検証者に納得させることができる。 Luoらは最近ZkUnsatというプロトコルを導入し、ゼロ知識における弱化解決証明の有効性を証明した。 ZkUnsatは、ゼロ知識認証の実現可能性を示しているが、より大規模な実世界のインスタンスへのスケーラビリティは、証明可能なメモリオーバーヘッドによって制限されており、実世界の適用性が制限されている。 LRAT などの UNSAT 証明フォーマットの進歩により,効率的な平文検証が可能となり,ZkUnsat の効率を向上する前処理技術を提案する。 我々のアプローチは証明を正規化し、各派生節が固定された公長 k の分解鎖によって正当化される。 これにより、チェーン長のリークを排除し、プロファイラメモリの使用を削減できる。 k = 16 では,SAT 2002 のコンペティションベンチマークのベースラインである ZkUnsat よりも約 62% のインスタンスを認証する。 さらに、同等の認証済みインスタンス数に対して、メモリフットプリントはベースラインに必要な25%以下に低下する。

関連論文リスト

• ProofPulse: Interactive Proof Coverage Analysis for Dafny [47.23158426199152]
  帰納的検証は、実装がその仕様を満たすことを保証しますが、成功した検証は仕様の品質を保証しません。 本稿では,3値の証明カバレッジモデルを用いて,仕様品質を診断するDafny用ツールであるProgrampulseを提案する。
  論文  参考訳（メタデータ） (2026-08-31T14:00:31Z)
• Zero-Knowledge Predicate Proofs Between AI Agents: A Measured, Cross-Protocol Gateway and the Source-Integrity Gap [0.0]
  マルチエージェントAIプラットフォームは、ステージングからプロダクションへ素早く移行するが、エージェントが信頼を確立する方法はまだ初歩的だ。 提案から実行システムまで,エージェント間での検証可能なデータ最小化を行う。 32ビットのしきい値述語は6.2msで証明され、608バイトのBulletproofs証明で1.0msで検証される。
  論文  参考訳（メタデータ） (2026-08-30T23:16:17Z)
• Repurposing Backdoors for Good: Ephemeral Intrinsic Proofs for Verifiable Aggregation in Cross-silo Federated Learning [30.440611659881494]
  暗号証明からtextitIntrinsic Proofs へ移行する軽量アーキテクチャを提案する。 モデルパラメータに直接検証信号を埋め込むために、カタストロフィックフォーッティングを利用する。 我々の手法は、暗号ベースラインと比較して、ResNet-18で1000ドル以上のスピードアップを実現し、大規模モデルに効果的にスケールする。
  論文  参考訳（メタデータ） (2026-03-11T12:04:18Z)
• Verifier-Bound Communication for LLM Agents: Certified Bounds on Covert Signaling [0.0]
  言語モデルエージェントを結合することで、ポリシーに準拠したメッセージの調整を表面レベルで隠蔽することができる。 生成と受け入れを分離するプロトコルであるCLBCを提案する。 このプロトコルは、遅延リークと明示的な残留チャネルの観点から、転写リークの上限をいかに高めるかを示す。
  論文  参考訳（メタデータ） (2026-02-27T23:42:37Z)
• The Compliance Paradox: Semantic-Instruction Decoupling in Automated Academic Code Evaluation [11.984098021215878]
  SPACI(Semantic-Preserving Adrial Code Injection)フレームワークとAST-ASIP(Abstract Syntax Tree-Aware Semantic Injection Protocol)を紹介する。 これらの方法は、抽象構文木(英語版)の構文的に不活性な領域(トリヴィアノード)に逆方向の指示を埋め込むことにより、構文解析ギャップを利用する。 Python、C、C++、Javaの25,000のサブミッションにまたがる9つのSOTAモデルの大規模な評価を通じて、DeepSeek-V3のような高容量オープンウェイトモデルにおいて、破滅的な失敗率(>95%)を明らかにします。
  論文  参考訳（メタデータ） (2026-01-29T07:40:58Z)
• CLUE: Non-parametric Verification from Experience via Hidden-State Clustering [64.50919789875233]
  隠れアクティベーションの軌跡内の幾何的に分離可能なシグネチャとして解の正しさが符号化されていることを示す。 ClUE は LLM-as-a-judge ベースラインを一貫して上回り、候補者の再選において近代的な信頼に基づく手法に適合または超えている。
  論文  参考訳（メタデータ） (2025-10-02T02:14:33Z)
• Latent Veracity Inference for Identifying Errors in Stepwise Reasoning [78.29317733206643]
  本稿では、精度割当てに対する離散探索アルゴリズムであるVeracity Search(VS)を紹介する。 その他の方法では、後続の精度値よりも後続の分布において難解な推論を行う。 VSを一般化し、新しいコンテキストで正確なゼロショットの精度推論を可能にする。
  論文  参考訳（メタデータ） (2025-05-17T04:16:36Z)
• Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
  大規模言語モデル(LLM)は、現実のパーソナライズされたアプリケーションにますます統合されている。 RAGで使用される知識基盤の貴重かつしばしばプロプライエタリな性質は、敵による不正使用のリスクをもたらす。 これらの知識基盤を保護するための透かし技術として一般化できる既存の方法は、一般的に毒やバックドア攻撃を含む。 我々は、無害な」知識基盤の著作権保護の名称を提案する。
  論文  参考訳（メタデータ） (2025-02-10T09:15:56Z)
• 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)
• Input-Specific Robustness Certification for Randomized Smoothing [76.76115360719837]
  本稿では,ロバストネス認証の費用対効果を達成するために,インプット・スペクティブ・サンプリング(ISS)の高速化を提案する。 ISSは、認定半径0.05の限られたコストで3回以上、認定をスピードアップすることができる。
  論文  参考訳（メタデータ） (2021-12-21T12:16:03Z)

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

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