Automated Safety Verification of Posterior Distributions of Probabilistic Programs

Watanabe, Kazuki; Unno, Hiroshi

doi:10.24963/ijcai.2026/91

Automated Safety Verification of Posterior Distributions of Probabilistic Programs

Kazuki Watanabe, Hiroshi Unno

Download BibTeX Cite

Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence. Main Track. Pages 807-816.

https://doi.org/10.24963/ijcai.2026/91

Keywords

Constraint Satisfaction and Optimization: Constraint satisfaction
AI Ethics, Trust, Fairnes: Safety and robustness
Knowledge Representation and Reasoning: Automated reasoning and theorem proving
Constraint Satisfaction and Optimization: Solvers and tools
Constraint Satisfaction and Optimization: Satisfiabilty

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.

Kazuki Watanabe, and Hiroshi Unno. 2026. Automated Safety Verification of Posterior Distributions of Probabilistic Programs. In Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-26. IJCAI, 807–816. https://doi.org/10.24963/ijcai.2026/91

@inproceedings{ijcai2026p91,
  title     = {Automated Safety Verification of Posterior Distributions of Probabilistic Programs},
  author    = {Watanabe, Kazuki and Unno, Hiroshi},
  booktitle = {Proceedings of the Thirty-Fifth International Joint Conference on
               Artificial Intelligence, {IJCAI-26}},
  publisher = {International Joint Conferences on Artificial Intelligence Organization},
  editor    = {Diego Calvanese},
  pages     = {807--816},
  year      = {2026},
  month     = {8},
  note      = {Main Track},
  doi       = {10.24963/ijcai.2026/91},
  url       = {https://doi.org/10.24963/ijcai.2026/91},
}

TY  - CPAPER
TI  - Automated Safety Verification of Posterior Distributions of Probabilistic Programs
AU  - Watanabe, Kazuki
AU  - Unno, Hiroshi
T2  - Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-26
PB  - International Joint Conferences on Artificial Intelligence Organization
PY  - 2026
SP  - 807
EP  - 816
DO  - 10.24963/ijcai.2026/91
UR  - https://doi.org/10.24963/ijcai.2026/91
ER  -