一句话：提出首个正则表达式等价性的零知识证明协议 Crêpe，基于导数与余归纳，可在数秒内验证大规模证明。
零知识协议允许开发者在不泄露程序本身的情况下证明程序正确性。正则表达式在软件中广泛使用，已有协议可证明某字符串属于某正则表达式语言，但尚无协议处理更复杂的 PSPACE 完全问题：证明两个正则表达式等价。本文提出 Crêpe，首个编码正则表达式等价性证明的零知识协议，也是首个面向 PSPACE 完全问题的零知识协议。Crêpe 采用基于正则表达式导数和余归纳定制的证明规则演算，并提出一种可靠且完备的算法来生成该格式的证明。作者在包含数百个正则表达式等价性证明的测试集上评估 Crêpe，每个大型证明仅需数秒即可验证。
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 Crêpe , the first ZK protocol for encoding regular expression equivalence proofs and also the first ZK protocol to target a PSPACE-complete problem. Crêpe 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 Crêpe on a suite of hundreds of regular expression equivalence proofs. Crêpe can validate large proofs in only a few seconds each.
@article{paperbot3001,
title = {Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge},
author = {John C. Kolesar and Shan Ali and Timos Antonopoulos and Ruzica Piskac},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763063}
}