## Universal equivalence and majority on probabilistic programs over finite fields

Gilles Barthe, Charlie Jacomme, and Steve Kremer. Universal equivalence and majority on probabilistic programs over finite fields. In * Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'20)*, pp. 155–166, ACM, Saarbrücken, July 2020.

doi:10.1145/3373718.3394746

### Download

### Abstract

We study equivalence checking of probabilistic programs, a fundamental problem which arises in many application areas including cryptography, privacy, algorithmic fairness and machine learning. The programming language we consider manipulates polynomials over a finite field of characteristic $q$ and supports sampling and conditioning making it sufficiently expressive to encode boolean and arithmetic circuits. We consider two variants of the equivalence checking problem: the first one considers an interpretation over the finite field $\Fq$, while the second one, which we call universal equivalence, verifies equivalence over all extensions $\Fqk$ of $\Fq$. The universal variant typically arises in provable cryptography when one wishes to prove equivalence for any length of bitstrings, i.e., elements of $\F_2^k$ for any $k$. While the first problem is obviously decidable, we establish its exact complexity which lies in the counting hierarchy. To show decidability, and a doubly exponential upper bound, of the universal variant we rely on results from algorithmic number theory and the possibility to compare local zeta functions associated to given polynomials. Finally we study several variants of the equivalence problem, including a problem we call majority, motivated by differential privacy.

### BibTeX

@InProceedings{BJK-lics20, author = {Barthe, Gilles and Jacomme, Charlie and Kremer, Steve}, abstract = { We study equivalence checking of probabilistic programs, a fundamental problem which arises in many application areas including cryptography, privacy, algorithmic fairness and machine learning. The programming language we consider manipulates polynomials over a finite field of characteristic $q$ and supports sampling and conditioning making it sufficiently expressive to encode boolean and arithmetic circuits. We consider two variants of the equivalence checking problem: the first one considers an interpretation over the finite field $\Fq$, while the second one, which we call universal equivalence, verifies equivalence over all extensions $\Fqk$ of $\Fq$. The universal variant typically arises in provable cryptography when one wishes to prove equivalence for any length of bitstrings, i.e., elements of $\F_{2^k}$ for any $k$. While the first problem is obviously decidable, we establish its exact complexity which lies in the counting hierarchy. To show decidability, and a doubly exponential upper bound, of the universal variant we rely on results from algorithmic number theory and the possibility to compare local zeta functions associated to given polynomials. Finally we study several variants of the equivalence problem, including a problem we call majority, motivated by differential privacy. }, title = {Universal equivalence and majority on probabilistic programs over finite fields}, booktitle = {{P}roceedings of the 35th {A}nnual {ACM}/{IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'20)}, year = 2020, editor = {Holger Hermanns and Lijun Zhang and Naoki Kobayashi and Dale Miller}, month = Jul, address = {Saarbr\"ucken}, pages = {155--166}, publisher = {ACM}, acronym = {{LICS}'20}, nmonth = 7, doi = {10.1145/3373718.3394746}, }