Equivalence and Similarity Refutation for Probabilistic Programs
summary
Searches for a concrete output function f and automated certificates—an upper expectation supermartingale for one program and a lower expectation submartingale for the other—whose expected values differ, giving a formal refutation of distributional equivalence and a lower bound on Kantorovich distance. The prototype reduces polynomial-for-all constraints via Handelman's theorem to existential linear constraints and solves them with Gurobi; it handles infinite-state real-valued programs, runs on 72 benchmarks, and refutes nearly all cases (distances as small as 0.005).
AI-written summary · about
chapters (12)
- 0:00Equivalence refutation intro
- 1:04Why equivalence refutation is hard
- 2:29Output equivalence definition
- 3:12Limitations of prior approaches
- 4:15Automated static analysis method
- 6:40Expectation submartingales proof rules
- 8:30Template synthesis algorithm
- 9:57Algorithm on example programs
- 10:18Measuring program similarity
- 11:01Experimental evaluation vs PSI/Mathematica
- 12:51Summary and future work
- 13:52Q&A
related talks
20mSuperDP: Differential Privacy Refutation via Supermartingales
15mA Modular Cost Analysis for Probabilistic Programs
30mRelatively Complete Verification of Probabilistic Programs
21mChecking Equivalence in a Non-strict Language
22mVerifying the Equivalence of Parameterized Quantum Circuits
20mVerified Density Compilation for a Probabilistic Programming Language
01h 02mThe Truth of a Procedure
49mSemantic Foundations for Probabilistic Programming