論文の概要: zkStruDul: Programming zkSNARKs with Structural Duality

• arxiv url: http://arxiv.org/abs/2511.10565v1
• Date: Fri, 14 Nov 2025 01:58:08 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-11-14 22:53:22.932339
• Title: zkStruDul: Programming zkSNARKs with Structural Duality
• Title（参考訳）: zkStruDul: 構造的双対でzkSNARKをプログラミングする
• Authors: Rahul Krishnan, Ashley Samuelson, Emily Yao, Ethan Cecchetti,
• Abstract要約: zkStruDulは、入力変換を統一し、定義を単一の複合抽象化に述語する言語である。 我々は、ソースレベルのセマンティクスを提供し、その振る舞いが予測されたセマンティクスと同一であることを証明する。
• 参考スコア（独自算出の注目度）: 0.2449909275410287
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Non-Interactive Zero Knowledge (NIZK) proofs, such as zkSNARKS, let one prove knowledge of private data without revealing it or interacting with a verifier. While existing tooling focuses on specifying the predicate to be proven, real-world applications optimize predicate definitions to minimize proof generation overhead, but must correspondingly transform predicate inputs. Implementing these two steps separately duplicates logic that must precisely match to avoid catastrophic security flaws. We address this shortcoming with zkStruDul, a language that unifies input transformations and predicate definitions into a single combined abstraction from which a compiler can project both procedures, eliminating duplicate code and problematic mismatches. zkStruDul provides a high-level abstraction to layer on top of existing NIZK technology and supports important features like recursive proofs. We provide a source-level semantics and prove its behavior is identical to the projected semantics, allowing straightforward standard reasoning.
• Abstract（参考訳）: 非対話ゼロ知識(NIZK)証明(zkSNARKS)は、プライベートデータの知識を公開せずに証明し、検証者と対話させる。 既存のツールは証明すべき述語を指定することに重点を置いているが、実世界のアプリケーションは証明生成オーバーヘッドを最小限に抑えるために述語定義を最適化するが、それに対応する述語入力を変換する必要がある。 これら2つのステップを別々に実装することは、破滅的なセキュリティ欠陥を避けるために、正確に一致しなければならないロジックを複製する。 zkStruDulは、入力変換を統一し、定義を述語する言語で、コンパイラが両方のプロシージャを投影し、重複するコードと問題のあるミスマッチを排除できる単一の統合抽象化にします。 zkStruDulは既存のNIZK技術の上に高レベルの抽象化を提供し、再帰的証明のような重要な機能をサポートしている。 我々は、ソースレベルのセマンティクスを提供し、その振る舞いが予測されたセマンティクスと同一であることを証明する。

関連論文リスト

• Misquoted No More: Securely Extracting F* Programs with IO [0.3848364262836075]
  効果を表すモナドを使用する浅層埋め込みは、証明指向言語で人気がある。 浅い組込みプログラムが検証されると、しばしばOCamlやCのような主流言語に抽出される。 私たちはこのアイデアに基づいていますが、翻訳バリデーションの使用を最初の抽出ステップに制限します。
  論文  参考訳（メタデータ） (2026-02-23T15:37:18Z)
• Lookahead-then-Verify: Reliable Constrained Decoding for Diffusion LLMs under Context-Free Grammars [17.13122301190815]
  本稿では,dLLMに特化して設計された制約付き復号法であるLAVEを提案する。 提案手法は,dLLMの鍵となる特性,すなわち前方通過時の全位置のトークン分布を予測する能力を利用する。 広く使用されている4つのdLLMと3つの代表的なベンチマークによる大規模な実験は、LAVEが既存のベースラインを一貫して上回り、構文的正確性を大幅に改善し、無視可能なランタイムオーバーヘッドを発生させることを示した。
  論文  参考訳（メタデータ） (2026-01-31T08:58:15Z)
• Multi-Agent Procedural Graph Extraction with Structural and Logical Refinement [66.51979814832332]
  モデル式は、専用の構造的および論理的洗練を伴う多ラウンド推論プロセスとして手続きグラフ抽出を定式化する。 実験により、モデルが強いベースラインに対して構造的正当性と論理的整合性の両方において大幅に改善されることが示されている。
  論文  参考訳（メタデータ） (2026-01-27T04:00:48Z)
• VIRO: Robust and Efficient Neuro-Symbolic Reasoning with Verification for Referring Expression Comprehension [51.76841625486355]
  Referring Expression (REC) は、自然言語クエリに対応する画像領域をローカライズすることを目的としている。 最近のニューロシンボリックRECアプローチは、大規模言語モデル(LLM)と視覚言語モデル(VLM)を利用して構成推論を行う。 推論ステップ内に軽量な演算子レベルの検証器を組み込む,ニューロシンボリックなフレームワークであるVIROを紹介する。
  論文  参考訳（メタデータ） (2026-01-19T07:21:19Z)
