Automated Safety Verification of Posterior Distributions of Probabilistic Programs

Kazuki Watanabe; Hiroshi Unno

IJCAI 20260 citations

Automated Safety Verification of Posterior Distributions of Probabilistic Programs

Abstract

Ensuring the safety of probabilistic systems is a central challenge in formal verification. We propose an automated refinement technique for verifying a safety property of posterior distributions in probabilistic programs. Our approach builds on the counterexample-guided abstraction refinement (CEGAR) framework and exploits the duality in convex optimisation and the adequacy of predicate-transformer semantics in probabilistic settings. We implement the technique and evaluate its effectiveness through preliminary experiments.

AI Ethics, Trust, Fairnes: Safety and robustnessConstraint Satisfaction and Optimization: Constraint satisfactionConstraint Satisfaction and Optimization: SatisfiabiltyConstraint Satisfaction and Optimization: Solvers and toolsKnowledge Representation and Reasoning: Automated reasoning and theorem proving

BibTeX

@inproceedings{ijcai2026_automatedsafetyv,
  title = {Automated Safety Verification of Posterior Distributions of Probabilistic Programs},
  author = {Kazuki Watanabe and Hiroshi Unno},
  booktitle = {IJCAI 2026},
  year = {2026}
}