論文の概要: Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge

• arxiv url: http://arxiv.org/abs/2504.01198v1
• Date: Tue, 01 Apr 2025 21:25:34 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-04-03 13:17:43.435824
• Title: Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
• Title（参考訳）: ゼロ知識における正規表現等価性の共帰的証明
• Authors: John Kolesar, Shan Ali, Timos Antonopoulos, Ruzica Piskac,
• Abstract要約: Crepeは正規表現同値証明を符号化する最初のプロトコルである。 PSPACE完全問題をターゲットにした最初のZKプロトコルも導入する。 クレープは、それぞれ数秒で大きな証明を検証できる。
• 参考スコア（独自算出の注目度）: 4.215558175939218
• License:
• Abstract: Zero-knowledge (ZK) protocols enable software developers to provide proofs of their programs' correctness to other parties without revealing the programs themselves. Regular expressions are pervasive in real-world software, and zero-knowledge protocols have been developed in the past for the problem of checking whether an individual string appears in the language of a regular expression, but no existing protocol addresses the more complex PSPACE-complete problem of proving that two regular expressions are equivalent. We introduce Crepe, the first ZK protocol for encoding regular expression equivalence proofs and also the first ZK protocol to target a PSPACE-complete problem. Crepe uses a custom calculus of proof rules based on regular expression derivatives and coinduction, and we introduce a sound and complete algorithm for generating proofs in our format. We test Crepe on a suite of hundreds of regular expression equivalence proofs. Crepe can validate large proofs in only a few seconds each.
• Abstract（参考訳）: Zero-knowledge (ZK) プロトコルにより、ソフトウェア開発者はプログラム自体を公開することなく、プログラムの正しさの証明を他の当事者に提供することができる。 正規表現は実世界のソフトウェアで広く普及しており、正規表現の言語に個々の文字列が現れるかどうかを確認するためにゼロ知識プロトコルが過去に開発されてきたが、既存のプロトコルでは2つの正規表現が等価であることを示すより複雑なPSPACE完全問題に対処していない。 本稿では、正規表現同値証明を符号化する最初のZKプロトコルであるCrepeと、PSPACE完全問題をターゲットにしたZKプロトコルを紹介する。 クレープは正規表現微分と造語に基づく証明規則のカスタム計算を用いており、我々の形式で証明を生成するための健全で完全なアルゴリズムを導入している。 我々は、何百もの正規表現同値証明のスイートでCrepeをテストする。 クレープは、それぞれ数秒で大きな証明を検証できる。

関連論文リスト

• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
  本稿では,オープンソースの大規模言語モデル(LLM)であるGoedel-Proverを紹介する。
  論文  参考訳（メタデータ） (2025-02-11T15:27:35Z)
• $O_2$ is a multiple context-free grammar: an implementation-, formalisation-friendly proof [0.0]
  それらを生成することができる文法の表現力に応じて言語を分類することは、計算言語学における根本的な問題である。 本稿では,各証明が検証された(すなわち,証明支援者によってチェックされる)アルゴリズムに繋がるかどうかを,MCFGを通して解析できるかどうかを体系的に研究する,計算的および証明理論的な視点から,既存の証明を解析する。
  論文  参考訳（メタデータ） (2024-05-15T14:51:11Z)
• Formal Verification of the Sumcheck Protocol [2.3591022864158067]
  1992年に導入されたsumcheckプロトコルは、多くの確率的証明システムの重要な構成要素である対話的証明である。 本稿では,対話型定理証明器Isabelle/HOLを用いた要約プロトコルのセキュリティ解析について述べる。
  論文  参考訳（メタデータ） (2024-02-08T23:01:32Z)
• Compositional Program Generation for Few-Shot Systematic Generalization [59.57656559816271]
  コンポジションプログラムジェネレータ(CPG)と呼ばれるニューロシンボリックアーキテクチャに関する研究 CPGには3つの重要な特徴がある: 文法規則の形で、テキストモジュラリティ、テキストコンポジション、テキストタストラクションである。 SCAN と COGS のベンチマークでは,SCAN の14例と COGS の22例を使用して,完全な一般化を実現している。
  論文  参考訳（メタデータ） (2023-09-28T14:33:20Z)
• Toward Unified Controllable Text Generation via Regular Expression Instruction [56.68753672187368]
  本稿では,正規表現の利点をフル活用し,多様な制約を一様にモデル化する命令ベース機構を用いた正規表現指導(REI)を提案する。 提案手法では,中規模言語モデルの微調整や,大規模言語モデルでの少数ショット・インコンテクスト学習のみを要し,各種制約の組み合わせに適用した場合のさらなる調整は不要である。
  論文  参考訳（メタデータ） (2023-09-19T09:05:14Z)
• Real-time Regular Expression Matching [65.268245109828]
  本稿では,有限状態オートマトン,正規表現マッチング,パターン認識,指数的爆破問題について述べる。 本稿では,正規言語の複雑なクラスに対する指数的爆破問題に対する理論的およびハードウェア的解法を提案する。
  論文  参考訳（メタデータ） (2023-08-20T09:25:40Z)
• Context Perception Parallel Decoder for Scene Text Recognition [52.620841341333524]
  シーンテキスト認識手法は高い精度と高速な推論速度を達成するのに苦労している。 本稿では、STRにおけるARデコーディングの実証的研究を行い、ARデコーダが言語文脈をモデル化するだけでなく、視覚的文脈知覚のガイダンスも提供することを明らかにする。 我々は一連のCPPDモデルを構築し、提案したモジュールを既存のSTRデコーダにプラグインする。英語と中国語のベンチマーク実験により、CPPDモデルはARベースモデルよりも約8倍高速に動作し、高い競争精度を達成できることを示した。
  論文  参考訳（メタデータ） (2023-07-23T09:04:13Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)
• Improving Structured Text Recognition with Regular Expression Biasing [13.801707647700727]
  本研究では,ある形式に従う構造化テキストの認識の問題について検討する。 偏見の正規表現 (regexes) を指定することにより, 構造化テキストの認識精度を向上させることを提案する。
  論文  参考訳（メタデータ） (2021-11-10T23:12:05Z)
• Proving Equivalence Between Complex Expressions Using Graph-to-Sequence Neural Models [0.0]
  プログラム同値性のためのグラフ・ツー・シーケンスニューラルネットワークシステムを開発した。 我々は、リッチな多型線形代数表現言語を用いて、我々のシステムを広範囲に評価する。 我々の機械学習システムは、全ての真正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の
  論文  参考訳（メタデータ） (2021-06-01T20:45:42Z)
• FOREST: An Interactive Multi-tree Synthesizer for Regular Expressions [5.21480688623047]
  デジタルフォームバリデーションのための正規表現シンセサイザーであるFORESTについて紹介する。 forestryは入力値の所望のパターンにマッチする正規表現を生成する。 また、与えられた正規表現のキャプチャ条件を合成する新しいSMTエンコーディングも提案する。
  論文  参考訳（メタデータ） (2020-12-28T14:06:01Z)

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

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