Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Equivalence and Similarity Refutation for Probabilistic Programs

Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný, Đorđe Žikelić

TL;DR

This work tackles static verification of equivalence and similarity between the output distributions of probabilistic programs. It introduces a novel martingale-based framework that jointly synthesizes a function $f$ and two state functions (a UESM for the first program and a LESM for the second) to certify non-equivalence via $\mathbb{E}_{\mu_1}[f] \neq \mathbb{E}_{\mu_2}[f]$. The approach yields formal guarantees, is automated, and extends to infinite-state programs; for similarity, it can provide lower bounds on the Kantorovich distance by requiring $f$ to be $1$-Lipschitz. An automated constraint-solver pipeline synthesizes $f$, $U_f$, and $L_f$ as polynomial templates and translates the resulting conditions into a linear program, enabling scalable analysis on polynomial probabilistic programs. The results demonstrate effective refutation and distance lower-bounding across a diverse set of benchmarks, highlighting the method’s practical impact for debugging and compiler verification in probabilistic programming.

Abstract

We consider the problems of statically refuting equivalence and similarity of output distributions defined by a pair of probabilistic programs. Equivalence and similarity are two fundamental relational properties of probabilistic programs that are essential for their correctness both in implementation and in compilation. In this work, we present a new method for static equivalence and similarity refutation. Our method refutes equivalence and similarity by computing a function over program outputs whose expected value with respect to the output distributions of two programs is different. The function is computed simultaneously with an upper expectation supermartingale and a lower expectation submartingale for the two programs, which we show to together provide a formal certificate for refuting equivalence and similarity. To the best of our knowledge, our method is the first approach to relational program analysis to offer the combination of the following desirable features: (1) it is fully automated, (2) it is applicable to infinite-state probabilistic programs, and (3) it provides formal guarantees on the correctness of its results. We implement a prototype of our method and our experiments demonstrate the effectiveness of our method to refute equivalence and similarity for a number of examples collected from the literature.

Equivalence and Similarity Refutation for Probabilistic Programs

TL;DR

This work tackles static verification of equivalence and similarity between the output distributions of probabilistic programs. It introduces a novel martingale-based framework that jointly synthesizes a function and two state functions (a UESM for the first program and a LESM for the second) to certify non-equivalence via . The approach yields formal guarantees, is automated, and extends to infinite-state programs; for similarity, it can provide lower bounds on the Kantorovich distance by requiring to be -Lipschitz. An automated constraint-solver pipeline synthesizes , , and as polynomial templates and translates the resulting conditions into a linear program, enabling scalable analysis on polynomial probabilistic programs. The results demonstrate effective refutation and distance lower-bounding across a diverse set of benchmarks, highlighting the method’s practical impact for debugging and compiler verification in probabilistic programming.

Abstract

We consider the problems of statically refuting equivalence and similarity of output distributions defined by a pair of probabilistic programs. Equivalence and similarity are two fundamental relational properties of probabilistic programs that are essential for their correctness both in implementation and in compilation. In this work, we present a new method for static equivalence and similarity refutation. Our method refutes equivalence and similarity by computing a function over program outputs whose expected value with respect to the output distributions of two programs is different. The function is computed simultaneously with an upper expectation supermartingale and a lower expectation submartingale for the two programs, which we show to together provide a formal certificate for refuting equivalence and similarity. To the best of our knowledge, our method is the first approach to relational program analysis to offer the combination of the following desirable features: (1) it is fully automated, (2) it is applicable to infinite-state probabilistic programs, and (3) it provides formal guarantees on the correctness of its results. We implement a prototype of our method and our experiments demonstrate the effectiveness of our method to refute equivalence and similarity for a number of examples collected from the literature.
Paper Structure (39 sections, 9 theorems, 25 equations, 3 figures, 2 tables)

This paper contains 39 sections, 9 theorems, 25 equations, 3 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Overview
  3. Extension to similarity refutation.
  4. Limitations.
  5. Preliminaries
  6. Program Syntax
  7. Program Semantics
  8. Termination.
  9. Output distribution.
  10. Kantorovich distance of probability distributions
  11. Kantorovich distance: definition.
  12. Problem Statement
  13. Equivalence Refutation Problem
  14. Similarity Refutation Problem
  15. Finite first moment assumption.
  16. ...and 24 more sections

Key Result

theorem 1

Let $\mathcal{C}=(\mathit{L},V,V_{\mathit{out}},\ell_{\mathit{init}},\mathbf{x}_{\mathit{init}},\mapsto,G,\mathit{Up})$ be an a.s. terminating pCFG with output distribution $\mu^\mathcal{C}$ and $f \colon \mathbb{R}^{|V_\mathit{out}|} \rightarrow \mathbb{R}$ a Borel measurable function over the outp

Figures (3)

  • Figure 1: Transmission protocol example.
  • Figure 2: Compilation bug example.
  • Figure 3: The Fork and Join queuing network example.

Theorems & Definitions (16)

  • Remark 1: Martingale-based approach to relational analysis
  • definition 1: Kantorovich distance of output distributions
  • definition 2: Upper expectation supermartingale (UESM)
  • definition 3: Lower expectation submartingale (LESM)
  • definition 4: OST-soundness
  • theorem 1: Soundness of U/LESMs
  • theorem 2: Soundness of equivalence and similarity refutation
  • theorem 3: Correctness of Equivalence Refutation
  • definition 5
  • definition 6: Stopping time
  • ...and 6 more