Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System

TL;DR

The paper tackles automated verification of higher-order probabilistic programs by developing a dependent refinement type system for a generalised higher-order fixed point logic (HFL) and encoding program properties via CPS into HFL terms. Soundness is established through a categorical semantics framework, and verification reduces to solving constrained Horn clauses extended with admissible and integrable predicate variables to handle least fixed points and continuous distributions. The authors implement a type checker (extending RCaml) and demonstrate it on benchmarks, solving 11 of 14 problems across four verification tasks, including both discrete and continuous distributions and conditioning. This approach preserves reusability with non-probabilistic verification tooling by only modifying the CHC solver and adding a couple of predicate-variable templates, enabling broad applicability to higher-order probabilistic verification tasks with practical automation potential.

Abstract

Verification of higher-order probabilistic programs is a challenging problem. We present a verification method that supports several quantitative properties of higher-order probabilistic programs. Usually, extending verification methods to handle the quantitative aspects of probabilistic programs often entails extensive modifications to existing tools, reducing compatibility with advanced techniques developed for qualitative verification. In contrast, our approach necessitates only small amounts of modification, facilitating the reuse of existing techniques and implementations. On the theoretical side, we propose a dependent refinement type system for a generalised higher-order fixed point logic (HFL). Combined with continuation-passing style encodings of properties into HFL, our dependent refinement type system enables reasoning about several quantitative properties, including weakest pre-expectations, expected costs, moments of cost, and conditional weakest pre-expectations for higher-order probabilistic programs with continuous distributions and conditioning. The soundness of our approach is proved in a general setting using a framework of categorical semantics so that we don't have to repeat similar proofs for each individual problem. On the empirical side, we implement a type checker for our dependent refinement type system that reduces the problem of type checking to constraint solving. We introduce admissible predicate variables and integrable predicate variables to constrained Horn clauses (CHC) so that we can soundly reason about the least fixed points and samplings from probability distributions. Our implementation demonstrates that existing CHC solvers developed for non-probabilistic programs can be extended to a solver for the extended CHC with only small efforts. We also demonstrate the ability of our type checker to verify various concrete examples.

Figures (9)

• Figure 1: Outline of our approach.
• Figure 2: Simple types $\sigma, \tau$; simple contexts $\Gamma$; and terms $M, N$. In the definition above, $x$ ranges over variables, $b$ over base types in $\mathbf{Base}$, and $\mathbf{op}$ over basic operators in $\mathbf{BO}$. We assume variables in a context are mutually distinct.
• Figure 3: Selected typing rules.
• Figure 4: Typing rules for $\dot{\Gamma} \vdash M : \dot{\sigma}$.
• Figure 5: The standard typing rule for (the partial correctness) of recursion is unsound for fixed points.

Theorems & Definitions (106)

• theorem 1: from kura2023
• theorem 2: soundness
• proof
• corollary 1
• corollary 2: soundness of weakest pre-expectations and expected costs
• corollary 3: soundness of cost moment analyses
• corollary 4: soundness of the conditional weakest pre-expectations
• definition 1: admissible subset
• definition 2: admissible formula
• lemma 1