論文の概要: StateSync-GKR: Machine-Checking the Trust Chain from Sparse-Merkle State Transitions to GKR Verification
- arxiv url: http://arxiv.org/abs/2610.05335v1
- Date: Sun, 04 Oct 2026 15:56:51 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-10 21:30:15.061216
- Title: StateSync-GKR: Machine-Checking the Trust Chain from Sparse-Merkle State Transitions to GKR Verification
- Title（参考訳）: StateSync-GKR: Sparse-Merkle状態遷移からGKR検証への信頼連鎖の機械化
- Abstract要約: GKRの音質は、演算回路に関する偽の出力要求を束縛するが、アプリケーションは、その回路が意図した状態遷移を符号化することを保証する必要がある。
Isabelle/HOLのスパースマークル会員、非メンバーシップ、更新について、この接続をマシンでチェックします。
再利用可能なプロトコルモデルは、レイヤリダクション、配線述語拡張、インポートされた要約音を明示的な連鎖イベントのバウンダリに集約する。
- 参考スコア（独自算出の注目度）: 9.32030540168344
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: GKR soundness bounds false output claims about arithmetic circuits, but an application also needs assurance that its circuit encodes the intended state transition. We machine-check this connection for sparse-Merkle membership, non-membership, and update in Isabelle/HOL. A compiler model relates circuit acceptance to transition validity in both directions. A reusable protocol model assembles layer reduction, wiring-predicate extensions, and imported sumcheck soundness into a bound on an explicit chain event. Their composition transfers semantic invalidity to that bound, with the witness fixed before the challenge experiment. Concrete interpretations and premise activations expose vacuous assumption sets that a clean build alone would miss. A further development constructs the exact degree-four KoalaBear extension, lifts the base-field circuit objects, and establishes the assembly bound with denominator $p^4$ under its stated challenge assumptions. An executable Rust prover accompanies the model. Creusot/Why3 contracts provide a partial implementation connection, and a conditional theorem relates successful verifier traces to the model event under an undischarged value-correspondence premise. Neither the transcript's online challenge distribution nor a multi-round Fiat--Shamir reduction is established. The contribution is the composition, within one proof assistant, of compiler correctness with a GKR assembly model, together with an explicit account of the remaining implementation and cryptographic obligations.
- Abstract（参考訳）: GKRの音質は、演算回路に関する偽の出力要求を束縛するが、アプリケーションは、その回路が意図した状態遷移を符号化することを保証する必要がある。
Isabelle/HOLのスパースマークル会員、非メンバーシップ、更新について、この接続をマシンでチェックします。
コンパイラモデルは、回路受入と両方向の遷移妥当性を関連付ける。
再利用可能なプロトコルモデルは、レイヤリダクション、配線述語拡張、インポートされた要約音を明示的な連鎖イベントのバウンダリに集約する。
彼らの構成は、挑戦実験の前に証人が固定されたまま、意味的無効性をその境界に転送する。
具体的な解釈と前提のアクティベーションは、クリーンなビルドだけで見逃すであろう空虚な仮定を露呈する。
更なる開発は、正確な次数4のKoalaBear拡張を構築し、ベースフィールドの回路オブジェクトを持ち上げ、宣言されたチャレンジ仮定の下で分母$p^4$で束縛されたアセンブリを確立する。
実行可能なRust証明器がモデルに同伴する。
Creusot/Why3 契約は部分的な実装接続を提供し、条件付き定理は、未充足値対応の前提の下で、モデル事象に追従した検証結果を関連付ける。
書き起こしのオンライン・チャレンジ・ディストリビューションもマルチラウンド・フィアット・リダクションも確立していない。
コントリビューションは、GKRアセンブリモデルによるコンパイラの正しさの1つの証明アシスタント内で、残りの実装と暗号的義務の明示的な説明とともに構成されている。
関連論文リスト
- Answer with Evidence: Consistency-Aware Grounded Visual Question Answering for Roadside Traffic Scenes [67.12965225696523]
RoadSceneVQA-Gは34.7Kの質問応答対のベンチマークである。
RoadSceneVQA-Gは34.7Kの質問応答対のベンチマークである。
論文 参考訳（メタデータ） (2026-10-04T14:48:54Z) - ReTrace: Rejected-Trajectory Conditioning for Speculative Decoding [46.17292752074153]
本稿では,前回のラウンドから削除された接尾辞に対して,各ドラフトブロックを条件付けするReTraceを紹介する。
ReTraceは、DFlashバックボーン上で、平均受信長とエンドツーエンドの復号速度を継続的に改善する。
論文 参考訳（メタデータ） (2026-08-30T12:20:54Z) - Benchmarking Cyberattack Detection in Electric Vehicle Charging Infrastructure with Benign User Updates [3.9286216777643737]
電気自動車の充電インフラにおけるサイバー攻撃検出は、要求されたエネルギーと出発時間に対する正常な動作後の修正によって複雑である。
本稿では, 実適応充電ネットワーク(ACN)セッションの入力順序を保存するための, リーク制御されたセッションレベルベンチマークを開発する。
固定プールは、生成された各攻撃をソースセッションの分割に保持し、物理的に動機付けられた6つの攻撃とその調整されたバリエーションを含む。
論文 参考訳（メタデータ） (2026-08-11T14:50:24Z) - LEDGERMIND: Provenance-Constrained Multimodal Agentic Reasoning with a Structured Evidence Ledger [11.70343232168598]
LedgerMindはプロビデンスに制約のあるエージェント推論エンジンである。
最終回答の精度が曖昧になる傾向にある4つの繰り返し発生する障害パターンをターゲットにしています。
答えの正確さと軌道レベルの忠実さの両方を改善する。
論文 参考訳（メタデータ） (2026-07-30T15:35:34Z) - Agree on the Model, Verify the Inference: GKR Protocols for HND-Based Transformer Inference [16.820164197707044]
Outsourced Transformer推論は、クライアントに置換と実行をモデル化する。
本稿では、同型非同型分解変換器のバックボーンを検証するための登録モデルプロトコルであるGKR-HNDを提案する。
論文 参考訳（メタデータ） (2026-07-23T10:52:53Z) - Towards Verifiable Transformers: Solver-Checkable Circuit Explanations [0.23689955632456092]
本稿では,タスクローカライズされたトランスフォーマー回路を有界,ソルバチェック可能なクレームに変換するためのフレームワークであるVerifiable Transformersを紹介する。
署名付きL1 BandNorm、スパースマックスアテンション、LeakyReLUを用いて、GPTスタイルのアーキテクチャで直接検証を行う。
また,タスクローカライズされた回路上でのサロゲートによる検証も行った。
論文 参考訳（メタデータ） (2026-05-21T05:21:40Z) - LC-ERD: Mining Latent Logic for Self-Evolving Reasoning via Consistency-Regulated Reward Decomposition [55.572260012037084]
本稿では, LC-ERD (Logic-Consistent Endogenous Reward Decomposition) を紹介する。
モデルの潜在論理エキスパートズ(Latent Logic Expertise)からのコンセンサスを集約することで、変分論理ポテンシャルを導出する。
LC-ERDは、論理の一貫性と正確性の間のトレードオフを明らかにする、堅牢な自己進化パスを提供する。
論文 参考訳（メタデータ） (2026-05-19T07:27:50Z) - 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) - Hybrid Reinforcement: When Reward Is Sparse, It's Better to Be Dense [36.71358559780692]
HEROは、検証者信号と報酬モデルスコアを構造化された方法で統合する強化学習フレームワークである。
HEROはRMのみのベースラインと検証者のみのベースラインを一貫して上回り、検証可能なタスクと検証しにくいタスクの両方で大きな利益を上げている。
論文 参考訳（メタデータ） (2025-10-08T17:09:41Z) - SIM-CoT: Supervised Implicit Chain-of-Thought [108.30049193668083]
Implicit Chain-of-Thought(CoT)メソッドは、大規模言語モデルにおける明示的なCoT推論に代わるトークン効率の代替手段を提供する。
暗黙的なCoTの計算予算をスケールする際の中核的な不安定性問題を特定する。
そこで我々はSIM-CoTを提案する。SIM-CoTは,遅延推論空間を安定化・拡張するためのステップレベルの監視を実現するモジュールである。
論文 参考訳（メタデータ） (2025-09-24T17:01:32Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。