# Verifying formulas for interventional distributions

arXiv: https://arxiv.org/abs/2607.13883 · HTML: https://mlsanity.com/paper/2607.13883/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 11 of its 45 references that are in the map.
- First posted on arXiv 15 Jul 2026.

## Builds on (most cited first, 11 of 11)

- [Nested Markov Properties for Acyclic Directed Mixed Graphs](https://mlsanity.com/paper/1701.06686/) (2017)
- [On the Testability of Causal Models with Latent and Instrumental Variables](https://mlsanity.com/paper/1302.4976/) (2013)
- [Margins of discrete Bayesian networks](https://mlsanity.com/paper/1501.02103/) (2015)
- [Adjustment Identification Distance: A gadjid for Causal Structure Learning](https://mlsanity.com/paper/2402.08616/) (2024)
- [Are Bayesian networks typically faithful?](https://mlsanity.com/paper/2410.16004/) (2024)
- [Variable elimination, graph reduction and efficient g-formula](https://mlsanity.com/paper/2202.11994/) (2022)
- [Linear-Time Algorithms for Front-Door Adjustment in Causal Graphs](https://mlsanity.com/paper/2211.16468/) (2022)
- [Unveiling the Structure of Do-Calculus Reasoning via Derivation Graphs](https://mlsanity.com/paper/2606.03719/) (2026)
- [On Probabilistic and Causal Reasoning with Summation Operators](https://mlsanity.com/paper/2405.03069/) (2024)
- [Deriving Complete Constraints in Hidden Variable Models](https://mlsanity.com/paper/2601.11242/) (2026)
- [Complete Causal Identification from Ancestral Graphs under Selection Bias](https://mlsanity.com/paper/2603.26301/) (2026)

## Abstract (arXiv)

We formalize verification in causal graphical models: deciding whether a given observational formula identifies a target interventional distribution. This opens a problem complementary to identification, asking not whether any identifying formula exists, but whether the given formula is identifying. We show that even sound and complete solutions to identification do not solve verification. We propose a falsifier as a first practical route forward, prove that it induces an almost-surely correct verifier for regular exponential-family models, and use the resulting verifier to develop the gateway test, which finds all sets admissible for use in a front-door formula.