@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@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},
}