• NormCode: A Semi-Formal Language for Context-Isolated AI Planning [7.3226942109207895]
  推論計画を構築するための半形式言語であるNormCodeを提示する。 各ステップはデータ分離で動作し、明示的に渡された入力のみを受け取り、設計によるクロスステップ汚染を排除します。 我々は,(1)任意の長さの入力に対して100%の精度を達成するベースX加算アルゴリズム,(2)NormCode自身の5フェーズコンパイラパイプラインの自己ホスト実行の2つのデモを通じて,NormCodeを検証する。
  論文  参考訳（メタデータ） (2025-12-11T11:50:50Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。 提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
  論文  参考訳（メタデータ） (2025-11-26T06:39:19Z)
• QiMeng-CRUX: Narrowing the Gap between Natural Language and Verilog via Core Refined Understanding eXpression [48.84841760215598]
  大規模言語モデル(LLM)はハードウェア記述言語(HDL)生成において有望な能力を示している。 既存のアプローチは、しばしば曖昧で冗長で構造化されていない自由形式の自然言語記述に依存している。 我々は、ハードウェアコード生成を、オープンな自然言語空間からドメイン固有の高度に制約されたターゲット空間への複雑な変換として扱う。 構造化された中間空間であるCore Refined Understanding eXpression (CRUX)を導入し、ユーザの意図の本質的な意味を捉えながら、正確なVerilogコード生成のための式を整理する。
  論文  参考訳（メタデータ） (2025-11-25T09:17:32Z)
• Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
  現代言語モデル(LM)は、強い推論能力を示すが、標準的な評価は、人間のような推論の重要な側面である効率性を見越しながら、正確性を強調する。 本稿では、論理プログラミングのレンズを用いて、LM推論効率を評価するためのフレームワークを提案する。
  論文  参考訳（メタデータ） (2025-10-29T15:30:31Z)
• ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization [10.021930888250546]
  現在のアプローチでは、オリジナルの人間による議論の意味的意味と論理的構造を保存できない。 本稿では,構造的忠実度を主目的とする新しいパイプラインであるProofFlowを紹介する。 我々は184人の学部レベルの問題に対して,ステップバイステップのソリューションを手動でアノテートした新しいベンチマークを提示する。 また,構文的正しさ,意味的忠実度,構造的忠実度を評価するための新しい合成指標ProofScoreを導入する。
  論文  参考訳（メタデータ） (2025-10-13T10:20:11Z)
• Truth-Aware Decoding: A Program-Logic Approach to Factual Language Generation [0.2864713389096699]
  本稿では,ニューラルネットワーク生成を知識ベースに整合させる検証指向の復号法であるTrath-Aware Decoding (TAD)を紹介する。 i) オラクルフィルタリングをプログラム論理的判断として表現する制約に基づくセマンティクス、(ii) 欲求選択が音と完全ガードの下で局所的可能性優位性を楽しむことの証明、(iii) 知識を意識した安全な質量を通じて事実的リスクを定量化するエントロピー型不変量である。
  論文  参考訳（メタデータ） (2025-10-03T22:11:15Z)
• SLICET5: Static Program Slicing using Language Models with Copy Mechanism and Constrained Decoding [13.61350801915956]
  静的プログラムスライシングはソフトウェア工学の基本的な技術である。 ourtoolは静的プログラムスライシングをシーケンス・ツー・シーケンスタスクとして再構成する新しいスライシングフレームワークである。 ourtoolは、最先端のベースラインを一貫して上回る。
  論文  参考訳（メタデータ） (2025-09-22T03:14:47Z)
• ReF Decompile: Relabeling and Function Call Enhanced Decompile [50.86228893636785]
  逆コンパイルの目標は、コンパイルされた低レベルコード(アセンブリコードなど)を高レベルプログラミング言語に変換することである。 このタスクは、脆弱性識別、マルウェア分析、レガシーソフトウェアマイグレーションなど、さまざまなリバースエンジニアリングアプリケーションをサポートする。
  論文  参考訳（メタデータ） (2025-02-17T12:38:57Z)
• Enhancing LLM Character-Level Manipulation via Divide and Conquer [74.55804812450164]
  大規模言語モデル(LLM)は、幅広い自然言語処理(NLP)タスクにまたがる強力な一般化機能を示している。 彼らは文字レベルの文字列操作において顕著な弱点を示し、文字削除、挿入、置換といった基本的な操作に苦労した。 本稿では,トークンレベルの処理と文字レベルの操作のギャップを埋める新しい手法であるDivide and Conquerによる文字レベル操作を提案する。
  論文  参考訳（メタデータ） (2025-02-12T07:37:39Z)
• Localizing Factual Inconsistencies in Attributable Text Generation [74.11403803488643]
  本稿では,帰属可能なテキスト生成における事実の不整合をローカライズするための新しい形式であるQASemConsistencyを紹介する。 QASemConsistencyは、人間の判断とよく相関する事実整合性スコアを得られることを示す。
  論文  参考訳（メタデータ） (2024-10-09T22:53:48Z)
• SCALE: Constructing Structured Natural Language Comment Trees for Software Vulnerability Detection [36.37244302912536]
  本稿では,事前学習モデルに基づく構造化自然言語コメント木に基づくvulnerAbiLity dEtectionフレームワークを提案する。 提案したStructured Natural Language Comment Tree (SCT)は、コードステートメントのセマンティクスとコード実行シーケンスを統合する。
  論文  参考訳（メタデータ） (2024-03-28T02:20:03Z)
• Log Probabilities Are a Reliable Estimate of Semantic Plausibility in Base and Instruction-Tuned Language Models [50.15455336684986]
  意味的妥当性を評価するため,LogProbsの有効性と基本的なプロンプトを評価した。 LogProbsは、直接ゼロショットプロンプトよりも、より信頼性の高いセマンティックな妥当性を提供する。 我々は,プロンプトベースの評価の時代においても,LogProbsは意味的妥当性の有用な指標である,と結論付けた。
  論文  参考訳（メタデータ） (2024-03-21T22:08:44Z)
• SAGA: Summarization-Guided Assert Statement Generation [34.51502565985728]
  本稿では,アサート文の自動生成のための新しい要約誘導手法を提案する。 我々は、事前訓練された言語モデルを参照アーキテクチャとして利用し、アサート文生成のタスクでそれを微調整する。
  論文  参考訳（メタデータ） (2023-05-24T07:03:21Z)

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

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