Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge

• URL: http://arxiv.org/abs/2504.01198v1
• Date: Tue, 01 Apr 2025 21:25:34 GMT
• Title: Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
• Authors: John Kolesar, Shan Ali, Timos Antonopoulos, Ruzica Piskac,
• Abstract summary: Crepe is the first protocol for encoding regular expression equivalence proofs.<n>We also introduce the first ZK protocol to target a PSPACE-complete problem.<n> Crepe can validate large proofs in only a few seconds each.
• Score: 4.215558175939218
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• MathGAP: Out-of-Distribution Evaluation on Problems with Arbitrarily Complex Proofs [80.96119560172224]
  MathGAP generates problem statements and chain-of-thought reasoning traces according to specifications about their arithmetic proof structure.<n>Using MathGAP, we find that LLMs show a significant decrease in performance as proofs get deeper and wider.
  arXiv  Detail & Related papers  (2024-10-17T12:48:14Z)
• $O_2$ is a multiple context-free grammar: an implementation-, formalisation-friendly proof [0.0]
  Classifying languages according to the expressiveness of grammars able to generate them is a fundamental problem in computational linguistics. This paper analyses the existing proofs from the computational and the proof-theoretical point of views systematically studying whether each proof can lead to a verified (i.e., checked by a proof assistant) algorithm parsing balanced languages via MCFGs.
  arXiv  Detail & Related papers  (2024-05-15T14:51:11Z)
• Formal Verification of the Sumcheck Protocol [2.3591022864158067]
  The sumcheck protocol, introduced in 1992, is an interactive proof which is a key component of many probabilistic proof systems. We provide a formally verified security analysis of the sumcheck protocol using the interactive theorem prover Isabelle/HOL.
  arXiv  Detail & Related papers  (2024-02-08T23:01:32Z)
• Compositional Program Generation for Few-Shot Systematic Generalization [59.57656559816271]
  This study on a neuro-symbolic architecture called the Compositional Program Generator (CPG) CPG has three key features: textitmodularity, textitcomposition, and textitabstraction, in the form of grammar rules. It perfect achieves generalization on both the SCAN and COGS benchmarks using just 14 examples for SCAN and 22 examples for COGS.
  arXiv  Detail & Related papers  (2023-09-28T14:33:20Z)
• Toward Unified Controllable Text Generation via Regular Expression Instruction [56.68753672187368]
  Our paper introduces Regular Expression Instruction (REI), which utilizes an instruction-based mechanism to fully exploit regular expressions' advantages to uniformly model diverse constraints. Our method only requires fine-tuning on medium-scale language models or few-shot, in-context learning on large language models, and requires no further adjustment when applied to various constraint combinations.
  arXiv  Detail & Related papers  (2023-09-19T09:05:14Z)
• Real-time Regular Expression Matching [65.268245109828]
  This paper is devoted to finite state automata, regular expression matching, pattern recognition, and the exponential blow-up problem. This paper presents a theoretical and hardware solution to the exponential blow-up problem for some complicated classes of regular languages.
  arXiv  Detail & Related papers  (2023-08-20T09:25:40Z)
• Context Perception Parallel Decoder for Scene Text Recognition [52.620841341333524]
  Scene text recognition methods have struggled to attain high accuracy and fast inference speed. We present an empirical study of AR decoding in STR, and discover that the AR decoder not only models linguistic context, but also provides guidance on visual context perception. We construct a series of CPPD models and also plug the proposed modules into existing STR decoders. Experiments on both English and Chinese benchmarks demonstrate that the CPPD models achieve highly competitive accuracy while running approximately 8x faster than their AR-based counterparts.
  arXiv  Detail & Related papers  (2023-07-23T09:04:13Z)
• Lexinvariant Language Models [84.2829117441298]
  Token embeddings, a mapping from discrete lexical symbols to continuous vectors, are at the heart of any language model (LM) We study textitlexinvariantlanguage models that are invariant to lexical symbols and therefore do not need fixed token embeddings in practice. We show that a lexinvariant LM can attain perplexity comparable to that of a standard language model, given a sufficiently long context.
  arXiv  Detail & Related papers  (2023-05-24T19:10:46Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  We present a novel stepwise method NLProofS (Natural Language Proof Search) NLProofS learns to generate relevant steps conditioning on the hypothesis. It achieves state-of-the-art performance on EntailmentBank and RuleTaker.
  arXiv  Detail & Related papers  (2022-05-25T02:22:30Z)
• Improving Structured Text Recognition with Regular Expression Biasing [13.801707647700727]
  We study the problem of recognizing structured text that follows certain formats. We propose to improve the recognition accuracy of structured text by specifying regular expressions (regexes) for biasing.
  arXiv  Detail & Related papers  (2021-11-10T23:12:05Z)
• Proving Equivalence Between Complex Expressions Using Graph-to-Sequence Neural Models [0.0]
  We develop a graph-to-sequence neural network system for program equivalence. We extensively evaluate our system on a rich multi-type linear algebra expression language. Our machine learning system guarantees correctness for all true negatives, and ensures 0 false positive by design.
  arXiv  Detail & Related papers  (2021-06-01T20:45:42Z)
• FOREST: An Interactive Multi-tree Synthesizer for Regular Expressions [5.21480688623047]
  We present FOREST, a regular expression synthesizer for digital form validations. Forestry produces a regular expression that matches the desired pattern for the input values. We also present a new SMT encoding to synthesize capture conditions for a given regular expression.
  arXiv  Detail & Related papers  (2020-12-28T14:06:01Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.