Verification of ML Systems via Reparameterization

TL;DR

This paper introduces a reparameterization technique to automatically verify probabilistic claims in machine learning systems using proof assistants, demonstrated through classic learning theory and fairness verification.

Contribution

It presents a novel reparameterization method enabling automatic reasoning about probabilistic programs within theorem provers for ML system verification.

Findings

Verified PAC-learnability of decision stumps

Proved fairness criterion in Bayesian hypothesis testing

Automated proofs of measurability in probabilistic programs

Abstract

As machine learning is increasingly used in essential systems, it is important to reduce or eliminate the incidence of serious bugs. A growing body of research has developed machine learning algorithms with formal guarantees about performance, robustness, or fairness. Yet, the analysis of these algorithms is often complex, and implementing such systems in practice introduces room for error. Proof assistants can be used to formally verify machine learning systems by constructing machine checked proofs of correctness that rule out such bugs. However, reasoning about probabilistic claims inside of a proof assistant remains challenging. We show how a probabilistic program can be automatically represented in a theorem prover using the concept of \emph{reparameterization}, and how some of the tedious proofs of measurability can be generated automatically from the probabilistic program. To demonstrate that this approach is broad enough to handle rather different types of machine learning systems, we verify both a classic result from statistical learning theory (PAC-learnability of decision stumps) and prove that the null model used in a Bayesian hypothesis test satisfies a fairness criterion called demographic parity.