Efficient Discovery of Actual Causality in Stochastic Systems
summary
Formalizes Fenton‑Glynn probabilistic actual causality for discrete‑time Markov chains and reduces discovery to an SMT problem solved with Z3 using quantified real arithmetic and uninterpreted functions, including nonlinear probability sums. An abstraction‑refinement pipeline lifts DTMCs to MDPs, selects minimizing/maximizing schedulers, and restores concrete states until a cause is found. Case studies: Mountain Car (cause state s1: actual prob 0.345 vs counterfactual 0.15), Lunar Lander, and an F‑16 MPC; abstraction cuts solve time by up to 95% improvement and handles models up to 47,000 states via SMT encoding with Z3.
AI-written summary · about
chapters (17)
- 0:00Actual causality intro
- 1:25Causality challenges in stochastic systems
- 3:12Discrete-time Markov chains
- 5:25Probabilistic causality constraints
- 7:57Discovery as SMT problem
- 11:36Abstraction refinement for large models
- 13:41Abstraction refinement steps
- 15:07SMT encoding for MDPs
- 17:18States for refinement
- 18:05Case studies: lunar lander & F-16
- 20:35Performance: concrete vs abstraction
- 22:06Summary of contributions
- 23:11Future work in causality
- 23:53Q&A: SMT theory
- 26:22Q&A: Factual world quantification
- 27:31Q&A: Execution time differences
- 28:34Q&A: Predicates for refinement
related talks
01h 06mIntroduction to Causal Graphical Models: Graphs, d-separation, do-calculus
48mCausal Discovery in the Quantum Context
59mA Welcome to Causal Probabilistic Programming
14mA Unifying Approach to Product Constructions for Quantitative Temporal Inference
29m🧠🧹 Causality - Mental Hygiene for Data Science
01h 02mClassical Strategies and Concepts in Causal Discovery
43mControlling Probabilistic Systems Under Partial Observation
13mTyped Abstractions for Causal Probabilistic Programming