論文の概要: 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技術の上に高レベルの抽象化を提供し、再帰的証明のような重要な機能をサポートしている。
我々は、ソースレベルのセマンティクスを提供し、その振る舞いが予測されたセマンティクスと同一であることを証明する。
関連論文リスト
- 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。