Verifying formulas for interventional distributions Francesco Freni1 and Leonard Henckel2,* and Sebastian Weichwald1,* 1 Department of Mathematical Sciences, University of Copenhagen, Denmark 2 School of Mathematics and Statistics, University College Dublin, Ireland * Equal contribution.
arXiv:2607.13883v1 [stat.ME] 15 Jul 2026
Abstract 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. Keywords: Causal graphical models; Falsification; Identification; Verification.
1 Introduction We introduce and formalize the problem of verification in causal graphical models (Pearl, 2009): given a graph, treatment and outcome variables, and a candidate observational formula, decide whether that formula identifies the target interventional distribution. This opens a problem complementary to identification, which asks whether the target interventional distribution is determined by the graph and observational distribution, and, if so, how to express it as an observational formula (Pearl, 1995a). This new problem also requires making explicit what is often left implicit in identification: specifying which observational formulas are admissible in the first place. There exists a rich literature on identification, including graphical criteria (Maathuis and Colombo, 2015; Perković et al., 2018), sound and complete algorithms using graphical decompositions and do-calculus (Tian and Pearl, 2002; Huang and Valtorta, 2006; Shpitser and Pearl, 2008; Jaber et al., 2022; Chen and Mooij, 2026), and extensions to surrogate experiments, stochastic policies, and statistical efficiency analysis (Bareinboim and Pearl, 2012; Correa and Bareinboim, 2020; Witte et al., 2020; Henckel et al., 2022; Rotnitzky and Smucler, 2020). Some existing results can be repurposed to verify formulas in restricted classes, for example linear instrumental-variable formulas (Henckel et al., 2023) or adjustment formulas (Shpitser et al., 2010; Perković et al., 2018). But verification itself has not been developed as a problem in its own right. Verification matters for causal graphical modelling. Conceptually, proof assistants such as Lean highlight the value of independently checking that a proposed mathematical object has the claimed meaning (de Moura and Ullrich, 2021); here, the object is an observational formula claimed to be identifying for a target interventional distribution. Practically, candidate formulas need not be direct outputs of a single identification run: they may be simplified expressions, outputs of software or human derivations, formulas transferred from related graphs, or alternatives expected to be easier to estimate efficiently (Guo et al., 2023). This is important to enable evolvable causal analysis, where graphs, assumptions, measurements, and formulas change over time. The question is then not whether
1
some identifying formula exists, but whether this particular formula remains correct for the causal model currently under consideration. Methodologically, verification can help check derivations, test graphical criteria and conjectures, expose new graphical implications or identifying formulas, and support downstream tasks such as comparing graphs by the identification claims they share (Henckel et al., 2024). We first show why verification is not a by-product of the existing identification machinery. Sound and complete identification algorithms such as ID (Shpitser and Pearl, 2006) return an identifying formula when one exists, but do not decide whether a given alternative formula is also identifying. Direct proof search in the do-calculus proof system does not solve the verification problem either: fair enumeration of do-calculus and probability-algebra derivations only semi-decides derivability of a candidate formula, terminating with a certificate when a derivation exists but potentially running forever otherwise (Theorem 3.4). We then propose a falsifier as a first practical route forward. Rather than searching for a derivation of the candidate formula, the falsifier searches for disagreement between the candidate formula and the target interventional distribution in sampled graph-compatible models. For regular conditional exponential-family models, we prove that this induces an almost-surely correct verifier relative to the chosen parametric family (Theorem 4.9). Finally, we illustrate what verification enables by developing the gateway test, a sound and exhaustively complete procedure for finding all sets whose front-door formula identifies the target interventional distribution. This shows that verification can also characterize identifying strategies. Our code is available at github.com/francescofreni/hiprof. We close by outlining open directions toward a broader study of verification, including strengthening falsification from parametric toward non-parametric guarantees, clarifying the limits of do-calculus proof search, and extending verification beyond equality of interventional formulas.
2 Causal graphical models and identification We fix working notation and definitions here, collecting graphical and causal background in Appendix A. Throughout, let G be a causal directed acyclic graph over V = O ⊔ L, with observed variables O, latent variables L, and disjoint outcome and intervention node sets Y, T ⊆ O. Let G 𝑝 be the latent projection of G onto O (Verma and Pearl, 1990; Richardson, 2003), and let A (O) denote the class of latent projections (or acyclic directed mixed graphs) over O. Î For A ⊆ V, set the product sample space XA = 𝑉 ∈A X𝑉 and let 𝜇A be the corresponding product measure. All distributions considered admit densities with respect to the relevant 𝜇A , and P (XA ) denotes the class of such densities. A density 𝑞 ∈ P (XV ) factorizes according to G if there Î exist conditional densities {𝑞 𝑉 |pa(𝑉 ) : 𝑉 ∈ V}, such that 𝑞(v) = 𝑉 ∈V 𝑞 𝑉 |pa(𝑉 ) (v𝑉 | vpa(𝑉 ) ) for 𝜇V -almost every v. Let PG (XV ) denote the class of such full densities. The causal directed acyclic graph G, together with this factorization and truncated factorizations for interventions, specifies a non-parametric causal graphical model: each 𝑞 ∈ PG (XV ) induces a marginal observational density 𝑞O and a family of interventional densities; for t ∈ XT , we write 𝑞Y|do(T=t) for the induced density of Y under the hard intervention do(T = t) (see Appendix A.2). Definition 2.1 (Observational formula). An observational formula 𝜙 for Y under intervention on T is a well-typed, kernel-preserving symbolic expression with no free variables other than y and t, generated from observational marginals and conditionals by the grammar in Appendix B. The grammar restricts products and quotients so that formulas have probabilistic rather than merely
2
algebraic semantics. We write ⟦𝜙⟧ : P (XO ) × XT ⇀ P (XY ) for the partial functional induced by an admissible formula 𝜙, and ΦY,T for the class of such formulas. The grammar excludes arbitrary algebraic expressions that need not define densities (see Appendix B), and covers standard identifying formulas, including those derived via do-calculus and those written using fixing notation via their underlying kernel-preserving operations (Richardson et al., 2023). When unambiguous, we use the standard shorthand that the arguments of a density symbol determine the corresponding marginal, conditional, or interventional density. Densities and conditional-density terms are understood up to the usual almost-everywhere equivalence; pointwise evaluations are taken only where the chosen representatives are defined. In observational formulas, marginalization sums are shorthand for integration with respect to the relevant measures; primed or subscripted bound variables are dummy copies of the corresponding base variable; for example, 𝑡 ′ and 𝑡1 range over X𝑇 and are integrated with respect to 𝜇𝑇 . Definition 2.2 (Identifying formula). An observational formula 𝜙 is identifying for Y | do(T) in G if, for every 𝑞 ∈ PG (XV ) and every t ∈ XT for which ⟦𝜙⟧(𝑞O , t) is defined, ⟦𝜙⟧(𝑞O , t) = 𝑞Y|do(T=t)
𝜇Y -almost everywhere.
(1)
eG (XV ) ⊆ PG (XV ) if the above equality We say that 𝜙 is identifying for Y | do(T) in G relative to P eG (XV ) and every t ∈ XT . holds for every 𝑞 ∈ P Example 2.3 (Interpreting an observational formula). Consider the graph 𝑋 → 𝑇 → 𝑌 and Í 𝑋 → 𝑌 . The observational formula 𝜙adj = 𝑥 𝑝(𝑦 | 𝑡,∫𝑥) 𝑝(𝑥) with free variables 𝑦 and 𝑡 denotes a functional ⟦𝜙adj ⟧ that maps (𝑞O , 𝑡) to the density 𝑦 ↦→ 𝑞𝑌 |𝑇 ,𝑋 (𝑦 | 𝑡, 𝑥)𝑞𝑋 (𝑥) 𝑑𝜇𝑋 (𝑥) on X𝑌 . Since {𝑋 } is a valid adjustment set in this graph, 𝜙adj is identifying for 𝑌 | do(𝑇), while the observational formula 𝑝(𝑦 | 𝑡) is not. Graphical identifiability depends only on the latent projection: 𝜙 is identifying for Y | do(T) in G 𝑝 if and only if it is identifying in any, equivalently every, full graph G whose latent projection onto O is G 𝑝 (Richardson et al., 2023, Corollary 49). For H ∈ {G, G 𝑝 }, we say that Y | do(T) is identifiable in H if and only if there exists 𝜙 ∈ ΦY,T that is identifying for Y | do(T) in H . Identification asks whether Y | do(T) is identifiable and, when it is, provides an identifying formula for Y | do(T). We view an identification procedure I with associated, possibly restricted, I formula class ΦY,T ⊆ ΦY,T abstractly as assigning to each latent projection G 𝑝 ∈ A (O) and I disjoint node sets Y, T ⊆ O, a set of formulas I (G 𝑝 , Y, T) ⊆ ΦY,T . The procedure is sound (for 𝑝 identification) if each 𝜙 ∈ I (G , Y, T) is identifying for Y | do(T). The procedure is complete (for identification) if it returns at least one identifying formula whenever Y | do(T) is identifiable in G 𝑝 . I The procedure is exhaustively complete relative to ΦY,T if it is complete for finding all identifying I I formulas in ΦY,T , that is, for every 𝜙 ∈ ΦY,T , if 𝜙 is identifying for Y | do(T), then 𝜙 ∈ I (G 𝑝 , Y, T).
3
G1
𝐶
𝑇
𝑀 Í
G2
𝐶
𝑇
𝑀
𝑌
𝑌
ID output: 𝜙2 = 𝑝(𝑦 | 𝑡) Í Í Identifying in both graphs: 𝜙3 = 𝑚 𝑝(𝑚 | 𝑡) 𝑡 ′ 𝑝(𝑦 | 𝑡 ′ , 𝑚) 𝑝(𝑡 ′ )
ID output: 𝜙1 =
𝑐 𝑝(𝑦 | 𝑡, 𝑐) 𝑝(𝑐)
Figure 1: The ID algorithm returns one identifying formula for Y | do(T) when one exists; here, the adjustment formula 𝜙1 in G1 and the conditional density 𝜙2 in G2 . Each formula is specific to its graph and fails in the other: V (G1 , 𝑌 , 𝑇, 𝜙2 ) = false and V (G2 , 𝑌 , 𝑇, 𝜙1 ) = false. Conversely, non-return by ID is not evidence of a formula being non-identifying: the front-door formula 𝜙3 is identifying in both graphs, but is not the formula returned by ID in either. Thus, completeness for identification is an existence guarantee, insufficient to enable verification of arbitrary formulas.
3 The verification problem Identification asks for some identifying observational formula for a target Y | do(T). Verification is the complementary decision problem: given a graph, a target, and a proposed answer, decide whether that answer is correct. We formalize this decision task as follows. Definition 3.1 (Verifier). A verifier V is a decision procedure, that is, a Boolean-valued algorithm that halts on every valid input, computing the following map. It takes as input a latent projection G 𝑝 ∈ A (O), disjoint node sets Y, T ⊆ O, and either an observational formula 𝜙 ∈ ΦY,T or the symbol none. Let G be any latent-variable causal directed acyclic graph whose latent projection onto O is G 𝑝 . The verifier returns true if and only if one of the following holds: 1. 𝜙 ∈ ΦY,T and 𝜙 is identifying for Y | do(T) in G; or 2. 𝜙 = none and Y | do(T) is not identifiable in G. Otherwise, V returns false. The verification task is not solved by identification alone. A sound and complete identification procedure need only return some identifying formula when one exists, and therefore need not decide whether an arbitrary observational formula is identifying. This applies, for instance, to the ID algorithm, which halts on every valid input and returns an identifying formula when the target is identifiable, and reports non-identifiability otherwise (Shpitser and Pearl, 2006). One can also obtain some more, but not necessarily all, identifying formulas using the approach of Yvernes et al. (2026). Figure 1 illustrates why this is not enough to decide whether an arbitrary observational formula is identifying. While an identification procedure I that is sound and exhaustively complete relative to a formula I class ΦY,T , such as adjustment formulas (see Appendix C), may be repurposed for verification by checking whether a formula belongs to I (G 𝑝 , Y, T), it can at best verify formulas within that class, not arbitrary formulas in ΦY,T . One might therefore try to make the class as broad as possible, but this does not remove the difficulty and instead shifts it to deciding membership in I (G 𝑝 , Y, T). 4
The natural broad route is proof search: try to verify a candidate observational formula by searching for a derivation of that formula in the do-calculus proof system (Pearl, 1995a, Section 4; see also Appendix D). Soundness of do-calculus guarantees that observational formulas derived by a sequence of derivation steps starting from the target are identifying for the target, and completeness guarantees that some identifying formula is derivable whenever the target is identifiable (Shpitser and Pearl, 2006; Huang and Valtorta, 2006). Since our observational formulas are written in the same symbolic density language used in do-calculus derivations, this is a meaningful route. However, it turns verification into a derivability problem. We next formalize this problem and show that direct proof search via fair enumeration of derivations only semi-decides it: derivable formulas are eventually accepted, with the derivation serving as a certificate, whereas non-derivable formulas need not lead to termination. 3.1 The limits of do-calculus proof search for verification Let Σ be a finite alphabet containing the symbols needed to write the density expressions, interventions, algebraic operations, and marginalizations considered below. Let Σ∗ denote the set of finite strings over Σ and let L do-calc ⊆ Σ∗ be the language of well-formed symbolic density expressions used in do-calculus and probability-algebra derivations. Since we fix this syntax throughout, membership do-calc ⊆ L do-calc of strings representing observational in the language L do-calc and in the subclass ΦY,T formulas for Y under intervention on T is decidable, in the sense that there is an algorithm that halts on every input and correctly determines membership. For simplicity, we take R to be a finite set of sound rule schemas for symbolic density expressions, including the do-calculus and probability-algebra schemas; finiteness simplifies the enumeration argument below, but effective enumerability of rules and decidable rule applicability would suffice. Definition 3.2 (Derivation). A derivation of length 𝑚 ∈ N from a starting query expression 𝜉 0 = 𝑄Y,T is a finite sequence 𝑑 𝑚 = ( 𝑗1 , . . . , 𝑗 𝑚 ) that determines a sequence of expressions 𝜉 1 , . . . , 𝜉 𝑚 ∈ L do-calc by a computable transition function. For all 𝑘 ∈ {1, . . . , 𝑚}, 𝑗 𝑘 : 𝑎 𝑘 ⇝ 𝑏 𝑘 is a local rewrite step, where 𝑎 𝑘 is an occurrence of a probability-kernel sub-expression of 𝜉 𝑘−1 , and 𝑏 𝑘 is the expression obtained from 𝑎 𝑘 by one application of a rule schema in R. The next expression 𝜉 𝑘 is obtained from 𝜉 𝑘−1 by replacing the selected occurrence of 𝑎 𝑘 with 𝑏 𝑘 . The derivation is valid relative to G 𝑝 if all steps are well-formed and all graph-dependent side conditions of the applied rules hold in G 𝑝 . do-calc , a derivation 𝑑 derives 𝜙 from 𝑄 Given a candidate observational formula 𝜙 ∈ ΦY,T 𝑚 Y,T in 𝑝 G if the expression obtained after applying all its rewrite steps, 𝜉 𝑚 , is syntactically equal to 𝜙; the
following example illustrates this. Example 3.3 (Front-door formula derivation). Consider the graph G1 in Figure 1 and the query 𝜉 0 = 𝑄𝑌 ,𝑇 = 𝑝(𝑦 | do(𝑡)). Using probability manipulations and the do-calculus rules stated in Appendix D, a possible derivation of the front-door formula 𝜙3 is the finite sequence 𝑑7 = ( 𝑗1 , . . . , 𝑗 7 ),
5
where 𝑗1 :
𝑝(𝑦 | do(𝑡)) ⇝
∑︁
𝑝(𝑦 | do(𝑡), 𝑚) 𝑝(𝑚 | do(𝑡)),
marginalizing over 𝑀;
𝑚
𝑗2 :
𝑝(𝑚 | do(𝑡)) ⇝ 𝑝(𝑚 | 𝑡),
by Rule 2 of do-calculus;
𝑗3 :
𝑝(𝑦 | do(𝑡), 𝑚) ⇝ 𝑝(𝑦 | do(𝑡, 𝑚)),
by Rule 2 of do-calculus;
𝑗4 :
𝑝(𝑦 | do(𝑡, 𝑚)) ⇝ 𝑝(𝑦 | do(𝑚)),
by Rule 3 of do-calculus;
𝑗5 :
𝑝(𝑦 | do(𝑚)) ⇝
∑︁
𝑝(𝑦 | do(𝑚), 𝑡 ′ ) 𝑝(𝑡 ′ | do(𝑚)),
marginalizing over 𝑇;
𝑡′
𝑗6 :
𝑝(𝑡 ′ | do(𝑚)) ⇝ 𝑝(𝑡 ′ ),
by Rule 3 of do-calculus;
𝑗7 :
𝑝(𝑦 | do(𝑚), 𝑡 ′ ) ⇝ 𝑝(𝑦 | 𝑚, 𝑡 ′ ),
by Rule 2 of do-calculus.
Applying these local rewrites successively to 𝜉 0 yields 𝜙3 . Thus, we say that this particular derivation 𝑑7 derives 𝜙3 from 𝑄𝑌 ,𝑇 in G1 . Let 𝐷 𝑚 be the set of all length-𝑚 derivations, and consider 𝑄Y,T := 𝑝(y | do(t)) as starting query expression. Let Check(𝐺 𝑝 , 𝑄Y,T , 𝜙, 𝑑 𝑚 ) be an algorithm taking as input the graph G 𝑝 and query do-calc , and a derivation 𝑑 ∈ 𝐷 ; Check returns true if 𝑑 𝑄Y,T , an observational formula 𝜙 ∈ ΦY,T 𝑚 𝑚 𝑚 𝑝 is a valid derivation relative to G that derives 𝜙, and false otherwise. We consider the set of observational formulas that are derivable from 𝑄Y,T in finitely many steps, and are hence identifying formulas, as do-calc I do-calc (G 𝑝 , Y, T) = {𝜙 ∈ ΦY,T | ∃𝑚 ∈ N, 𝑑 𝑚 ∈ 𝐷 𝑚 : Check(G 𝑝 , 𝑄Y,T , 𝜙, 𝑑 𝑚 ) = true},
which formally defines a language over Σ as well as a sound and complete identification procedure. do-calc . This do-calculus-based identification procedure may even be exhaustively complete relative to ΦY,T Nevertheless, this does not by itself provide a verifier for arbitrary candidate formulas, because membership in the derivable set I do-calc (G 𝑝 , Y, T) is only semi-decidable. Recall that a language 𝐿 ⊆ Σ∗ is semi-decidable if there is an algorithm that halts and accepts on inputs in 𝐿, while it may run forever on inputs outside 𝐿. Theorem 3.4 (Semi-decidability of derivation search). I do-calc (G 𝑝 , Y, T) is semi-decidable. We provide a proof in Appendix E.1. It constructs an algorithm that fairly enumerates all candidate do-calc ; if none exists, the search derivations and halts once it finds one that derives a given 𝜙 ∈ ΦY,T continues forever. Example 3.5 (Non-terminating derivation search). Consider the graph G2 in Figure 1 and the query 𝑄𝑌 ,𝑇 = 𝑝(𝑦 | do(𝑡)). To see that the adjustment formula 𝜙1 is not identifying for 𝑌 | do(𝑇) in G2 , we provide a counterexample for which the formula and the target disagree. Consider the Gaussian density 𝑝 that factorizes according to G2 with 𝑇 ∼ N (0, 1), 𝑀 | 𝑇 = 𝑡 ∼ N (𝑡, 1), 𝑌 | 𝑀 = 𝑚 ∼ N (𝑚, 1), and 𝐶 | 𝑇 = 𝑡, 𝑌 = 𝑦 ∼ N (𝑡 + 𝑦, 1). Under do(𝑇 = 1), the interventional 6
distribution is 𝑌 | do(𝑇 = 1) ∼ N (1, 2). On the other hand, 𝐶 ∼ N (0, 7) and, for fixed 𝑐, 𝑌 |𝑇 = 1, 𝐶 = 𝑐 ∼ 𝑁 (2𝑐/3 − 1/3, 2/3), and hence 1 34 ≠ N (𝑦; 1, 2) = 𝑝𝑌 |do(𝑇=1) (𝑦). ⟦𝜙1 ⟧( 𝑝, 1) (𝑦) = N 𝑦; − , 3 9 We explain what happens if one tries to verify 𝜙1 by derivation search. For all 𝑚 ∈ N and all 𝑑 𝑚 ∈ 𝐷 𝑚 , Check(G2 , 𝑄𝑌 ,𝑇 , 𝜙1 , 𝑑 𝑚 ) = false, because otherwise, by soundness of R, 𝜙1 would be identifying, contradicting the counterexample above. However, this does not allow the procedure to halt and reject, because the derivation space has no finite bound. Indeed, even from the target expression, one can insert probabilistic identities leaving the represented kernel unchanged. For example, we may rewrite ∑︁ 𝑝(𝑦 | do(𝑡)) ⇝ 𝑝(𝑦 | do(𝑡)) 𝑝(𝑐 | 𝑦, do(𝑡)) ⇝ 𝑝(𝑦 | do(𝑡)), 𝑐
Í
because 𝑐 𝑝(𝑐 | 𝑦, do(𝑡)) = 1. This is a valid two-step derivation loop. For all 𝑘 ∈ N, one may insert this loop 𝑘 times before applying any other rewrite, which gives arbitrarily long valid candidate derivations. After checking finitely many candidate derivations, the procedure has ruled out only finitely many candidates, but there remain longer derivations that have not yet been checked. Theorem 3.4 does not rule out the existence of a terminating decision procedure for derivability. Such a procedure would exist, for example, if one could compute a finite bound 𝐵, possibly depending on the input, such that, whenever 𝜙 is derivable, it has a valid derivation of length at most 𝐵. One could then enumerate all derivations up to length 𝐵, accept if one of them derives 𝜙, and reject otherwise. Alternatively, a terminating procedure might search the derivation space while somehow ignoring redundant detours such as the one in Example 3.5. We are not aware of such a terminating procedure for the derivability problem considered here, and this problem may even be undecidable, meaning that no algorithm can correctly decide all instances while halting on every input. While we do not prove such a result, this impossibility is in line with known undecidability results for closely related probabilistic and causal reasoning problems (Ibeling et al., 2025). The verification task therefore remains open as a separate problem, despite a rich identification literature.
4 A falsification-based verifier 4.1 Falsification procedure Our strategy to verification is based on falsification: instead of attempting to prove that Equation (1) holds for all densities factorizing according to the graph, we search for a counterexample violating it. This yields a verification procedure for parametric submodels (Theorem 4.9). We consider a parametric family {𝑝 𝜃 } 𝜃 ∈Θ := {{𝑝 𝜃𝑉 (𝑣 | vpa(𝑉 ) )} 𝜃𝑉 ∈Θ𝑉 }𝑉 ∈V of densities factorÎ izing according to G, where, for all 𝑉 ∈ V, Θ𝑉 ⊆ R𝑑𝑉 , and Θ := 𝑉 ∈V Θ𝑉 ⊆ R𝑑 . For all 𝑉 ∈ V, let 𝜋𝑉 be a Ë distribution on Θ𝑉 that is absolutely continuous with respect to the Lebesgue measure, and let 𝜋 := 𝑉 ∈V 𝜋𝑉 be the joint distribution on Θ. We write PΘ (XV ) ⊆ PG (XV ) for the parametric submodel induced by this family. Then, a falsifier is defined as follows. Definition 4.1 (Falsifier). A falsifier F is a decision procedure, that is, a Boolean-valued algorithm that halts on every valid input, computing the following map. It takes as input a latent projection 7
G 𝑝 ∈ A (O), disjoint node sets Y, T ⊆ O, and either an observational formula 𝜙 ∈ ΦY,T or the symbol none. Let G be any latent-variable causal directed acyclic graph whose latent projection onto O is G 𝑝 , and consider a parametric family {𝑝 𝜃 } 𝜃 ∈Θ of densities factorizing according to G. Let 𝜃 1 , . . . , 𝜃𝐾 , with 𝐾 ∈ N, be independent draws from 𝜋. Then, conditioned on {𝑝 𝜃 } 𝜃 ∈Θ and on the realized parameter values, F returns true if and only if one of the following holds: 1. 𝜙 ∈ ΦY,T , and, for all 𝑖 ∈ {1, . . . , 𝐾 } and all t ∈ XT , ⟦𝜙⟧( 𝑝 𝜃𝑖 ,O , t) = 𝑝 𝜃𝑖 ,Y|do(T=t)
𝜇Y -almost everywhere; or
2. 𝜙 = none and Y | do(T) is not identifiable in G. Otherwise, F returns false. We say that a falsifier is an almost-surely correct verifier relative to PΘ (XV ) if, with probability one over the sampled parameters, it returns true exactly when either 𝜙 ∈ ΦY,T is identifying for Y | do(T) in G relative to PΘ (XV ), or 𝜙 = none and Y | do(T) is not identifiable in G. When 𝜙 is none (Case 2), we use the ID algorithm to check identifiability, which has been shown to be sound and complete (for identification) (Shpitser and Pearl, 2006). Case 1, instead, involves two nontrivial tasks: (a) deciding whether two densities agree 𝜇Y -almost everywhere, and (b) checking this equality for all intervention values t ∈ XT . Both tasks can be difficult for general parametric families, but in our implementation we use the canonical directed acyclic graph associated with G 𝑝 , where each bidirected edge 𝑎 ↔ 𝑏 is represented by an additional variable 𝑢 with 𝑎 ← 𝑢 → 𝑏 (an alternative implementation avoids specifying the latent structure; we discuss its trade-offs in Appendix F), and use a linear Gaussian parametrization, which makes the above problems tractable. To obtain the interventional density, we remove all incoming edges into the treatment variables and set the treatment variables to their intervened values. In this linear Gaussian setting, all relevant densities are Gaussian (see the closure result in Appendix B.1). Therefore, task (a) reduces to comparing mean vectors and covariance matrices. Moreover, by the same closure result, admissible formula outputs have mean affine in t and covariance independent of t, and for fixed parameters, task (b) reduces to comparing the covariance matrices and comparing the mean functions at |T| + 1 affinely independent intervention values. Example 4.2 (Falsification in a Gaussian model). Consider the acyclic directed mixed graph G 𝑝 : 𝑇 ← 𝐶 ↔ 𝑌 and the query 𝑄𝑌 ,𝑇 = 𝑝(𝑦 | do(𝑡)). For parametric falsification, consider the canonical directed acyclic graph G : 𝑇 ← 𝐶 ← 𝐿 → 𝑌 with the centred linear Gaussian model: 𝐿 ∼ N (0, 𝜎𝐿2 ), 𝐶 | 𝐿 = 𝑙 ∼ N (𝜆𝐿𝐶 𝑙, 𝜎𝐶2 ), 𝑇 | 𝐶 = 𝑐 ∼ N (𝜆𝐶𝑇 𝑐, 𝜎𝑇2 ), and 𝑌 | 𝐿 = 𝑙 ∼ N (𝜆𝐿𝑌 𝑙, 𝜎𝑌2 ), where 𝜃 = (𝜆𝐶𝑇 , 𝜆𝐿𝐶 , 𝜆𝐿𝑌 , 𝜎𝑇2 , 𝜎𝐶2 , 𝜎𝐿2 , 𝜎𝑌2 ) collects the parameters of the induced joint. The centering is only for exposition: intercepts leave the covariance calculations unchanged and add affine terms to the means. For compactness, write 𝑞 := 𝜆2𝐿𝐶 𝜎𝐿2 + 𝜎𝐶2 , 𝑠𝑇𝐶 := 𝜆𝐶𝑇 𝑞,
2 𝑣 𝑇 := 𝜆𝐶𝑇 𝑞 + 𝜎𝑇2 ,
𝑣𝑌 := 𝜆2𝐿𝑌 𝜎𝐿2 + 𝜎𝑌2 ,
𝑠𝑌𝑇 := 𝜆𝐶𝑇 𝜆𝐿𝐶 𝜆𝐿𝑌 𝜎𝐿2 , 𝑠𝑌𝐶 := 𝜆𝐿𝐶 𝜆𝐿𝑌 𝜎𝐿2 ,
2 Δ := 𝑣 𝑇 𝑞 − 𝑠𝑇𝐶 .
The induced joint, observed joint, and interventional distribution are Gaussian, and by the closure result in Appendix B.1, each admissible formula returns a Gaussian density. Thus checking 𝜇𝑌 -almost everywhere equality reduces to comparing mean and covariance parameters. 8
Under the intervention do(𝑇 = 𝑡), truncating the factor for childless 𝑇 yields 𝑝 𝜃 ,𝑌 |do(𝑇=𝑡 ) (𝑦) = N (𝑦; 0, 𝑣𝑌 ). We now compare this target with the outputs of two candidate observational formulas: Í 𝜙1 := 𝑝(𝑦 | 𝑡) and 𝜙2 := 𝑐 𝑝(𝑦 | 𝑡, 𝑐) 𝑝(𝑐). The expressions below are obtained mechanically from the observed joint by Gaussian marginalization, conditioning, and kernel composition. We intentionally leave the resulting rational expressions unsimplified to reflect the form manipulated by the implementation. In principle, equality could be checked symbolically by reducing the resulting rational polynomial identities (showing it is decidable), but in practice this becomes computationally expensive beyond toy examples; the two formulas below already illustrate how quickly the expressions grow. Consider 𝜙1 first. Marginalizing the observed joint to (𝑇, 𝑌 ) and conditioning on 𝑇 = 𝑡 yields ! 2 𝑠𝑌𝑇 𝑠𝑌𝑇 ⟦𝜙1 ⟧( 𝑝 𝜃 , 𝑡) (𝑦) = N 𝑦; 𝑡, 𝑣𝑌 − . 𝑣𝑇 𝑣𝑇 These parameters generally differ from the target parameters. Thus, a single sampled parameter value at which either the mean or the variance differs is enough to falsify 𝜙1 . However, on the lower-dimensional subset {𝜃 : 𝜆𝐶𝑇 = 0}, we have 𝑠𝑌𝑇 = 0, and hence 𝜙1 agrees with the target for every 𝑡, even though it is not identifying in the graph. Consider now 𝜙2 . Starting from the observed joint, conditioning gives the first factor, marginalization gives the second, and marginalizing their product over 𝑐 gives ⟦𝜙2 ⟧( 𝑝 𝜃 , 𝑡) (𝑦) ! 2 𝑞 − 2𝑠 2 −𝑠 𝑠 + 𝑠 𝑣 2 𝑠𝑌𝑇 𝑠𝑌𝑇 𝑞 − 𝑠𝑌𝐶 𝑠𝑇𝐶 𝑌𝑇 𝑠𝑌𝐶 𝑠𝑇𝐶 + 𝑠𝑌𝐶 𝑣 𝑇 𝑌𝑇 𝑇𝐶 𝑌𝐶 𝑇 𝑞 . = N 𝑦; 𝑡, 𝑣𝑌 − + Δ Δ Δ Symbolic simplification reduces the displayed mean to 0 and the displayed variance to 𝑣𝑌 , so 𝜙2 agrees with the target. In the falsification procedure, we instead compare the induced Gaussian parameters at sampled parameter values 𝜃 1 , . . . , 𝜃𝐾 . The equality is required for all intervention values 𝑡, but in the linear Gaussian setting the means are affine in 𝑡 and the variances are independent of 𝑡 (Appendix B.1). Since |𝑇 | = 1 here, it is enough to compare the mean functions at two distinct intervention values 𝑡0 , 𝑡1 . A disagreement at any sampled parameter value and intervention value falsifies the formula. Agreement at finitely many sampled parameter values does not prove identification: a non-identifying formula can agree with the target accidentally on special parameter values, as 𝜙1 does when 𝜆𝐶𝑇 = 0. Below, we show that such accidents form measure-zero sets under the sampling distribution. 4.2 Almost-sure correct verifier When 𝜙 ∈ ΦY,T is identifying, Equation (1) holds for all densities factorizing according to the graph whenever 𝜙 is well-defined; hence, a counterexample found by the falsifier certifies that 𝜙 is non-identifying. If the falsifier does not find a counterexample, two cases remain possible: (i) 𝜙 is non-identifying relative to PΘ (XV ), but the sampled parameter values happen to lie in a set on which the formula agrees with the target (for instance, in Example 4.2, no witnessing counterexample is found for 𝜙1 if all sampled parameter values lie in {𝜃 : 𝜆𝐶𝑇 = 0}); (ii) 𝜙 is identifying relative to PΘ (XV ). We address the first case by restricting our focus on conditional exponential families and show that, under regularity assumptions, (i) happens only on a nowhere dense measure-zero subset of the parameter space (Proposition 4.8). 9
Definition 4.3 (Conditional exponential-family parametrization). A parametric family {𝑝 𝜃 } 𝜃 ∈Θ of densities factorizing according to G is said to admit a conditional exponential-family parametrization if, for all 𝑉 ∈ V and 𝜃 𝑉 ∈ Θ𝑉 , ⊤
𝑝 𝜃𝑉 (𝑣 | vpa(𝑉 ) ) = 𝑏 𝑉 (𝑣, vpa(𝑉 ) ) 𝑒 𝜂𝑉 ( 𝜃𝑉 ) 𝑠𝑉 (𝑣,vpa(𝑉 ) ) − 𝐴𝑉 ( 𝜂𝑉 ( 𝜃𝑉 ) ,vpa(𝑉 ) ) , where 𝑏 𝑉 : X𝑉 × Xpa(𝑉 ) → [0, ∞) is a non-negative function, 𝜂𝑉 : Θ𝑉 → R 𝑘𝑉 is the natural parameter, and 𝑠𝑉 : X𝑉 × Xpa(𝑉 ) → R 𝑘𝑉 is the sufficient statistic, with 𝑘 𝑉 ∈ N. For all 𝑉 ∈∫ V, 𝜃 𝑉 ∈ Θ𝑉 and vpa(𝑉 ) ∈ Xpa(𝑉 ) , 𝐴𝑉 (𝜂𝑉 (𝜃 𝑉 ), vpa(𝑉 ) ) < ∞, where 𝐴𝑉 (𝜂𝑉 (𝜃 𝑉 ), vpa(𝑉 ) ) := ⊤ log X 𝑏 𝑉 (𝑣, vpa(𝑉 ) )𝑒 𝜂𝑉 ( 𝜃𝑉 ) 𝑠𝑉 (𝑣,vpa(𝑉 ) ) d𝜇𝑉 (𝑣) is the normalizer. 𝑉
Given a conditional exponential-family parametrization {𝑝 𝜃 } 𝜃 ∈Θ of densities factorizing according to G and an observational formula 𝜙, we introduce the following assumptions, which are satisfied for the linear Gaussian submodel in our implementation. Assumption 4.4 (Open and connected parameter space). For all 𝑉 ∈ V, Θ𝑉 is open and connected. Assumption 4.5 (Analyticity of the natural parameters). For all 𝑉 ∈ V, the map 𝜃 𝑉 ↦→ 𝜂𝑉 (𝜃 𝑉 ) is analytic with open image 𝜂𝑉 (Θ𝑉 ). Assumption 4.6 (Regularity). For all t ∈ XT , {𝑝 𝜃 ,X|do(T=t) (x)} 𝜃 ∈Θ , where X = V \ T, form a regular exponential family. ⊤ Regularity implies that, for all 𝜃 ∈ Θ and all t ∈ XT , 𝑝 𝜃 ,X|do(T=t) (x) ∝ e 𝑏t (x)𝑒 𝜂et ( 𝜃 ) e𝑠t (x) , where e 𝑏t : XX → [0, ∞), 𝜂et : Θ → R 𝑘t , and e 𝑠t : XX → R 𝑘t , with 𝑘t ∈ N, are such that the parametrization is minimal, full, and 𝜂et (Θ) is open (Barndorff-Nielsen, 2014, p. 116). Here, minimality refers to affine independence of the components of 𝜂et and 𝜇x -almost independence of the components ∫ sure affine 𝛾t⊤ e 𝑠t (x) 𝑘 t e of e 𝑠t , while fullness means that 𝜂et (Θ) = {𝛾t ∈ R : 𝑏t (x)𝑒 d𝜇x (x) < ∞}. This assumption holds, for example, for discrete and Gaussian but not arbitrary conditional exponential-family parametrizations (Boeken et al., 2026).
Assumption 4.7 (Analyticity of the candidate formula). There exists a measurable set 𝐸 ⊆ XY of full measure such that, for all y ∈ 𝐸 and all t ∈ XT , the map 𝜃 ↦→ ⟦𝜙⟧( 𝑝 𝜃 ,O , t) (y) is analytic on Θ. Under Assumptions 4.4–4.6, the observational marginal densities that form the base terms of our grammar are analytic in the parameters (Boeken et al., 2026, Theorem 8). In the non-degenerate linear Gaussian case considered in our implementation, the same holds for the conditional densities. Indeed, the mean and covariance parameters of the marginal and conditional Gaussian base terms are analytic in 𝜃: the Gaussian mean and covariance are analytic functions of the natural parameters, while marginalization and conditioning involve only block extraction and analytic operations. By the closure result in Appendix B.1, every formula satisfying our grammar therefore yields a Gaussian density whose mean and covariance are obtained from those of the base terms through finitely many operations that preserve analyticity. Since a Gaussian density is obtained from its mean and covariance through compositions of real-analytic functions, it is analytic in these parameters; therefore, every admissible formula satisfies Assumption 4.7.
10
Proposition 4.8 (Generic failure of non-identifying formulas). Define the set of parameters for which the target interventional density agrees with the observational formula for all t ∈ XT as 𝑆 := {𝜃 ∈ Θ : for all t ∈ XT , ⟦𝜙⟧( 𝑝 𝜃 ,O , t) = 𝑝 𝜃 ,Y|do(T=t) 𝜇Y -almost everywhere}. Let 𝐸 be the full-measure set from Assumption 4.7. Under Assumptions 4.4–4.7, if there exists 𝜃 ∗ ∈ Θ and t∗ ∈ XT such that 𝜇Y ({y ∈ 𝐸 : ⟦𝜙⟧( 𝑝 𝜃 ∗ ,O , t∗ ) (y) ≠ 𝑝 𝜃 ∗ ,Y|do(T=t∗ ) (y)}) > 0, then 𝑆 has Lebesgue measure zero. We prove the result in Appendix E.2 by establishing analyticity of the interventional density, and combining it with the analyticity of the candidate formula ensured by our grammar. Their difference is therefore analytic, and the measure-zero conclusion follows from the identity theorem (Mityagin, 2020) for real-analytic functions: the zero set of a non-zero analytic function on an open connected domain has Lebesgue measure zero. The falsifier therefore never rejects an identifying formula and, for a non-identifying formula, returns a counterexample with probability one relative to the chosen parametric family. Combining these properties with the soundness and completeness of the ID algorithm yields the following result, proved in Appendix E.3. Theorem 4.9 (Almost-surely correct verifier). For conditional exponential-family parametrizations, under Assumptions 4.4–4.7, the falsifier in Definition 4.1 induces an almost-surely correct verifier relative to PΘ (XV ). In light of Theorem 4.9, 𝐾 = 1 in Definition 4.1 suffices for almost-sure correctness relative to PΘ (XV ) under exact evaluation and absolutely continuous parameter sampling. These conditions are not met by pseudo-random floating-point implementations, and comparisons up to a fixed tolerance do not inherit the same guarantee (see Appendix G for an example). In the linear Gaussian case, however, Equation (1) is a rational function of the mean and covariance parameters; after clearing denominators, verification therefore reduces to polynomial identity testing, which is decidable by exact symbolic procedures (Shpilka and Yehudayoff, 2010, Chapter 4). Since symbolic procedures are often computationally expensive, and efficient deterministic procedures are not available in general, falsification remains justified as a practical randomized procedure: we sample parameters from a large finite integer set and evaluate the polynomial using exact arithmetic. This addresses the gap between the idealized assumptions and actual computational implementation: it removes floating-point error and the polynomial identity testing bound controls the finite-sampling probability of falsely accepting a non-identifying formula. See Appendix G for details.
5 Verification for front-door gateways Í fd := {𝜙Zfd := z 𝑝(z | Consider identification relative to the class of front-door formulas ΦY,T Í t) t′ 𝑝(y | t′ , z) 𝑝(t′ ) : Z ⊆ O \ (T ∪ Y)}. The front-door criterion (Pearl, 1995a, Section 3.2) gives graphical conditions on a candidate set Z sufficient for the corresponding front-door formula to be identifying for Y | do(T) (see Appendix H). These conditions have been described as overly restrictive (Pearl, 2009, Section 3.3.2). Indeed, the front-door criterion is sound but not exhaustively fd : there exist sets Z for which 𝜙fd is identifying for Y | do(T) even though Z complete relative to ΦY,T Z does not satisfy the criterion. Consider for instance Figure 2, which shows an acyclic directed mixed graph with unobserved confounding between 𝑇 and 𝑌 . Here, neither {𝑀, 𝐴} nor {𝑀, 𝐶} satisfies the 11
𝐴
𝑇
𝑀
𝑌
𝐶
𝐵
Figure 2: Acyclic directed mixed graph with unobserved confounding between 𝑇 and 𝑌 . Although {𝑀, 𝐴} and {𝑀, 𝐶} do not satisfy the front-door criterion, the front-door adjustment formula can still be certified as identifying. Example based on Wienöbst et al. (2024, Figure 1). front-door criterion, since there is a back-door path from these sets to 𝑌 through 𝐵 that is not blocked by 𝑇. Nevertheless, our falsifier certifies the front-door formula for either set as identifying relative to the parametric submodel it considers. In this example, we can in fact prove that the formulas are identifying in the full non-parametric model; see Appendix H.1. A successful do-calculus derivation would also certify such formulas, but derivation search is not a general halting verifier of candidate formulas (Theorem 3.4). Therefore, the front-door criterion is not exhaustively complete relative to fd : it can fail to certify front-door formulas that are identifying nonetheless. ΦY,T Verification allows us to develop the gateway test, a procedure that is sound and exhaustively fd . The gateway test enumerates all candidate sets Z ⊆ O \ (T ∪ Y), constructs complete relative to ΦY,T fd , and applies the verifier to it. A candidate set Z the corresponding front-door formula 𝜙Zfd ∈ ΦY,T passes the test if and only if 𝜙Zfd is verified as identifying. Thus, with an exact verifier, the gateway test returns exactly those candidate sets whose front-door formulas are identifying. In practice, if one uses the falsifier from Section 4, the procedure is almost-surely sound and exhaustively complete fd for the conditional exponential family chosen in the falsification routine. The same relative to ΦY,T idea applies to any finite class of candidate formulas. When a formula class is indexed by candidate sets, a graphical criterion can replace the verifier in the inner loop, but only if it is exhaustively complete relative to that class (see Appendix I): for each candidate set, it must decide whether the associated formula is identifying, rather than merely guarantee that some valid set is found whenever one exists (the latter suffices for completeness for identification).
6 Discussion and outlook Our strategy to verification restricts the model class, which makes verification decidable and tractable. However, restricting the model class is not a general solution, since other parametric families can involve non-algebraic expressions leading to an undecidable decision problem (Richardson, 1968). The falsification strategy comes with guarantees that are relative to the parametric submodel PΘ (XV ) used by the falsifier (Theorem 4.9): if a candidate formula is certified by the falsifier, it is identifying relative to PΘ (XV ) almost surely, but it need not be valid in the full non-parametric graphical model PG (XV ). Characterizing when correctness relative to PΘ (XV ) transfers to correctness in PG (XV ) remains open. Possible directions include using increasingly rich parametric families or relaxing Definition 2.1 to focus on mean effects rather than interventional distributions. Finally, verification can be extended beyond unconditional interventional targets by allowing both sides of Equation (1) to be functionals in observational and interventional densities, including (in)equality constraints implied by the graph (Sachs et al., 2026), as well as beyond our formula
12
grammar in Definition 2.1, for example, to include formulas in linear instrumental-variable models identifying mean effects instead of full interventional distributions.
References E. Bareinboim and J. Pearl. Causal inference by surrogate experiments: z-identifiability. In Proceedings of the Twenty-Eighth Conference on Uncertainty in Artificial Intelligence, page 113–120. AUAI Press, 2012. (Cited on page 1.) O. Barndorff-Nielsen. Information and Exponential Families: In Statistical Theory. John Wiley & Sons, 2014. (Cited on pages 10, 27, and 28.) P. Boeken, P. Forré, and J. M. Mooij. Are Bayesian networks typically faithful? arXiv preprint arXiv: 2410.16004, 2026. (Cited on pages 10, 24, and 26.) L. Chen and J. M. Mooij. Complete Causal Identification from Ancestral Graphs under Selection Bias. arXiv preprint arXiv: 2603.26301, 2026. (Cited on page 1.) J. B. Conway. Functions of One Complex Variable I. Springer New York, 2nd edition, 1978. (Cited on page 24.)
J. Correa and E. Bareinboim. A Calculus for Stochastic Interventions: Causal Effect Identification and Surrogate Experiments. Proceedings of the AAAI Conference on Artificial Intelligence, 34(06): 10093–10100, 2020. (Cited on page 1.) L. de Moura and S. Ullrich. The Lean 4 Theorem Prover and Programming Language. In Automated Deduction – CADE 28, volume 12699, pages 625–635. Springer, 2021. (Cited on page 1.) R. A. DeMillo and R. J. Lipton. A probabilistic remark on algebraic program testing. Information Processing Letters, 7(4):193–195, 1978. (Cited on page 35.) M. Drton, R. Foygel, and S. Sullivant. Global identifiability of linear structural equation models. The Annals of Statistics, 39(2):865 – 886, 2011. (Cited on page 33.) R. J. Evans. Margins of discrete Bayesian networks. The Annals of Statistics, 46(6A):2623 – 2656, 2018. (Cited on page 33.) F. R. Guo, E. Perković, and A. Rotnitzky. Variable elimination, graph reduction and the efficient g-formula. Biometrika, 110(3):739–761, 2023. (Cited on page 1.) L. Henckel, E. Perković, and M. H. Maathuis. Graphical Criteria for Efficient Total Effect Estimation Via Adjustment in Causal Linear Models. Journal of the Royal Statistical Society Series B: Statistical Methodology, 84(2):579–599, 2022. (Cited on page 1.) L. Henckel, M. Buttenschoen, and M. H. Maathuis. Graphical tools for selecting conditional instrumental sets. Biometrika, 111(3):771–788, 2023. (Cited on page 1.) L. Henckel, T. Würtzen, and S. Weichwald. Adjustment Identification Distance: A gadjid for Causal Structure Learning. In Proceedings of the Fortieth Conference on Uncertainty in Artificial Intelligence, 2024. (Cited on page 2.) 13
Y. Huang and M. Valtorta. Identifiability in causal Bayesian networks: a sound and complete algorithm. In Proceedings of the 21st National Conference on Artificial Intelligence - Volume 2, page 1149–1154, 2006. (Cited on pages 1 and 5.) D. Ibeling, T. Icard, and M. Mossé. On probabilistic and causal reasoning with summation operators. Journal of Logic and Computation, 35(8):exae068, 2025. (Cited on page 7.) A. Jaber, A. Ribeiro, J. Zhang, and E. Bareinboim. Causal Identification under Markov equivalence: Calculus, Algorithm, and Completeness. In Advances in Neural Information Processing Systems, volume 35, pages 3679–3690, 2022. (Cited on page 1.) M. H. Maathuis and D. Colombo. A generalized back-door criterion. The Annals of Statistics, 43(3): 1060–1088, 2015. (Cited on page 1.) B. S. Mityagin. The Zero Set of a Real Analytic Function. Mathematical Notes, 107(3):529–530, 2020. (Cited on pages 11 and 25.) J. Pearl. Causal Diagrams for Empirical Research. Biometrika, 82(4):669–688, 1995a. (Cited on pages 1, 5, 11, 22, and 38.)
J. Pearl. On the testability of causal models with latent and instrumental variables. In Proceedings of the Eleventh Conference on Uncertainty in Artificial Intelligence, page 435–443. Morgan Kaufmann Publishers Inc., 1995b. (Cited on page 33.) J. Pearl. Causality: Models, Reasoning, and Inference. Cambridge University Press, 2nd edition, 2009. (Cited on pages 1, 11, 18, 26, and 39.) E. Perković, J. Textor, M. Kalisch, and M. H. Maathuis. Complete Graphical Characterization and Construction of Adjustment Sets in Markov Equivalence Classes of Ancestral Graphs. Journal of Machine Learning Research, 18(220):1–62, 2018. (Cited on pages 1 and 22.) J. Peters, D. Janzing, and B. Schölkopf. Elements of Causal Inference: Foundations and Learning Algorithms. The MIT Press, 2017. (Cited on page 18.) D. Richardson. Some Undecidable Problems Involving Elementary Functions of a Real Variable. The Journal of Symbolic Logic, 33(4):514–520, 1968. (Cited on page 12.) T. Richardson. Markov Properties for Acyclic Directed Mixed Graphs. Scandinavian Journal of Statistics, 30(1):145–157, 2003. (Cited on pages 2 and 18.) T. Richardson and P. Spirtes. Ancestral graph Markov models. The Annals of Statistics, 30(4):962 – 1030, 2002. (Cited on page 22.) T. S. Richardson, R. J. Evans, J. M. Robins, and I. Shpitser. Nested Markov properties for acyclic directed mixed graphs. The Annals of Statistics, 51(1):334 – 361, 2023. (Cited on pages 3, 18, 21, and 34.)
J. Robins. A new approach to causal inference in mortality studies with a sustained exposure period—application to control of the healthy worker survivor effect. Mathematical Modelling, 7 (9):1393–1512, 1986. (Cited on page 19.) 14
A. Rotnitzky and E. Smucler. Efficient Adjustment Sets for Population Average Causal Treatment Effect Estimation in Graphical Models. Journal of Machine Learning Research, 21(188):1–86, 2020. (Cited on page 1.) M. C. Sachs, E. E. Gabriel, R. J. Evans, and A. Sjölander. Deriving Complete Constraints in Hidden Variable Models. arXiv preprint arXiv: 2601.11242, 2026. (Cited on page 12.) J. T. Schwartz. Fast Probabilistic Algorithms for Verification of Polynomial Identities. Journal of the ACM, 27(4):701–717, 1980. (Cited on page 35.) A. Shpilka and A. Yehudayoff. Arithmetic Circuits: A survey of recent results and open questions. Foundations and Trends in Theoretical Computer Science, 5(3–4):207–388, 2010. (Cited on pages 11 and 35.)
I. Shpitser and J. Pearl. Identification of joint interventional distributions in recursive semi-markovian causal models. In Proceedings of the 21st National Conference on Artificial Intelligence - Volume 2, page 1219–1226. AAAI Press, 2006. (Cited on pages 2, 4, 5, 8, and 23.) I. Shpitser and J. Pearl. Complete Identification Methods for the Causal Hierarchy. Journal of Machine Learning Research, 9(64):1941–1979, 2008. (Cited on page 1.) I. Shpitser, T. VanderWeele, and J. M. Robins. On the validity of covariate adjustment for estimating causal effects. In Proceedings of the Twenty-Sixth Conference on Uncertainty in Artificial Intelligence, page 527–536, 2010. (Cited on pages 1 and 22.) I. Shpitser, R. J. Evans, T. S. Richardson, and J. M. Robins. Introduction to Nested Markov Models. Behaviormetrika, 41(1):3–39, 2014. (Cited on page 33.) I. Shpitser, R. Evans, and T. Richardson. Acyclic linear SEMs obey the Nested Markov property. In Proceedings of the Thirty-Fourth Conference on Uncertainty in Artificial Intelligence, pages 735–745, 2018. (Cited on page 33.) P. Spirtes, C. Glymour, and R. Scheines. Causation, Prediction, and Search. The MIT Press, 2000. (Cited on pages 19 and 33.)
J. Tian and J. Pearl. A general identification condition for causal effects. In Eighteenth National Conference on Artificial Intelligence, page 567–573. American Association for Artificial Intelligence, 2002. (Cited on page 1.) T. Verma and J. Pearl. Equivalence and synthesis of causal models. In Proceedings of the Sixth Annual Conference on Uncertainty in Artificial Intelligence, page 255–270, 1990. (Cited on pages 2, 18, and 33.)
M. Wienöbst, B. van der Zander, and M. Liśkiewicz. Linear-time algorithms for front-door adjustment in causal graphs. In Proceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence and Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence and Fourteenth Symposium on Educational Advances in Artificial Intelligence. AAAI Press, 2024. (Cited on page 12.)
15
J. Witte, L. Henckel, M. H. Maathuis, and V. Didelez. On Efficient Adjustment in Causal Graphs. Journal of Machine Learning Research, 21(246):1–45, 2020. (Cited on page 1.) C. Yvernes, E. Devijver, M. Clausel, and E. Gaussier. Unveiling the Structure of Do-Calculus Reasoning via Derivation Graphs. arXiv preprint arXiv: 2606.03719, 2026. (Cited on page 4.) R. Zippel. Probabilistic Algorithms for Sparse Polynomials. In Proceedings of the International Symposiumon on Symbolic and Algebraic Computation, pages 216–226. Springer, 1979. (Cited on page 35.)
16
Contents of the Appendix A Preliminaries
17
B A typed, kernel-preserving grammar for observational formulas
19
C Verifying adjustment formulas with graphical criteria
22
D Do-calculus
22
E Proofs
23
F Alternative implementation via the nested Markov model
33
G Numerical evaluation and exact arithmetic
34
H The front-door criterion
38
I
40
Recovering all identifying formulas in a finite class
Appendix A. Preliminaries A.1 Graphical preliminaries A graph G = (V, E) consists of a finite non-empty node set V, whose nodes represent random variables, and an edge set E. Nodes joined by an edge are called adjacent, and an edge joining two nodes is incident to those nodes. If the edge set contains only ordered pairs of distinct vertices, that is, if E ⊆ {(𝑉𝑖 , 𝑉𝑗 ) ∈ V × V : 𝑉𝑖 ≠ 𝑉𝑗 }, then G is a directed graph; for (𝑉𝑖 , 𝑉𝑗 ) ∈ E, we write 𝑉𝑖 → 𝑉𝑗 . Directed graphs contain at most one edge between any pair of distinct nodes. A directed mixed graph may instead contain two types of edges: directed (→) and bidirected (↔), with at most one edge of each type between any pair of distinct nodes. A walk 𝑤 in G is a sequence of nodes 𝑉1 , . . . , 𝑉𝑗 ∈ V and a corresponding sequence of edges 𝑒 1 , . . . , 𝑒𝑗 −1 such that, for all 𝑖 ∈ {1, . . . , 𝑗 − 1}, 𝑒 𝑖 is an edge between 𝑉𝑖 and 𝑉𝑖+1 . The first node 𝑉1 and the last node 𝑉𝑗 are called the endpoints of 𝑤. A path is a walk whose nodes are distinct. A walk, or path, from a set X ⊆ V to a disjoint set Y ⊆ V is a walk, or path, from some 𝑋 ∈ X to some 𝑌 ∈ Y. Such a walk, or path, is proper if only its first node belongs to X. A back-door path from a set X ⊆ V to a disjoint set Y ⊆ V is a proper path whose first edge has an arrowhead into a node in X. A directed walk, or path, from 𝑉1 to 𝑉𝑗 is a walk, or path, whose edges are all directed and point from 𝑉1 towards 𝑉𝑗 . A directed cycle is a directed walk 𝑉1 , . . . , 𝑉𝑗 , 𝑉1 with 𝑉1 , . . . , 𝑉𝑗 distinct. A directed graph without directed cycles is a directed acyclic graph, whereas a directed mixed graph without directed cycles is an acyclic directed mixed graph. If 𝑉𝑖 → 𝑉𝑗 , then 𝑉𝑖 is a parent of 𝑉𝑗 . For all 𝑉 ∈ V, we write pa(𝑉) for the set of parents of 𝑉 in G. In the latent-variable setting, we write V = O ⊔ L, where O and L denote the observed and latent variables, respectively. We represent a latent-variable directed acyclic graph G by an acyclic directed
17
mixed graph G 𝑝 obtained via latent projection (Verma and Pearl, 1990; Richardson, 2003), defined as follows. Definition A.1 (Richardson et al., 2023, Definition A.2). Let G be a latent-variable directed acyclic graph with node set V = O ⊔ L, where nodes in O are observed and nodes in L are unobserved. The latent projection of G onto O is an acyclic directed mixed graph G 𝑝 where, for all distinct 𝑂 𝑖 , 𝑂 𝑗 ∈ O: (i) G 𝑝 contains a directed edge 𝑂 𝑖 → 𝑂 𝑗 if G has a directed path from 𝑂 𝑖 to 𝑂 𝑗 whose non-endpoint nodes, if any, all belong to L. (ii) G 𝑝 contains a bidirected edge 𝑂 𝑖 ↔ 𝑂 𝑗 if G has a path between 𝑂 𝑖 and 𝑂 𝑗 such that 𝑂 𝑖 ← 𝐿 1 ← · · · ← 𝐿 ℎ → · · · → 𝐿 𝑚 → 𝑂 𝑗 , with 𝐿 𝑘 ∈ L for all 𝑘 ∈ {1, . . . , 𝑚}. Given a directed acyclic graph G over nodes V, let 𝑤 be a walk with node sequence 𝑉1 , . . . , 𝑉𝑗 ∈ V. A non-endpoint node 𝑉𝑖 , with 𝑖 ∈ {2, . . . , 𝑗 − 1}, is a collider on 𝑤 if the two edges on 𝑤 incident to 𝑉𝑖 both have arrowheads into 𝑉𝑖 , that is, if 𝑤 contains the subwalk 𝑉𝑖−1 → 𝑉𝑖 ← 𝑉𝑖+1 . A non-endpoint node on 𝑤 that is not a collider is called a non-collider. These notions lead to the definition of 𝑑-separation. Definition A.2 (𝒅-connection and separation). Given a directed acyclic graph G over nodes V, a walk 𝑤 in G is open given a set S ⊆ V \ {𝑉1 , 𝑉𝑚 } if 1. every collider on 𝑤 belongs to S; and 2. every non-collider on 𝑤 does not belong to S. A walk that is not open given S is blocked given S. For all disjoint subsets A, B, S ⊆ V, we say that A and B are 𝑑-connected by S if there exist 𝐴 ∈ A, 𝐵 ∈ B, and an open walk from 𝐴 to 𝐵 given S. Otherwise, A and B are 𝑑-separated by S. This definition of 𝑑-separation is equivalent to the path-based definition, such as those of Pearl (2009, Definition 1.2.3) and Peters et al. (2017, Definition 6.1). A.2 Causal preliminaries Consider a latent-variable directed acyclic graph G over V = O ⊔ L and suppose that all directed edges in G represent causal relationships. Under this interpretation, for all 𝑉1 , 𝑉2 ∈ V, a directed edge 𝑉1 → 𝑉2 indicates that 𝑉1 is a direct cause of of 𝑉2 ; a directed path 𝑉1 → · · · → 𝑉2 indicates that 𝑉1 is a cause of 𝑉2 ; and a bidirected edge 𝑉1 ↔ 𝑉2 indicates that 𝑉1 and 𝑉2 share an unobserved common cause. For all 𝑉 ∈ V, let X𝑉 be the sample space of 𝑉, and let 𝜇𝑉 be a 𝜎-finite measure on X𝑉 . Throughout, we consider densities in PG (XV ), that is, densities that factorize according to G (see Section 2). Every 𝑞 ∈ PG (XV ) satisfies the global Markov property with respect to G: for all disjoint A, B, S ⊆ V, if A and B are 𝑑-separated by S in G, then A and B are conditionally independent given S under 𝑞. Consider the intervention node set T ⊆ O, and intervention values t ∈ XT . Under the intervention do(T = t) (or shorthand do(t)), the variables in T are set to t. Let X := O \ T. The resulting interventional density is given by the truncated factorization formula (Pearl, 2009, Section 1.3)
18
(interventions may change the reference measure; we nevertheless adopt the standard notation for simplicity): ∫ 𝑝X|do(T=t) (x) = 𝑝(x, ℓ) d𝜇L (ℓ), XL
where 𝑝(x, ℓ) =
Ö
𝑝(𝑣 | vpa(𝑉 ) ) T=t ,
𝑉 ∈V\T
that is, the conditional densities corresponding to the intervened variables are removed from the factorization and the remaining factors are evaluated after substituting T = t. The above expression, also known as the g-formula (Robins, 1986), or the manipulated density (Spirtes et al., 2000), uses the factorization over the full latent-variable causal directed acyclic graph; as only the observational marginal 𝑝O is observed, the resulting interventional density need not be identifiable from it. Identification concerns precisely when the interventional can nevertheless be expressed as a functional of 𝑝O satisfying constraints encoded by the latent projection G 𝑝 (see Section 2).
Appendix B. A typed, kernel-preserving grammar for observational formulas We introduce a well-defined grammar for observational formulas, designed to generate expressions that denote probability kernels rather than arbitrary algebraic combinations of densities. For disjoint sets A, B ⊆ O, write 𝐸 :A|B to mean that the expression 𝐸 denotes a conditional density over A given B, or equivalently a density representation of a Markov kernel from XB to XA . This notation is a typing device: it records the output variables of an expression and its conditioning arguments. Base terms. base terms:
For disjoint sets A, B ⊆ O, observational marginals and conditionals are admissible 𝑝(a) : A | ∅,
𝑝(a | b) : A | B.
where 𝑝(a | b) is understood only on the part of XB on which 𝑝(b) > 0. Although marginals and conditionals, where defined, can be derived from the observed joint by the rules below, we take them as base terms to match the usual notation for identifying formulas. Quotient notation such as 𝑝(a, b)/𝑝(b) is understood only as shorthand for the corresponding conditional density, not as an arbitrary division operation. Well-formed products. Products are admissible only when they can be interpreted as sequential compositions of kernels. Each factor must then introduce a new set of output variables, so that every output variable is assigned exactly to one factor. Moreover, every conditioning variable must already be available when the factor is evaluated: it must either be conditioned on by the product as a whole, or have been introduced by an earlier factor. More formally, let A1 , . . . , A 𝑘 , C ⊆ O, where A1 , . . . , A 𝑘 are pairwise disjoint and disjoint from C. Suppose the factors can be ordered so that, for all 𝑖 ∈ {1, . . . , 𝑘 }, 𝐸 𝑖 : A𝑖 | D𝑖 ,
D𝑖 ⊆ C ∪ A1 ∪ · · · ∪ A𝑖−1 . 19
A factor need not depend on all variables that are already available; the requirement is only that it does not condition on variables that have not yet been introduced. Then, the product of the factors is ! 𝑘 𝑘 Ö Ä 𝐸𝑖 : A𝑖 | C. 𝑖=1
𝑖=1
Thus, the product denotes a kernel over all variables introduced by the factors, conditional on C. This rule includes ordinary chain-rule products and more general chain-like constructions. For example, 𝑝(𝑥) 𝑝(𝑦 | 𝑡, 𝑥) is admissible as a kernel over (𝑋, 𝑌 ) conditional on 𝑇: the first factor introduces 𝑋, and the second factor introduces 𝑌 while conditioning only on 𝑇 and the already introduced variable 𝑋. The rule also allows products such as 𝑝(𝑥) 𝑝(𝑦), which denotes a density over (𝑋, 𝑌 ), although not necessarily the observational joint 𝑝(𝑥, 𝑦). By contrast, products such as 𝑝(𝑦) 𝑝(𝑦) are not admissible, since the same output variable is introduced twice. Similarly, products such as 𝑝(𝑎 | 𝑏) 𝑝(𝑏 | 𝑎) are not admissible either, since no ordering makes the conditioning variables available before the corresponding outputs are introduced. Marginalization. Marginalization is admissible when it removes output variables from a well-typed kernel. If an expression denotes a joint kernel over disjoint sets of variables A and B conditional on C, that is, 𝐸 : A, B | C, then, integrating out B leaves a kernel over A, conditional on the same variables C: ∑︁ 𝐸 (a, b | c) : A | C. b
Internal conditional division. The grammar allows variables to be moved from the output side of an intermediate kernel to its conditioning side. For pairwise disjoint sets A, B, R ⊆ O, if 𝐸 : A, R | B, then, for every fixed b, 𝐸 (a, r | b) denotes a joint density over (A, R). Let M ⊆ A. From the same kernel 𝐸, form the conditional kernel of R given (M, B), denoted by 𝐸 (r | m, b). Where this conditional is defined, the grammar admits 𝐸 (a, r | b) : A | B, R. 𝐸 (r | m, b) Thus, internal conditional division turns a kernel over (A, R) given B into a kernel over A given (B, R). Ordinary conditioning of an intermediate kernel is the special case with M = ∅. The denominator must be derived from the same kernel 𝐸 as the numerator. A quotient with the same formal variables but with an independently supplied denominator is not generally kernelpreserving. This is why the rule is an internal conditional division, rather than an arbitrary algebraic quotient. Quotients are admissible only when they are parsed as conditionals or as internal conditional divisions, where kernel preservation follows from typing rule. To see why this rule preserves kernel normalization, write U = A \ M such that A = (U, M) and recall that 𝐸 (a, r | b) is, for each fixed b, a joint density over (A, R). For every b, by the product rule, 𝐸 (u, m, r | b) = 𝐸 (u | m, r, b)𝐸 (r | m, b)𝐸 (m | b). 20
After division by the internally derived conditional 𝐸 (r | m, b), the resulting expression is 𝐸 (u | m, r, b)𝐸 (m | b), which, for every (r, b), integrates to one over (U, M) = A. Internal conditional division is purely a typing rule: it is stated in terms of kernels and does not refer to a graph. Graphical fixability is different: it is a graph-based condition used to determine when a corresponding fixing operation is valid (Richardson et al., 2023). When such a fixing operation is written at the level of kernels, its division step is an instance of the internal conditional division rule above: the denominator is a conditional kernel derived from the same intermediate kernel as the numerator. Thus, the expressions at the kernel level obtained from fixing notation are covered by the grammar after expansion, while fixability itself is not an additional typing rule. Admissible formulas. An observational formula 𝜙 for Y under intervention on T is an expression generated recursively by the preceding rules, with no free variables other than y and t, and of type Y | T, which induces the partial functional ⟦𝜙⟧ : P (XO ) × XT ⇀ P (XY ). This formalizes a convention often left implicit in identification formulas: products of density terms must be well-formed products, sums or integrals must marginalize variables from a well-typed kernel, and quotients must be conditionals or internal conditional divisions rather than arbitrary Í algebraic ratios. For example, 𝑐 𝑝(𝑦 | 𝑡, 𝑐) 𝑝(𝑐) is admissible and has type 𝑌 | 𝑇, whereas 𝑝(𝑦) 𝑝(𝑦) is not admissible merely as an algebraic product of density symbols. B.1 Gaussian closure In the Gaussian case, we restrict attention to non-degenerate Gaussian kernels, that is, Gaussian kernels with strictly positive-definite covariance matrices. Marginalizations and well-formed products preserve non-degeneracy, which ensures that all conditionals and internal conditional divisions are defined everywhere. Suppose the observational law over O is multivariate Gaussian, O ∼ N (𝜇, Σ), with Σ ≻ 0. Then every admissible observational formula 𝜙 of type Y | T denotes, for all t ∈ XT , a linear Gaussian density over Y: wherever ⟦𝜙⟧( 𝑝O , t) is defined, there exist 𝑎 𝜙 ∈ R |Y| , 𝐵𝜙 ∈ R |Y| × |T| , Ω𝜙 ∈ R |Y| × |Y| , depending on 𝑝 and 𝜙 but not on the intervention value t, such that ⟦𝜙⟧( 𝑝O , t) (y) = N y; 𝑎 𝜙 + 𝐵𝜙 t, Ω𝜙 . Thus, the mean parameter is affine in t, while the covariance parameter is independent of t. The claim follows by induction over the grammar: Gaussian marginals and conditionals are linear Gaussian kernels; well-formed products of compatible linear Gaussian kernels define joint linear Gaussian kernels; marginalizing a proper Gaussian kernel again yields a Gaussian kernel over the remaining variables; and internal conditional division preserves linear Gaussianity because the denominator is the conditional kernel computed from the same joint Gaussian kernel as the numerator, and the quotient is therefore another conditional Gaussian kernel of that joint law. Hence, every admissible formula remains linear Gaussian.
21
Appendix C. Verifying adjustment formulas with graphical criteria Instead of asking whether the target interventional density is identifiable (by any observational formula), one may ask whether it is identifiable by some member of a restricted class of formulas. Consider the class of adjustment formulas ( ) ∑︁ adj adj ΦY,T := 𝜙Z := 𝑝(y | t, z) 𝑝(z) : Z ⊆ O \ (T ∪ Y) . (C.2) z
Covariate adjustment asks whether there exists a set Z yielding an identifying formula for Y | do(T), and graphical criteria for adjustment are conditions on candidate sets Z that certify when the adj corresponding adjustment formula 𝜙Z is identifying for Y | do(T). Different criteria give different guarantees. The back-door criterion (Pearl, 1995a, Section 3.1), for instance, is sound but not adj exhaustively complete relative to ΦY,T . The adjustment criterion (Shpitser et al., 2010, Definition 5) adj
is instead sound and exhaustively complete relative to ΦY,T . Both criteria are formulated for directed acyclic graphs, while others extend adjustment to richer graph classes. In particular, the generalized adjustment criterion (Perković et al., 2018, Definition 4) is sound and exhaustively complete relative adj to ΦY,T in directed acyclic graphs, maximal ancestral graphs (Richardson and Spirtes, 2002), and their respective equivalence classes, thus allowing for the presence of unobserved variables. These criteria do not, however, apply to acyclic directed mixed graphs. In graph classes for which a sound and exhaustively complete graphical adjustment criterion is available, checking whether a candidate set Z satisfies the criterion is equivalent to verifying whether adj the corresponding adjustment formula 𝜙Z is identifying for Y | do(T). Such criteria can therefore be viewed as non-parametric graphical shortcuts to verification, but only in the graph class for which the criteria are valid. When no such shortcuts are available, verifiers still apply. For instance, even though no sound and exhaustively complete adjustment criterion is adj currently known for acyclic directed mixed graphs, one can still enumerate the finite class ΦY,T and verify each candidate adjustment formula directly (see Appendix I). Moreover, adjustment criteria can be repurposed as verifiers only for formulas in the restricted adj class ΦY,T . When no candidate adjustment set satisfies a sound and exhaustively complete graphical criterion for the relevant graph class, the target is not identifiable by any adjustment formula in adj ΦY,T , but it may still be identifiable. In fully observed directed acyclic graphs, this distinction is less visible for single-node interventions, since adjustment suffices to determine identifiability in that special case. Beyond this setting, however, the target need not be identifiable by adjustment formulas, but it may still be identifiable by other formulas in ΦY,T , such as front-door formulas (Pearl, 1995a, Section 3.2; see also Section 5 and Appendix H), or by formulas returned by more general identification procedures, such as the ID algorithm. These more general routes rely on do-calculus (Pearl, 1995a, Section 4; see also Appendix D), but, as discussed in Section 3.1, proof search with do-calculus does not by itself yield a verifier for arbitrary formulas in ΦY,T . Verifiers are therefore needed to check formulas that fall outside the scope of adjustment criteria.
Appendix D. Do-calculus The interventional density can sometimes be identified even when no set yields an identifying adjustment or front-door formula. Pearl (1995a, Section 4) introduced a collection of three rules,
22
known as do-calculus, that can be applied sequentially to rewrite interventional quantities and may eventually lead to an expression in observational quantities alone. Let G denote the underlying latent-variable directed acyclic graph over observed nodes O, and consider disjoint node sets Y, T, Z, W ⊆ O. Do-calculus consists of the following rules: (i) “Insertion/deletion of observations”: 𝑝(y | do(t), z, w) = 𝑝(y | do(t), w), if Y and Z are 𝑑-separated by T, W in the graph obtained by removing incoming edges into T; (ii) “Action/observation exchange”: 𝑝(y | do(t, z), w) = 𝑝(y | do(t), z, w), if Y and Z are 𝑑-separated by T, W in the graph obtained by removing incoming edges into T and outgoing edges from Z; (iii) “Insertion/deletion of actions”: 𝑝(y | do(t, z), w) = 𝑝(y | do(t), w), if Y and Z are 𝑑-separated by T, W in the graph obtained as follows: first remove all incoming edges into nodes in T; then, in the resulting graph, identify those nodes of Z that are not ancestors of any node in W; finally, remove all incoming edges into these nodes of Z. These rules have been shown to be complete for identification (Shpitser and Pearl, 2006). For instance, do-calculus can be used to derive the front-door formula in (H.9). The ID algorithm (Shpitser and Pearl, 2006) allows one to derive one identifying formula, if one exists. However, as we discuss in Section 3, finding one formula with one derivation for it is not enough to determine for any proposed formula whether it can be derived using do-calculus.
Appendix E. Proofs E.1 Proof of Theorem 3.4 Theorem 3.4 (Semi-decidability of derivation search). I do-calc (G 𝑝 , Y, T) is semi-decidable. Proof. Showing that I do-calc (G 𝑝 , Y, T) is semi-decidable is equivalent to showing that there exists an algorithm 𝑀 that semi-decides I do-calc (G 𝑝 , Y, T), that is, an 𝑀 that halts and accepts for all inputs that are elements of I do-calc (G 𝑝 , Y, T), but need not terminate otherwise. The key point is to enumerate derivations fairly. Indeed, for a fixed derivation length, there may be infinitely many derivations, so an enumeration that first exhausts all candidates of length 1, then all candidates of length 2, and so on, may never reach longer derivations. Instead, we enumerate pairs (𝑚, 𝑖) ∈ N × N, where 𝑚 is the derivation length and 𝑖 is the index within the enumeration of candidates of that length; this ensures that 𝑀 can visit all derivations. For all 𝑚 ∈ N, fix a computable enumeration 𝑒 𝑚 : N → 𝐷 𝑚 of 𝐷 𝑚 , the set of derivations of length 𝑚. Such an enumeration exists because each derivation has a finite encoding over Σ. Let 𝑓 : N → N × N be a computable bijection that maps 𝑛 ∈ N to a tuple (𝑚, 𝑖) ∈ N × N. The algorithm 23
𝑀 proceeds as follows. For 𝑛 = 0, 1, 2, . . . , algorithm 𝑀 computes 𝑓 (𝑛) = (𝑚, 𝑖), sets the derivation 𝑑 𝑚,𝑖 = 𝑒 𝑚 (𝑖), and then runs Check(G 𝑝 , 𝑄Y,T , 𝜙, 𝑑 𝑚,𝑖 ) to check whether 𝑑 𝑚,𝑖 is a valid derivation relative to G 𝑝 that derives 𝜙 from 𝑄Y,T . Check halts for all inputs because it performs finitely many operations on finite strings and evaluates only decidable graphical side-conditions (such as d-separation) on a finite graph. If 𝜙 ∈ I do-calc (G 𝑝 , Y, T), then by definition there exists at least one derivation 𝑑 ∗ such that Check(G 𝑝 , 𝑄Y,T , 𝜙, 𝑑 ∗ ) = true. Therefore, there exists 𝑛∗ ∈ N such that 𝑓 (𝑛∗ ) = (𝑚 ∗ , 𝑖 ∗ ) and 𝑑 𝑚∗ ,𝑖∗ = 𝑒 𝑚∗ (𝑖 ∗ ) = 𝑑 ∗ . When 𝑀 reaches 𝑛∗ , it runs Check, accepts and halts. If 𝜙 ∉ I do-calc (G 𝑝 , Y, T), there exists no derivation for which Check returns true. In particular, since Check halts on every input, 𝑀 never encounters a derivation accepted by Check and therefore fails to terminate. This shows that I do-calc (G 𝑝 , Y, T) semi-decides L and concludes the proof of Theorem 3.4. E.2 Proof of Proposition 4.8 Proposition 4.8 (Generic failure of non-identifying formulas). Define the set of parameters for which the target interventional density agrees with the observational formula for all t ∈ XT as 𝑆 := {𝜃 ∈ Θ : for all t ∈ XT , ⟦𝜙⟧( 𝑝 𝜃 ,O , t) = 𝑝 𝜃 ,Y|do(T=t) 𝜇Y -almost everywhere}. Let 𝐸 be the full-measure set from Assumption 4.7. Under Assumptions 4.4–4.7, if there exists 𝜃 ∗ ∈ Θ and t∗ ∈ XT such that 𝜇Y ({y ∈ 𝐸 : ⟦𝜙⟧( 𝑝 𝜃 ∗ ,O , t∗ ) (y) ≠ 𝑝 𝜃 ∗ ,Y|do(T=t∗ ) (y)}) > 0, then 𝑆 has Lebesgue measure zero. Proof. We follow the proof strategy used to show that, for exponential-family parametrizations of densities factorizing according to the graph, under regularity assumptions, the set of parameter values for which the distribution is not faithful to the graph has Lebesgue measure zero (Boeken et al., 2026, Theorems 7 and 8). Define the set of parameters for which the target interventional density agrees with the observational formula on 𝐸 for all t ∈ XT as 𝑆 𝐸 := {𝜃 ∈ Θ : for all y ∈ 𝐸 and all t ∈ XT , ⟦𝜙⟧( 𝑝 𝜃 ,O , t) (y) = 𝑝 𝜃 ,Y|do(T=t) (y)}. We divide the proof in three steps: (i) Using Assumptions 4.4 and 4.7, if, for all y ∈ 𝐸 and all t ∈ XT , the real-valued map 𝜃 ↦→ 𝑝 𝜃 ,Y|do(T=t) (y) is analytic on Θ, we show that 𝑆 𝐸 has Lebesgue measure zero; (ii) Using (i), we show that 𝑆 has Lebesgue measure zero; (iii) Using Assumptions 4.4–4.6, we show that, for all y ∈ XY and all t ∈ XT , the real-valued map 𝜃 ↦→ 𝑝 𝜃 ,Y|do(T=t) (y) is analytic on Θ. Throughout, we use that sums, products, quotients with non-zero denominator, and compositions of analytic functions are analytic (see Conway, 1978, Chapter 3.2).
24
Proof of (i).
By the premises, there exists 𝜃 ∗ ∈ Θ, t∗ ∈ XT and y∗ ∈ 𝐸 such that ⟦𝜙⟧( 𝑝 𝜃 ∗ ,O , t∗ ) (y∗ ) ≠ 𝑝 𝜃 ∗ ,Y|do(T=t∗ ) (y∗ ).
Define, for all 𝜃 ∈ Θ, 𝑔t∗ (𝜃) := ⟦𝜙⟧( 𝑝 𝜃 ,O , t∗ ) (y∗ ) − 𝑝 𝜃 ,Y|do(T=t∗ ) (y∗ ). Then 𝑔t∗ (𝜃 ∗ ) ≠ 0 and hence 𝑔t∗ is not identically zero on Θ. By Assumption 4.7, the real-valued map 𝜃 ↦→ ⟦𝜙⟧( 𝑝 𝜃 ,O , t∗ ) (y∗ ) is analytic on Θ. If the real-valued map 𝜃 ↦→ 𝑝 𝜃 ,Y|do(T=t∗ ) (y∗ ) is analytic on Θ, which we show in the proof of (iii), since the difference of analytic functions is analytic, the real-valued map 𝜃 ↦→ 𝑔t∗ (𝜃) is analytic on Θ as well. t∗ ,y∗ t∗ ,y∗ Define 𝑆 𝐸 := {𝜃 ∈ Θ : 𝑔t∗ (𝜃) = 0}. Then, 𝑆 𝐸 ⊆ 𝑆 𝐸 . By the identity theorem (Mityagin, 2020, Proposition 1), the zero set of a real analytic function that is not identically zero on an open and connected domain has Lebesgue measure zero. Since, by Assumption 4.4, for all 𝑉 ∈ V, Θ𝑉 is Î t∗ ,y∗ open and connected, Θ = 𝑉 ∈V Θ𝑉 is open and connected as well. Therefore, 𝑆 𝐸 , and hence 𝑆 𝐸 , has Lebesgue measure zero. This completes the proof of (i). Proof of (ii). Let 𝜃 ∗ ∈ Θ and t∗ ∈ XT be the witnesses from the premise. For all 𝜃 ∈ Θ and y ∈ 𝐸, define 𝑔t∗ (𝜃, y) := ⟦𝜙⟧( 𝑝 𝜃 ,O , t∗ ) (y) − 𝑝 𝜃 ,Y|do(T=t∗ ) (y). Then the premise can be rewritten as 𝜇Y ({y ∈ 𝐸 : 𝑔t∗ (𝜃 ∗ , y) ≠ 0}) > 0. For all y ∈ 𝐸, by Assumption 4.7, and if the real-valued map 𝜃 ↦→ 𝑝 𝜃 ,Y|do(T=t∗ ) (y) is analytic on Θ (shown in the proof of (iii)), the real-valued map 𝜃 ↦→ 𝑔t∗ (𝜃, y) is analytic on Θ. Define 𝑆t∗ := 𝜃 ∈ Θ : ⟦𝜙⟧( 𝑝 𝜃 ,O , t∗ ) (y) = 𝑝 𝜃 ,Y|do(T=t∗ ) (y) 𝜇Y -almost everywhere and, for all 𝜃 ∈ Θ, 𝐷 𝜃 := y ∈ XY : ⟦𝜙⟧( 𝑝 𝜃 ,O , t∗ ) (y) ≠ 𝑝 𝜃 ,Y|do(T=t∗ ) (y) = {y ∈ XY : 𝑔t∗ (𝜃, y) ≠ 0} . By definition, for all 𝜃 ∈ Θ, 𝜃 ∈ 𝑆t∗ if and only if 𝜇Y (𝐷 𝜃 ) = 0. Since 𝐸 has full measure, 𝜇Y (𝐸 𝑐 ) = 0. Moreover, for all 𝜃 ∈ Θ, 𝐷 𝜃 = (𝐷 𝜃 ∩ 𝐸) ∪ (𝐷 𝜃 ∩ 𝐸 𝑐 ), and 𝐷 𝜃 ∩ 𝐸 𝑐 ⊆ 𝐸 𝑐 , which implies that 𝜇Y (𝐷 𝜃 ) = 0 if and only if 𝜇Y (𝐷 𝜃 ∩ 𝐸) = 0. By definition of 𝑔t∗ , 𝐷 𝜃 ∩ 𝐸 = {y ∈ 𝐸 : 𝑔t∗ (𝜃, y) ≠ 0}. Therefore, for all 𝜃 ∈ Θ, 𝜃 ∈ 𝑆t∗
⇐⇒
𝜇Y ({y ∈ 𝐸 : 𝑔t∗ (𝜃, y) ≠ 0}) = 0.
Since 𝑆 requires the 𝜇Y -almost everywhere equality for all t ∈ XT , 𝑆 ⊆ 𝑆t∗ . It is therefore enough to show that 𝑆t∗ has Lebesgue measure zero, which implies that 𝑆 has Lebesgue measure zero. Suppose, by contradiction, that 𝑆t∗ has positive Lebesgue measure: 𝜆(𝑆t∗ ) > 0. For all 𝜃 ∈ 𝑆t∗ , by the equivalence established above, 𝜇Y ({y ∈ 𝐸 : 𝑔t∗ (𝜃, y) ≠ 0}) = 0. Therefore, by Tonelli’s theorem: ∫ ∫ ∫ 0= 𝜇Y ({y ∈ 𝐸 : 𝑔t∗ (𝜃, y) ≠ 0}) d𝜆(𝜃) = 1{𝑔t∗ ( 𝜃 ,y)≠0} d𝜇Y (y)d𝜆(𝜃) 𝑆t∗ 𝑆t∗ 𝐸 ∫ ∫ = 1{𝑔t∗ ( 𝜃 ,y)≠0} d𝜆(𝜃)d𝜇Y (y). 𝐸
25
𝑆t∗
Since the integrand is nonnegative, it follows that, for 𝜇Y -almost every y ∈ 𝐸, 𝜆({𝜃 ∈ 𝑆t∗ : 𝑔t∗ (𝜃, y) ≠ 0}) = 0. Therefore, 𝜆({𝜃 ∈ 𝑆t∗ : 𝑔t∗ (𝜃, y) = 0}) = 𝜆(𝑆t∗ ) > 0, which means that, for 𝜇Y -almost every y ∈ 𝐸, the zero set of the analytic map 𝜃 ↦→ 𝑔t∗ (𝜃, y) has positive Lebesgue measure. By the identity theorem for real analytic functions, a real analytic function on an open and connected domain whose zero set has positive Lebesgue measure must be identically zero. Therefore, for 𝜇Y -almost every y ∈ 𝐸, 𝑔t∗ (·, y) ≡ 0 on Θ, and, in particular, 𝑔t∗ (𝜃 ∗ , y) = 0, 𝜇Y -almost everywhere on 𝐸. This contradicts the premise that 𝜇Y ({y ∈ 𝐸 : 𝑔t∗ (𝜃 ∗ , y) ≠ 0}) > 0. Hence the assumption that 𝑆t∗ has positive Lebesgue measure was false. It follows that 𝑆t∗ has Lebesgue measure zero. Since 𝑆 ⊆ 𝑆t∗ , we conclude that 𝑆 has Lebesgue measure zero. This completes the proof of (ii). Proof of (iii). We now show that, under Assumptions 4.4–4.6, for all y ∈ XY and all t ∈ XT , the real-valued map 𝜃 ↦→ 𝑝 𝜃 ,Y|do(T=t) (y) is analytic on Θ, which yields the premise of (i) and, via (i) and (ii), concludes the proof of Proposition 4.8. Fix an arbitrary t ∈ XT . By the truncated factorization formula ∫ (Pearl, 2009, Section 1.3), for all 𝜃 ∈ Θ and y ∈ XY , the interventional density is 𝑝 𝜃 ,Y|do(T=t) (y) = X 𝑝 𝜃 , (Y,W) |do(T=t) (y, w)d𝜇W (w), W with Ö 𝑝 𝜃 , (Y,W) |do(T=t) (y, w) = 𝑝 𝜃𝑉 (𝑣 | vpa(𝑉 ) ) T=t , (E.3) 𝑉 ∈V\T
where W := V \ (T ⊔ Y). For 𝑉 ∈ V, 𝜃 𝑉 ∈ Θ𝑉 , 𝑣 ∈ X𝑉 , and vpa(𝑉 )\T ∈ Xpa(𝑉 )\T , we define 𝑏 ∗𝑉 (𝑣, vpa(𝑉 )\T , t) := 𝑏 𝑉 (𝑣, vpa(𝑉 ) ) T=t , and
∗ 𝑠𝑉 (𝑣, vpa(𝑉 )\T , t) := 𝑠𝑉 (𝑣, vpa(𝑉 ) ) T=t ,
∗ 𝐴𝑉 (𝜂𝑉 (𝜃 𝑉 ), vpa(𝑉 )\T , t) := 𝐴𝑉 (𝜂𝑉 (𝜃 𝑉 ), vpa(𝑉 ) ) T=t ,
which are obtained by substituting T = t whenever T ⊆ pa(𝑉) and are such that ⊤ ∗
∗
𝑝 𝜃𝑉 (𝑣 | vpa(𝑉 ) ) T=t = 𝑏 ∗𝑉 (𝑣, vpa(𝑉 )\T , t)𝑒 𝜂𝑉 ( 𝜃𝑉 ) 𝑠𝑉 (𝑣,vpa(𝑉 )\T ,t) − 𝐴𝑉 ( 𝜂𝑉 ( 𝜃𝑉 ) ,vpa(𝑉 )\T ,t) . Recall that, by Assumption 4.6, if X = V \ T, for all 𝜃 ∈ Θ and all t ∈ XT , 𝑝 𝜃 ,X|do(T=t) (x) ∝ ⊤ e 𝑏t (x)𝑒 𝜂et ( 𝜃 ) e𝑠t (x) , where e 𝑏t , 𝜂et , and e 𝑠t are such that the parametrization is minimal, full, and 𝜂et (Θ) is open. We now adapt the argument used in the proof of Theorem 8 of Boeken et al. (2026) and proceed by showing the following steps. (a) For all 𝑉 ∈ V, 𝑣 ∈ X𝑉 , and vpa(𝑉 )\T ∈ Xpa(𝑉 )\T , the real-valued map 𝜃 𝑉 ↦→ 𝑝 𝜃𝑉 (𝑣 | vpa(𝑉 ) ) T=t is analytic on Θ𝑉 . (b) For all y ∈ XY and w ∈ XW , the real-valued map 𝜃 ↦→ 𝑝 𝜃 , (Y,W) |do(T=t) (y, w) is analytic on Θ. (c) The R 𝑘t -valued natural-parameter map 𝜃 ↦→ 𝜂et (𝜃) associated with the regular exponential family in Assumption 4.6 is analytic on Θ. (d) For all y ∈ XY , the real-valued map 𝜃 ↦→ 𝑝 𝜃 ,Y|do(T=t) (y) is analytic on Θ. After showing the above steps, since t ∈ XT was arbitrary, the result follows.
26
Step (a). Fix 𝑉 ∈ V, 𝑣 ∈ X𝑉 , and vpa(𝑉 )\T ∈ Xpa(𝑉 )\T . Let 𝜆𝑉 := 𝑏 ∗𝑉 (·, vpa(𝑉 )\T , t)𝜇𝑉 be a weighted measure on X𝑉 . Define the measure 𝜈𝑉 on R 𝑘𝑉 as the pushforward of 𝜆𝑉 under the map ∗ (·, v 𝑘𝑉 ∗ 𝑠𝑉 pa(𝑉 )\T , t) : X𝑉 → R , that is, 𝜈𝑉 := (𝑠𝑉 (·, vpa(𝑉 )\T , t))♯ 𝜆 𝑉 . Then, for all 𝜃 𝑉 ∈ Θ𝑉 , ∫ ⊤ ∗ 𝐴∗𝑉 ( 𝜂𝑉 ( 𝜃𝑉 ) ,vpa(𝑉 ) \T ,t) 𝑒 = 𝑏 ∗𝑉 (𝑣, vpa(𝑉 )\T , t)𝑒 𝜂𝑉 ( 𝜃𝑉 ) 𝑠𝑉 (𝑣,vpa(𝑉 )\T ,t) d𝜇𝑉 (𝑣) ∫X𝑉 ⊤ = 𝑒 𝜂𝑉 ( 𝜃𝑉 ) s d𝜈𝑉 (s). R 𝑘𝑉
∫
⊤
Let N𝑉 := {𝛾𝑉 ∈ R 𝑘𝑉 : R𝑘𝑉 𝑒 𝛾𝑉 s d𝜈𝑉 (s) < ∞} and define 𝐺 𝑉 : N𝑉 → (0, ∞) by 𝛾𝑉 ↦→ ⊤ ∗ 𝑒 𝛾𝑉 s d𝜈𝑉 (s). In particular, for all 𝜃 𝑉 ∈ Θ𝑉 , 𝐺 𝑉 (𝜂𝑉 (𝜃 𝑉 )) = 𝑒 𝐴𝑉 ( 𝜂𝑉 ( 𝜃𝑉 ) ,vpa(𝑉 )\T ,t) . Now define R 𝑘𝑉 e𝑉 : T𝑉 → C by T𝑉 := ∫{𝛾𝑉 + 𝑖𝜁𝑉 : 𝛾𝑉 ∈ N𝑉 , 𝜁𝑉 ∈ R 𝑘𝑉 } and define the complex extension 𝐺 ⊤s 𝑧𝑉 𝑧 𝑉 ↦→ R𝑘𝑉 𝑒 d𝜈𝑉 (s). ⊤ ⊤ e𝑉 is the Since, for all 𝛾𝑉 ∈ N𝑉 , 𝜁𝑉 ∈ R 𝑘𝑉 , 𝑧 𝑉 = 𝛾𝑉 + 𝑖𝜁𝑉 , and s ∈ R 𝑘𝑉 , one has |𝑒 𝑧𝑉 s | = 𝑒 𝛾𝑉 s , 𝐺 Fourier-Laplace transform of the pushforward measure 𝜈𝑉 . By Theorem 7.2 of Barndorff-Nielsen e𝑉 (𝑧 𝑉 ) is analytic on the interior int(T𝑉 ). Since 𝜂𝑉 (Θ𝑉 ) is (2014), the complex-valued map 𝑧 𝑉 ↦→ 𝐺 open by Assumption 4.5, and 𝜂𝑉 (Θ𝑉 ) ⊆ N𝑉 , we have 𝜂𝑉 (Θ𝑉 ) ⊆ int(N𝑉 ). Hence, for all 𝜃 𝑉 ∈ Θ𝑉 , 𝜂𝑉 (𝜃 𝑉 ) + 𝑖0 ∈ int(T𝑉 ). Moreover, the map 𝜃 𝑉 ↦→ 𝜂𝑉 (𝜃 𝑉 ) is analytic on Θ𝑉 by Assumption 4.5, so the composition e𝑉 (𝜂𝑉 (𝜃 𝑉 )) = 𝑒 𝐴∗𝑉 ( 𝜂𝑉 ( 𝜃𝑉 ) ,vpa(𝑉 )\T ,t) 𝜃 𝑉 ↦→ 𝐺 (E.4) e𝑉 (𝜂𝑉 (𝜃 𝑉 )) > 0, its reciprocal is analytic as well. is analytic on Θ𝑉 . Since, for all 𝜃 𝑉 ∈ Θ𝑉 , 𝐺 ∗ Moreover, since 𝑠𝑉 (𝑣, vpa(𝑉 )\T , t) does not depend on 𝜃 𝑉 and the exponential of an analytic function is analytic, it follows that the real-valued map ∫
⊤ ∗
𝜃 𝑉 ↦→ 𝑒 𝜂𝑉 ( 𝜃𝑉 ) 𝑠𝑉 (𝑣,vpa(𝑉 )\T ,t)
(E.5)
is analytic on Θ𝑉 . Therefore, the map 𝜃 𝑉 ↦→ 𝑝 𝜃𝑉 (𝑣 | vpa(𝑉 ) ) T=t is analytic on Θ𝑉 since it is the product of the 𝜃 𝑉 -independent factor 𝑏 ∗𝑉 (𝑣, vpa(𝑉 )\T , t), the analytic function in (E.5), and the reciprocal of the analytic function in (E.4). Since 𝑉 ∈ V, 𝑣 ∈ X𝑉 , and vpa(𝑉 )\T ∈ Xpa(𝑉 )\T were arbitrary, this holds for all such values. This proves (a). Step (b). By (E.3), for all y ∈ XY and w ∈ XW , the real-valued map 𝜃 ↦→ 𝑝 𝜃 , (Y,W) |do(T=t) (y, w) is a finite product of analytic functions, hence analytic on Θ. Therefore, (b) holds. Step (c). By Assumption 4.6, the post-intervention joint distribution lies in a regular exponential family. Then, for all 𝜃 ∈ Θ and x ∈ XX , ⊤
𝑝 𝜃 ,X|do(T=t) (x) = e 𝑏t (x)𝑒 𝜂et ( 𝜃 ) e𝑠t (x) − 𝐴t ( 𝜂et ( 𝜃 ) ) . e
Minimality guarantees the existence of 𝑘 + 1 points x0 , . . . , x 𝑘 ∈ XX such that the 𝑘 difference vectors ut1 := e 𝑠t (x1 ) − e 𝑠t (x0 ), . . . , ut𝑘 := e 𝑠t (x 𝑘 ) − e 𝑠t (x0 ) are linearly independent. For all 𝜃 ∈ Θ and x ∈ XX , et (e taking the logarithm of the density yields log 𝑝 𝜃 (x | do(t)) = log e 𝑏t (x) + 𝜂et (𝜃) ⊤e 𝑠t (x) − 𝐴 𝜂t (𝜃)). Thus, for all 𝑖 ∈ {1, . . . , 𝑘 }, log 𝑝 𝜃 ,X|do(T=t) (x𝑖 ) − log 𝑝 𝜃 ,X|do(T=t) (x0 ) = (log e 𝑏t (x𝑖 ) − log e 𝑏t (x0 )) + 𝜂et (𝜃) ⊤ (e 𝑠t (x𝑖 ) − e 𝑠t (x0 )) = −𝐶𝑖t + (ut𝑖 ) ⊤ 𝜂et (𝜃), 27
where 𝐶𝑖t := − log e 𝑏t (x𝑖 ) + log e 𝑏t (x0 ). We rearrange this to define, for 𝑖 ∈ {1, . . . , 𝑘 }, ℎt𝑖 (𝜃) := log 𝑝 𝜃 ,X|do(T=t) (x𝑖 ) − log 𝑝 𝜃 ,X|do(T=t) (x0 ) + 𝐶𝑖t = (ut𝑖 ) ⊤ 𝜂et (𝜃). Since in the previous steps we established that the joint density is analytic in 𝜃, for all 𝑖 ∈ {1, . . . , 𝑘 }, ℎt𝑖 is analytic as well as it is a difference of analytic functions plus a constant. Let 𝑈t := [ut1 , . . . , ut𝑘 ] be the 𝑘 × 𝑘 matrix whose 𝑖-th column is ut𝑖 , for all 𝑖 ∈ {1, . . . , 𝑘 }, and let ℎt (𝜃) := (ℎt1 (𝜃), . . . , ℎt𝑘 (𝜃)) ⊤ be the 𝑘-dimensional vector whose 𝑖-th entry is ℎt𝑖 (𝜃), for all 𝑖 ∈ {1, . . . , 𝑘 }. Then, we can write 𝑈t⊤ 𝜂et (𝜃) = ℎt (𝜃). Since the vectors ut1 , . . . , ut𝑘 are linearly independent, the matrix 𝑈t (and therefore 𝑈t⊤ ) has full rank 𝑘t and is invertible. Multiplying both sides by the inverse yields 𝜂et (𝜃) = (𝑈t⊤ ) −1 ℎt (𝜃). As a linear combination of the analytic components of ℎt (𝜃), the map 𝜃 ↦→ 𝜂et (𝜃) is analytic on Θ. The claim in (c) then follows. Step (d).
Let A, B be such that A ⊔ B = V \ T. For all b ∈ XB , the integral ∫ ⊤ e 𝜂et ↦→ 𝑏t (a, b)𝑒 𝜂et e𝑠t (a,b) d𝜇A (a) XA
can be viewed as the Fourier-Laplace transform of a pushforward measure. By Theorem 7.2 of Barndorff-Nielsen (2014), this map is analytic on a complex domain which, due to the openness of 𝜂et (Θ) given by Assumption 4.6, is open and contains 𝜂et (Θ). Consequently, its restriction to the real parameter space is analytic on 𝜂et (Θ). Because the map 𝜃 ↦→ 𝜂et (𝜃) is analytic on Θ by (c), for all b ∈ XB , the composition ∫ ⊤ e 𝜃 ↦→ 𝑏t (a, b)𝑒 𝜂et ( 𝜃 ) e𝑠t (a,b) d𝜇A (a) XA
is analytic on Θ. Taking A = W = V \ (T ⊔ Y), we obtain, for all 𝜃 ∈ Θ, t ∈ XT , and y ∈ XY , the unnormalized marginal ∫ ⊤ e 𝑝 𝜃 ,Y|do(T=t) (y) ∝ 𝑏t (y, w)𝑒 𝜂et ( 𝜃 ) e𝑠t (y,w) d𝜇W (w). XW
Taking instead A = X = V \ T, we obtain, for all 𝜃 ∈ Θ, the normalizing factor ∫ ⊤ e e 𝑒 𝐴t ( 𝜂et ( 𝜃 ) ) = 𝑏t (x)𝑒 𝜂et ( 𝜃 ) e𝑠t (x) d𝜇X (x). XX
Both the unnormalized marginal and the normalizing factor are therefore analytic in 𝜃. Since, for all e e 𝜃 ∈ Θ, 𝑒 𝐴t ( 𝜂et ( 𝜃 ) ) > 0, its reciprocal 𝑒 − 𝐴t ( 𝜂et ( 𝜃 ) ) is also analytic in 𝜃. Therefore, for all y ∈ XY and all t ∈ XT , the real-valued map 𝜃 ↦→ 𝑝 𝜃 ,Y|do(T=t) (y) is analytic on Θ as a product of analytic functions. This concludes the proof of Proposition 4.8. E.3 Proof of Theorem 4.9 Theorem 4.9 (Almost-surely correct verifier). For conditional exponential-family parametrizations, under Assumptions 4.4–4.7, the falsifier in Definition 4.1 induces an almost-surely correct verifier relative to PΘ (XV ). Proof. If the input to the falsifier is 𝜙 = none, the falsifier checks non-identifiability using the ID algorithm, returning false if the ID algorithm returns an identifying formula and true else. Since 28
the ID algorithm is sound and complete for identification, the falsifier’s output for the input none is correct. If the input to the falsifier is a candidate observational formula 𝜙 ∈ ΦY,T there are two cases. First, if 𝜙 is identifying relative to the chosen parametric family, then Equation (1) holds for all t ∈ XT and for all densities factorizing according to the graph whenever 𝜙 is well-defined. Hence, the falsifier never finds a counterexample and outputs true; in other words, the falsifier never incorrectly rejects an observational formula that is identifying as false. Second, if 𝜙 is not identifying relative to the chosen parametric family, then, by Proposition 4.8, the set 𝑆 of parameters where the candidate formula equals the target interventional density has Lebesgue measure zero. By absolute continuity of 𝜋 with respect to the Lebesgue measure, this implies that 𝜋(𝑆) = 0. Then, ! 𝐾 𝐾 Ù Ö P {𝜃 𝑖 ∈ 𝑆} = P(𝜃 𝑖 ∈ 𝑆) = (𝜋(𝑆)) 𝐾 = 0, 𝑖=1
𝑖=1
which implies that, if 𝜙 is not identifying relative to the chosen parametric family, the falsifier incorrectly accepts it as true with probability zero. This completes the proof of Theorem 4.9, which establishes a one-sided guarantee: if the falsifier rejects a candidate formula, it has found an actual counterexample and the rejection is correct; if the falsifier accepts a candidate formula, its output is correct almost surely, relative to the chosen parametric family. E.4 Proof of Theorem G.3 Theorem G.3 (Bound on false acceptance of non-identifying formulas). Suppose that the evaluation length of 𝜙 is at most 𝑐, and that 𝜙 is non-identifying relative to PΘ (XV ), that is, there exist 𝜃 ∗ ∈ Θ and t∗ ∈ XT such that the equality ⟦𝜙⟧( 𝑝 𝜃 ∗ ,O , t∗ ) = 𝑝 𝜃 ∗ ,Y|do(T=t∗ ) 𝜇Y -almost everywhere does not hold. Let 𝜃 ′ be the vector that collects all sampled parameters. Then, the probability that the falsifier accepts 𝜙 at the sampled parameter 𝜃 ′ satisfies Î𝑐 𝛾𝑙 (2𝑛 − 1) 1 + 𝑙=1 P ∀t ∈ XT , ⟦𝜙⟧( 𝑝 𝜃 ′ ,O , t) = 𝑝 𝜃 ′ ,Y|do(T=t) 𝜇Y -a.e. ≤ , (G.7) min1≤𝑖 ≤𝑑 | 𝐴𝑖 | where, for all 𝑙 ∈ {1, . . . , 𝑐}, 1, 𝛾𝑙 := 2, 𝑛 + 1,
if operation 𝑙 is Gaussian marginalization, if operation 𝑙 is scalar addition, subtraction, multiplication or division, if operation 𝑙 is Gaussian conditioning.
(G.8)
Proof. Since 𝜙 is non-identifying and since both the distribution returned by 𝜙 and the target interventional distribution are Gaussian, there exist 𝜃 ∗ ∈ Θ and t∗ ∈ XT such that at least one scalar entry of either 𝜇 𝜙 (𝜃 ∗ , t∗ ) − 𝜇do (𝜃 ∗ , t∗ ) or Σ 𝜙 (𝜃 ∗ ) − Σdo (𝜃 ∗ ) is non-zero. Let Δ(𝜃, t∗ ) denote such an entry, viewed as a rational function of 𝜃 after fixing t∗ , and write Δ(𝜃, t∗ ) = 𝑝Δ (𝜃)/𝑞Δ (𝜃). For all 𝜃 ∈ Θ, the corresponding Gaussian model is non-degenerate, and the admissible operations in 𝜙 preserve non-degeneracy (see Appendix B.1); hence, 𝑞Δ (𝜃) ≠ 0. Since Δ(𝜃 ∗ , t∗ ) ≠ 0, we have 𝑝Δ (𝜃 ∗ ) ≠ 0, and hence 𝑝Δ . 0. Let 𝐸 := ∀t ∈ XT , ⟦𝜙⟧( 𝑝 𝜃 ′ ,O , t) = 𝑝 𝜃 ′ ,Y|do(T=t) 𝜇Y -a.e. 29
be the event that the falsifier accepts 𝜙 at the sampled parameter 𝜃 ′ . If 𝐸 occurs, then the falsifier accepts, meaning that all scalar mean and covariance discrepancies vanish for all intervention values. In particular, the specific witness discrepancy Δ(𝜃 ′ , t∗ ) evaluated at the sampled parameter must vanish. Therefore, 𝐸 ⊆ {𝑝Δ (𝜃 ′ ) = 0} and P(𝐸) ≤ P( 𝑝Δ (𝜃 ′ ) = 0). By Theorem G.2, it remains to bound the degree of the non-zero polynomial 𝑝Δ . We first bound the degrees of the Gaussian quantities from which the evaluation of 𝜙 starts. Recall that 𝐵 is the 𝑛 × 𝑛 matrix collecting all edge coefficients. Since G is acyclic, for all integer 𝑚 ≥ 𝑛, (𝐵⊤ ) 𝑚 = 0, and therefore (𝐼 − 𝐵⊤ ) −1 = 𝐼 +
𝑛−1 ∑︁
(𝐵⊤ ) 𝑚 .
𝑚=1
Hence each entry of (𝐼 − 𝐵⊤ ) −1 is a polynomial in the edge coefficients of degree at most 𝑛 − 1. For all 𝑖, 𝑗 ∈ {1, . . . , 𝑛}, the (𝑖, 𝑗)-th entry of the covariance matrix in Equation (G.6) is Σ𝑖full 𝑗 (𝜃) =
𝑛 ∑︁
[(𝐼 − 𝐵⊤ ) −1 ] 𝑖𝑘 𝜎𝑘2 [(𝐼 − 𝐵) −1 ] 𝑘 𝑗 ,
𝑘=1
where, for all 𝑘 ∈ {1, . . . , 𝑛}, 𝜎𝑘2 is the variance of the 𝑘-th variable conditional on its parents. Therefore, the corresponding degree is such that deg(Σ𝑖full 𝑗 (𝜃)) ≤ (𝑛 − 1) + 1 + (𝑛 − 1) = 2𝑛 − 1. Í Similarly, for all 𝑖 ∈ {1, . . . , 𝑛}, the 𝑖-th entry of the mean is 𝜇𝑖full (𝜃) = 𝑛𝑘=1 [(𝐼 − 𝐵⊤ ) −1 ] 𝑖𝑘 𝛼 𝑘 , where, for all 𝑘 ∈ {1, . . . , 𝑛}, 𝛼 𝑘 is the mean of the 𝑘-th noise term. The corresponding degree is such that deg(𝜇𝑖full (𝜃)) ≤ (𝑛 − 1) + 1 = 𝑛 ≤ 2𝑛 − 1. Set ℎ0 := 2𝑛 − 1. Every scalar entry of the mean and covariance has therefore degree at most ℎ0 as polynomial in the parameters. Equivalently, the observational Gaussian quantities can be represented in shared-denominator form as 𝜇full (𝜃) = 𝑚 full (𝜃)/1 and Σfull (𝜃) = 𝐴full (𝜃)/1, where all numerator entries have degree at most ℎ0 . The same bound applies to the entries of the target interventional quantities 𝜇do (𝜃, t∗ ) and Σdo (𝜃), because after intervention these entries are again obtained from a linear Gaussian submodel on at most 𝑛 nodes. We now bound how degrees can grow during the evaluation of the candidate formula 𝜙. Suppose that, at some intermediate stage, scalar rational expressions have numerator and denominator degree at most ℎ, and every intermediate Gaussian mean and covariance is represented in shared-denominator form as 𝑚(𝜃) 𝐴(𝜃) 𝜇(𝜃) = , Σ(𝜃) = , 𝑒(𝜃) 𝑑 (𝜃) where 𝑚(𝜃) is a vector of polynomial numerators, 𝐴(𝜃) is a matrix of polynomial numerators, and 𝑒(𝜃) and 𝑑 (𝜃) are scalar polynomial denominators. Assume that every entry of 𝑚(𝜃) and 𝐴(𝜃), and the denominators 𝑒(𝜃) and 𝑑 (𝜃), have degree at most ℎ. We claim that one primitive operation increases this degree bound by at most the factor 𝑛 + 1. 30
Marginalization only selects subvectors and submatrices, and therefore does not increase degrees. Scalar addition, subtraction, multiplication, and division increase ℎ by at most a factor of 2. For example, 𝑝 1 (𝜃)/𝑞 1 (𝜃) + 𝑝 2 (𝜃)/𝑞 2 (𝜃) = ( 𝑝 1 (𝜃)𝑞 2 (𝜃) + 𝑝 2 (𝜃)𝑞 1 (𝜃))/(𝑞 1 (𝜃)𝑞 2 (𝜃)), and both numerator and denominator degrees are at most 2ℎ. The same holds for multiplication and division. Consider an intermediate Gaussian distribution on disjoint variable sets (A, B), with |A| = 𝑞 ≤ 𝑛 and |B| = 𝑝 ≤ 𝑛. Write its mean vector and covariance matrix in shared-denominator form as 1 𝑚A (𝜃) 1 𝐴AA (𝜃) 𝐴AB (𝜃) 𝜇(𝜃) = , Σ(𝜃) = . 𝑒(𝜃) 𝑚B (𝜃) 𝑑 (𝜃) 𝐴BA (𝜃) 𝐴BB (𝜃) where Σ(𝜃), 𝐴AA (𝜃), 𝐴BB (𝜃) are symmetric and 𝐴BA (𝜃) = 𝐴AB (𝜃) ⊤ . For all b ∈ XB , conditioning gives 𝜇A|B=b (𝜃) = 𝜇A (𝜃) + ΣAB (𝜃)ΣBB (𝜃) −1 (b − 𝜇B (𝜃)), ΣA|B (𝜃) = ΣAA (𝜃) − ΣAB (𝜃)ΣBB (𝜃) −1 ΣBA (𝜃). First, we treat the covariance update. Since ΣBB (𝜃) = 𝐴BB (𝜃)/𝑑 (𝜃), we have ΣBB (𝜃) −1 = 𝑑 (𝜃)
adj( 𝐴BB (𝜃)) . det( 𝐴BB (𝜃))
We bound the degree of the determinant and the adjugate entries. By the Leibniz formula, det( 𝐴BB (𝜃)) =
∑︁
sign(𝜆)
𝑝 Ö
( 𝐴BB (𝜃))ℓ,𝜆(ℓ ) ,
ℓ=1
𝜆∈Λ 𝑝
where Λ 𝑝 is the set of all permutations of {1, . . . , 𝑝}. For all 𝜆 ∈ Λ 𝑝 , the product contains 𝑝 factors, each of degree at most ℎ. Hence, each product has degree at most 𝑝ℎ. Taking a sum cannot increase the degree beyond the maximum degree of the summands, so deg(det( 𝐴BB (𝜃))) ≤ 𝑝ℎ. For all 𝑖, 𝑗 ∈ {1, . . . , 𝑝}, the (𝑖, 𝑗)-th entry of the adjugate matrix is a cofactor: adj( 𝐴BB (𝜃))𝑖 𝑗 = (−1) 𝑖+ 𝑗 det ( 𝐴BB (𝜃)) ( 𝑗,𝑖) , where ( 𝐴BB (𝜃)) ( 𝑗,𝑖) is obtained by deleting row 𝑗 and column 𝑖. This minor has size ( 𝑝 − 1) × ( 𝑝 − 1). Applying the same determinant argument to this minor, each determinant term is a product of 𝑝 − 1 entries, each of degree at most ℎ. Hence each such product has degree at most ( 𝑝 − 1)ℎ, and taking the sum over permutations cannot increase the degree. Therefore, deg(adj( 𝐴BB (𝜃))𝑖 𝑗 ) ≤ ( 𝑝 − 1)ℎ. Substituting these expressions into the conditional covariance gives ΣA|B (𝜃) =
𝐴AA (𝜃) det( 𝐴BB (𝜃)) − 𝐴AB (𝜃) adj( 𝐴BB (𝜃)) 𝐴BA (𝜃) . 𝑑 (𝜃) det( 𝐴BB (𝜃)) 31
Each entry of the first numerator term has degree at most ℎ + 𝑝ℎ = ( 𝑝 + 1)ℎ. For the second numerator term, for all 𝑖, 𝑗 ∈ {1, . . . , 𝑞}, the (𝑖, 𝑗)-th entry is a sum of products of the form ( 𝐴AB (𝜃))𝑖𝑢 adj( 𝐴BB (𝜃))𝑢𝑣 ( 𝐴BA (𝜃)) 𝑣 𝑗 , with 𝑢, 𝑣 ∈ {1, . . . , 𝑝}. Each such product has degree at most ℎ + ( 𝑝 − 1)ℎ + ℎ = ( 𝑝 + 1)ℎ. Since taking sums cannot increase the degree beyond the maximum degree of the summands, every numerator entry has degree at most ( 𝑝 + 1)ℎ. The denominator 𝑑 (𝜃) det( 𝐴BB (𝜃)) also has degree at most ℎ + 𝑝ℎ = ( 𝑝 + 1)ℎ. Since 𝑝 ≤ 𝑛, every entry of ΣA|B (𝜃) can be represented with numerator and denominator degree at most (𝑛 + 1)ℎ. The conditional mean is controlled by the same inverse block. Since b is fixed, each component of b − 𝜇B (𝜃) can be written as (b𝑒(𝜃) − 𝑚B (𝜃))/𝑒(𝜃), with numerator and denominator degree at most ℎ. Using the expression for ΣBB (𝜃) −1 above, we obtain 𝜇A|B=b (𝜃) =
𝑚A (𝜃) det( 𝐴BB (𝜃)) + 𝐴AB (𝜃) adj( 𝐴BB (𝜃)) (b𝑒(𝜃) − 𝑚B (𝜃)) . 𝑒(𝜃) det( 𝐴BB (𝜃))
The first numerator term has degree at most ℎ + 𝑝ℎ = ( 𝑝 + 1)ℎ. Each entry of the second numerator term is a sum of products with degree at most ℎ + ( 𝑝 − 1)ℎ + ℎ = ( 𝑝 + 1)ℎ. The denominator has degree at most ℎ + 𝑝ℎ = ( 𝑝 + 1)ℎ. Thus, every entry of the conditional mean also has numerator and denominator degree at most (𝑛 + 1)ℎ. We showed that every primitive operation increases the current degree bound by at most the factor 𝑛 + 1. Since the evaluation length of 𝜙 is at most 𝑐, if, for all 𝑙 ∈ {0, . . . , 𝑐 − 1}, ℎ𝑙 denotes the degree bound after 𝑙 primitive operations, then ℎ𝑙+1 ≤ 𝛾𝑙+1 ℎ𝑙 , with 𝛾𝑙+1 defined in Equation (G.8). Î𝑐 Starting from ℎ0 = 2𝑛 − 1, we obtain ℎ 𝑐 ≤ (2𝑛 − 1) 𝑙=1 𝛾𝑙 . Hence, every scalar entry of 𝜇 𝜙 (𝜃, t∗ ) and Σ 𝜙 (𝜃) can be written as a rational function whose numerator and denominator have total degree at most 𝑐 Ö 𝐻 := (2𝑛 − 1) 𝛾𝑙 . 𝑙=1
We now return to the polynomial 𝑝Δ . The discrepancy Δ(𝜃, t∗ ) is the difference between one scalar entry produced by 𝜙 and the corresponding scalar entry of the target interventional distribution. Write the entry produced by 𝜙 as 𝑝 𝜙 (𝜃)/𝑞 𝜙 (𝜃), where deg( 𝑝 𝜙 (𝜃)), deg(𝑞 𝜙 (𝜃)) ≤ 𝐻. Write the corresponding target entry as 𝑝do (𝜃)/𝑞do (𝜃). By the previous bound on the target interventional mean and covariance, deg( 𝑝do (𝜃)), deg(𝑞do (𝜃)) ≤ ℎ0 = 2𝑛 − 1. We have Δ(𝜃, t∗ ) =
𝑝 𝜙 (𝜃) 𝑝do (𝜃) 𝑝 𝜙 (𝜃)𝑞do (𝜃) − 𝑝do (𝜃)𝑞 𝜙 (𝜃) − = . 𝑞 𝜙 (𝜃) 𝑞do (𝜃) 𝑞 𝜙 (𝜃)𝑞do (𝜃)
Thus, we may take 𝑝Δ (𝜃) = 𝑝 𝜙 (𝜃)𝑞do (𝜃) − 𝑝do (𝜃)𝑞 𝜙 (𝜃). Since Δ(𝜃 ∗ , t∗ ) ≠ 0, we have 𝑝Δ (𝜃 ∗ ) ≠ 0, and hence 𝑝Δ . 0. Each product has degree at most 𝐻 + ℎ0 , and the difference cannot increase the degree. Hence, deg( 𝑝Δ (𝜃)) ≤ 𝐻 + ℎ0 . Applying Theorem G.2 to the non-zero polynomial 𝑃Δ gives Î𝑐 (2𝑛 − 1) 1 + 𝑙=1 𝛾𝑙 𝐻 + ℎ0 ′ P( 𝑝Δ (𝜃 ) = 0) ≤ = . min1≤𝑖 ≤𝑑 | 𝐴𝑖 | min1≤𝑖 ≤𝑑 | 𝐴𝑖 | Since 𝐸 ⊆ {𝑃Δ (𝜃 ′ ) = 0}, this concludes the proof of Theorem G.3. 32
Appendix F. Alternative implementation via the nested Markov model In Section 4, we instantiate the falsifier by replacing the input acyclic directed mixed graph G 𝑝 with its canonical directed acyclic graph. There are, however, infinitely many latent-variable directed acyclic graphs whose latent projection is G 𝑝 . An alternative is to avoid specifying the latent structure e𝑝 , that is, a maximal arid graph on and to work directly with G 𝑝 and its maximal arid projection G the same observed set as G 𝑝 . Aridity excludes certain graphical structures that prevent identifiability of the associated linear structural equation model (Drton et al., 2011). We refer to (Shpitser et al., 2018) for a formal definition of maximal arid projection and for an algorithm for computing it. Let XO = (𝑋𝑂1 , . . . , 𝑋𝑂𝑛 ) ⊤ denote the random vector associated with the observed variables O. e𝑝 : We consider the linear Gaussian structural equation model associated with G XO = 𝐵⊤ XO + 𝜖, where 𝐵 = (𝑏 𝑖 𝑗 ) ∈ R𝑛×𝑛 is such that, for all 𝑖, 𝑗 ∈ {1, . . . , 𝑛}, 𝑏 𝑖 𝑗 = 0 whenever 𝑂 𝑖 → 𝑂 𝑗 is not an e𝑝 , and where 𝜖 ∼ N (0, Ω), with Ω = (𝜔𝑖 𝑗 ) ∈ R𝑛×𝑛 positive definite and such that, for edge of G e𝑝 . The resulting all 𝑖, 𝑗 ∈ {1, . . . , 𝑛} with 𝑖 ≠ 𝑗, 𝜔𝑖 𝑗 = 0 whenever 𝑂 𝑖 ↔ 𝑂 𝑗 is not an edge of G −⊤ −1 covariance matrix is Σ = (𝐼𝑛 − 𝐵) Ω(𝐼𝑛 − 𝐵) . Under this parametrization, the falsifier can sample a masked matrix 𝐵 and positive definite matrix Ω, and then proceed as in Definition 4.1, but without choosing a particular latent structure. Let K ⊆ {1, . . . , 𝑛} be the set of indices such that T = {𝑂 𝑘 | 𝑘 ∈ K}. We can compute the interventional density by setting, for all 𝑘 ∈ K and all 𝑖 ∈ {1, . . . , 𝑛}, 𝑏 𝑖𝑘 = 0, and setting, for all 𝑘 ∈ K and 𝑖 ∈ {1, . . . , 𝑛} \ {𝑘 }, 𝜔𝑖𝑘 = 𝜔 𝑘𝑖 = 0. This construction is justified by the relationship between maximal arid projections and nested Markov models. Nested Markov models are graphical models for acyclic directed mixed graphs that capture not only the conditional independences but also generalized equality constraints implied by latent-variable models (see Shpitser et al., 2014, for an introduction). The maximal arid projection e𝑝 of an acyclic directed mixed graph G 𝑝 defines the same nested Markov model as G 𝑝 (Shpitser G et al., 2018, Theorem 30). Moreover, Shpitser et al. (2018, Theorem 35) show that the above linear e𝑝 of G 𝑝 coincides Gaussian structural equation model associated with the maximal arid projection G with the Gaussian nested Markov model of G 𝑝 . Thus, the maximal arid projection gives a linear Gaussian parametrization of exactly the Gaussian nested Markov model associated with G 𝑝 , rather than a potentially smaller model associated with the linear Gaussian structural equation model on G 𝑝 itself (Shpitser et al., 2018, Theorem 34). Both implementations (via the canonical directed acyclic graph or the maximal arid projection) should be contrasted to specifying a particular latent-variable directed acyclic graph and parametrizing that. Margins of latent-variable models may satisfy constraints beyond conditional independence, including generalized equality constraints, such as the Verma constraint (Verma and Pearl, 1990; Spirtes et al., 2000, Section 6.9), and inequality constraints, such as the instrumental inequalities of Pearl (1995b). The implementation based on the canonical directed acyclic graph fixes one particular latent structure whose latent projection is G 𝑝 , and may therefore fail to represent inequality constraints implied by other latent-variable directed acyclic graphs with the same latent projection. Conversely, the implementation based on the maximal arid projection works with the Gaussian nested Markov model, which does not, in general, capture inequality constraints (in the discrete case, nested Markov models capture all equality constraints though; Evans, 2018). Thus, there may exist distributions in the Gaussian nested Markov model of G 𝑝 that do not arise as observable margins of any such latent-variable model (Shpitser et al., 2014). This is not an obstacle for verifying candidate 33
observational formulas for interventional distributions, since identification of interventionals in latent-variable causal directed acyclic graphs is characterized at the level of the latent projection (Richardson et al., 2023). If the goal were instead to verify (in-)equality constraints, then the latent structure would have to be specified explicitly.
Appendix G. Numerical evaluation and exact arithmetic Theorem 4.9 gives an almost-sure guarantee for the falsification-based verifier under exact evaluation and absolutely continuous parameter sampling. This guarantee does not apply in floating-point implementations, where exact equality is replaced by comparison up to a tolerance 𝜂 > 0, and a non-zero discrepancy may be treated as zero. To see this, consider the linear Gaussian model on 𝑇 → 𝑋1 → · · · → 𝑋𝑟 → 𝑌 , with 𝑟 ∈ N, and all pairwise conditionals being of the form 𝑉 | 𝑊 = 𝑤 ∼ N (𝑤/2, 1) where pa(𝑉) = {𝑊 }. Under do(𝑇 = 𝑡), the coefficient of 𝑡 in the interventional mean of 𝑌 is (1/2) 𝑟+1 . Suppose that an incorrect candidate formula sets this coefficient to zero. Then, at 𝑡 = 1, the absolute discrepancy in the mean is (1/2) 𝑟+1 . With tolerance 𝜂 = 10−6 , this discrepancy is below the tolerance as soon as (1/2) 𝑟+1 < 10−6 , which first occurs at 𝑟 = 19. Thus, a tolerance-based falsifier may accept an invalid formula simply because the discrepancy is numerically small. Further decreasing the tolerance is not a principled solution, since floatingpoint arithmetic cannot represent arbitrarily small positive numbers, and underflow and rounding limit what can be distinguished numerically. For sufficiently large 𝑟, a non-zero discrepancy may therefore be treated as exactly zero. Thus, a naive floating-point implementation does not inherit the almost-sure one-sided guarantee. The measure-zero result rules out accidental exact agreement under exact evaluation and absolutely continuous parameter sampling, but says nothing about non-zero discrepancies that are hidden by underflow or a fixed tolerance. Treating this as a routine, numerical nuisance would disconnect the implementation from the theorem. A reliable falsifier must either decide the polynomial identity problem symbolically or control and analyze the additional error of a deliberate numerical implementation. In the linear Gaussian case, we consider an implementation based on exact arithmetic (and sampling parameters from a finite set of integers), which avoids floating-point error and allows us to bound the probability of this implementation falsely accepting a non-identifying formula (Theorem G.3). Suppose that G has 𝑛 nodes. We consider a parametric family {{𝑝 𝜃𝑗 (𝑣 𝑗 | vpa(𝑉𝑗 ) )} 𝜃𝑗 ∈Θ𝑗 }𝑉𝑗 ∈V where, for all 𝑗 ∈ {1, . . . , 𝑛} and all 𝜃 𝑗 = (𝛼𝑗 , {𝛽𝑖 𝑗 }𝑖:𝑉𝑖 ∈pa(𝑉𝑗 ) , 𝜎𝑗2 ) ∈ Θ𝑗 ⊆ R𝑑𝑗 , with 𝜎𝑗2 > 0, ∑︁ © ª 𝑝 𝜃𝑗 (𝑣 𝑗 | vpa(𝑉𝑗 ) ) = N 𝑣 𝑗 ; 𝛼𝑗 + 𝛽𝑖 𝑗 𝑣 𝑖 , 𝜎𝑗2 ® . 𝑖:𝑉𝑖 ∈pa(𝑉𝑗 ) « ¬ Í 𝑛 The parameter vector 𝜃 = (𝜃 1 , . . . , 𝜃 𝑛 ) ∈ Θ ⊆ R𝑑 , with 𝑑 = 𝑗=1 𝑑𝑗 , then collects all intercepts, edge coefficients and conditional variances. Define 𝛼 = (𝛼1 , . . . , 𝛼𝑛 ) ⊤ , Ω = diag(𝜎12 , . . . , 𝜎𝑛2 ), and the 𝑛 × 𝑛 matrix 𝐵, where, for all 𝑖, 𝑗 ∈ {1, . . . , 𝑛}, 𝑖 ≠ 𝑗, 𝐵𝑖 𝑗 = 𝛽𝑖 𝑗 if 𝑉𝑖 ∈ pa(𝑉𝑗 ), and 𝐵𝑖 𝑗 = 0 otherwise. Then the product of all Gaussian conditionals induces a joint Gaussian distribution with mean vector and covariance matrix 𝜇full (𝜃) = (𝐼 − 𝐵⊤ ) −1 𝛼,
Σfull (𝜃) = (𝐼 − 𝐵⊤ ) −1 Ω(𝐼 − 𝐵) −1 .
34
(G.6)
For fixed 𝜃 ∈ Θ and t ∈ XT , both the distribution returned by the candidate observational formula 𝜙 and the target interventional distribution are Gaussian. Therefore, checking that, for all t ∈ XT , ⟦𝜙⟧( 𝑝 𝜃 ,O , t) = 𝑝 𝜃 ,Y|do(T=t) 𝜇Y -almost everywhere is equivalent to checking equality of their mean vectors and covariance matrices; see also Section 4.1. For all 𝜃 ∈ Θ and t ∈ XT , let 𝜇 𝜙 (𝜃, t) and Σ 𝜙 (𝜃) denote the mean vector and covariance matrix obtained from the candidate formula 𝜙, and let 𝜇do (𝜃, t) and Σdo (𝜃) denote the corresponding quantities for the target interventional distribution. Since, for all 𝜃 ∈ Θ, Σ 𝜙 (𝜃) and Σdo (𝜃) are independent of t, and since, for all 𝜃 ∈ Θ, 𝜇 𝜙 (𝜃, t) and 𝜇do (𝜃, t) are affine functions of t, it is enough to compare the covariance matrices and compare the mean vectors at |T| + 1 affinely independent intervention values. In a linear Gaussian model, the entries of these vectors and matrices are rational functions of the model parameters. Therefore, after clearing denominators, verification reduces to checking whether the resulting polynomial differences are identically zero. This problem is known as polynomial identity testing (Shpilka and Yehudayoff, 2010), defined as follows. Definition G.1 (Polynomial identity testing). Let F be a field, and let F[𝑥 1 , . . . , 𝑥 𝑠 ] denote the set of polynomials in 𝑥 1 , . . . , 𝑥 𝑠 with coefficients in F. Given 𝑔 ∈ F[𝑥1 , . . . , 𝑥 𝑠 ], the polynomial identity testing problem is to decide whether 𝑔 is identically zero, that is, 𝑔 ≡ 0. Designing efficient deterministic algorithms for polynomial identity testing is an open problem in algebraic complexity theory. A standard alternative to computationally expensive symbolic solutions is randomized evaluation: choose a finite sampling set 𝐴 ⊆ F, sample 𝑥 ′ = (𝑥 1′ , . . . , 𝑥 𝑠′ ) ∈ 𝐴𝑠 , and evaluate 𝑔(𝑥 ′ ) exactly. If 𝑔(𝑥 ′ ) ≠ 0, then necessarily 𝑔 . 0. If 𝑔(𝑥 ′ ) = 0, then either 𝑔 ≡ 0, or 𝑔 . 0 and 𝑥 ′ lies in the zero set of 𝑔. The following result, due to DeMillo and Lipton (1978), Zippel (1979), and Schwartz (1980), and widely known as the Schwartz-Zippel lemma, bounds the probability of this latter event. Theorem G.2 (Schwartz-Zippel). Let 𝐴 ⊆ F be a non-empty finite set. For every non-zero polynomial 𝑔 ∈ F[𝑥 1 , . . . , 𝑥 𝑠 ] of total degree at most 𝐷, if 𝑥 ′ = (𝑥1′ , . . . , 𝑥 𝑠′ ) is sampled uniformly from 𝐴𝑠 , then 𝐷 P 𝑔(𝑥 ′ ) = 0 ≤ . | 𝐴| Our implementation based on exact arithmetic therefore avoids numerical issues that floating-point implementations would incur. It does not, however, rely on a full symbolic decision procedure for polynomial identity testing, which would be computationally expensive. Instead, we use a randomized procedure, which replaces the absolutely continuous parameter sampling in Theorem 4.9 by finite-set sampling, and therefore changes the guarantee. A non-zero polynomial may vanish at the sampled point, despite exact arithmetic being used, if the sampled point is exactly a zero of the polynomial. With Theorem G.2, we can bound the probability of this happening and in turn of the proposed falsifier falsely accepting a non-identifying formula as valid. For all 𝑖 ∈ {1, . . . , 𝑑1 , . . . , 𝑑1 + 𝑑2 , . . . , 𝑑}, that is, for each scalar parameter in 𝜃, let 𝐴𝑖 be a non-empty finite sampling set, and sample the corresponding parameter uniformly from 𝐴𝑖 . In our implementation, intercepts 𝛼𝑗 and edge coefficients 𝛽𝑖 𝑗 are sampled from {−𝑀, . . . , 𝑀 } \ {0} and the conditional variances are sampled from {1, . . . , 2𝑀 }, with 𝑀 ∈ N \ {0}. All subsequent operations are then evaluated using exact rational arithmetic. To apply Theorem G.2, we need to bound the degree of the polynomial obtained from the difference between the candidate and target mean or covariance entries, after clearing denominators. 35
This degree depends on the operations used to evaluate the candidate formula, so we introduce the notion of evaluation length. We say that 𝜙 has evaluation length at most 𝑐 if, for all 𝜃 ∈ Θ and t ∈ XT , each scalar entry of 𝜇 𝜙 (𝜃, t) and Σ 𝜙 (𝜃) can be obtained from 𝜇full (𝜃) and Σfull (𝜃) using at most 𝑐 primitive operations. Here, the evaluation length is not the number of terms appearing in the displayed formula 𝜙. Rather, the marginalizations, conditionals, products, and quotients appearing in 𝜙 are translated into operations on Gaussian means and covariances. For each scalar entry of the resulting mean and covariance, the evaluation length counts the operations needed to compute the entry. Each scalar addition, subtraction, multiplication, or division is counted as one primitive operation. Even though Gaussian marginalization and conditioning act on vectors and matrices, we count them as primitive operations as well, and account for their effect on the degrees of the resulting scalar rational expressions. Primitive operations contribute separately to the bound below, proven in Appendix E.4. Theorem G.3 (Bound on false acceptance of non-identifying formulas). Suppose that the evaluation length of 𝜙 is at most 𝑐, and that 𝜙 is non-identifying relative to PΘ (XV ), that is, there exist 𝜃 ∗ ∈ Θ and t∗ ∈ XT such that the equality ⟦𝜙⟧( 𝑝 𝜃 ∗ ,O , t∗ ) = 𝑝 𝜃 ∗ ,Y|do(T=t∗ ) 𝜇Y -almost everywhere does not hold. Let 𝜃 ′ be the vector that collects all sampled parameters. Then, the probability that the falsifier accepts 𝜙 at the sampled parameter 𝜃 ′ satisfies Î𝑐 𝛾𝑙 (2𝑛 − 1) 1 + 𝑙=1 P ∀t ∈ XT , ⟦𝜙⟧( 𝑝 𝜃 ′ ,O , t) = 𝑝 𝜃 ′ ,Y|do(T=t) 𝜇Y -a.e. ≤ , (G.7) min1≤𝑖 ≤𝑑 | 𝐴𝑖 | where, for all 𝑙 ∈ {1, . . . , 𝑐}, 1, 𝛾𝑙 := 2, 𝑛 + 1,
if operation 𝑙 is Gaussian marginalization, if operation 𝑙 is scalar addition, subtraction, multiplication or division, if operation 𝑙 is Gaussian conditioning.
(G.8)
By the non-identification premise, there is at least one non-zero scalar entry in 𝜇 𝜙 (𝜃 ∗ , t∗ ) − 𝜇do (𝜃 ∗ , t∗ ) or Σ 𝜙 (𝜃 ∗ ) − Σdo (𝜃 ∗ ). There may be several such entries, and the implementation compares all covariance entries and all mean entries at |T| + 1 intervention values. However, for the probability bound, one non-zero discrepancy is enough. Fix one such discrepancy. If the falsifier accepts, then all checked discrepancies vanish at the sampled parameter value; in particular, this fixed discrepancy must also vanish at the sampled parameter value. Therefore, the proof of Theorem G.3 uses that the false-acceptance event is contained in the event that one non-zero polynomial, obtained from this fixed discrepancy after clearing denominators, evaluates to zero. The following example shows how an observational formula is translated into operations on the Gaussian mean and covariance, and how these operations determine the resulting false-acceptance bound. Example G.4 (Computing the bound for the front-door formula). Fix 𝜃 ∈ Θ and t ∈ XT , and consider the front-door formula ∫ ∫ 𝑝 𝜃 ,Z|T (z | t) 𝑝 𝜃 ,Y|T,Z (y | t′ , z) 𝑝 𝜃 ,T (t′ ) dt′ dz, where all distributions are Gaussian. We count the primitive operations needed to compute one scalar entry of the covariance matrix returned by this formula, and then show that the same bound also controls the mean entries. We use this count to compute the bound in Equation (G.7). 36
We first translate the front-door formula into the corresponding Gaussian distribution. Let −1 = [ Γ W := (T, Z) and define ΓYW := ΣYW ΣWW YT ΓYZ ], where ΓYT and ΓYZ are the blocks of the regression coefficient of Y on the joint vector (T, Z) corresponding to T and Z, respectively. Therefore, for all t′ ∈ XT and z ∈ XZ , 𝑝 𝜃 ,Y|T,Z (y | t′ , z) = N (𝜇Y + ΓYW (w − 𝜇w ), ΣY|W ) = N (𝜇Y + ΓYT (t′ − 𝜇T ) + ΓYZ (z − 𝜇z ), ΣY|T,Z ). We use the following Gaussian affine-integration identity. For all 𝑟, 𝑠 ∈ N, all 𝑎 ∈ R𝑟 , 𝐵 ∈ R𝑟 ×𝑠 , 𝑚 ∈ R𝑠 , all positive definite 𝑆 ∈ R𝑟 ×𝑟 and 𝑉 ∈ R𝑠×𝑠 , and all y ∈ R𝑟 , ∫ N (y; 𝑎 + 𝐵x, 𝑆)N (x; 𝑚, 𝑉) 𝑑x = N (y; 𝑎 + 𝐵𝑚, 𝑆 + 𝐵𝑉 𝐵⊤ ). R𝑠
Since 𝑝 𝜃 ,T (t′ ) = N (𝜇T , ΣTT ), applying this identity to the inner integral gives, for all z ∈ XZ , ∫ ⊤ 𝑝 𝜃 ,Y|T,Z (y | t′ , z) 𝑝 𝜃 ,T (t′ ) dt′ = N 𝜇Y + ΓYZ (z − 𝜇Z ), ΣY|T,Z + ΓYT ΣTT ΓYT . We now evaluate the outer integral. Since 𝑝 𝜃 ,Z|T (z | t) = N 𝜇Z + ΓZT (t − 𝜇T ), ΣZ|T ,
−1 , ΓZT := ΣZT ΣTT
applying the same affine-integration identity to the outer integral gives ⟦𝜙Zfd ⟧( 𝑝 𝜃 ,O , t) = N (𝜇fd (𝜃, t), Σfd (𝜃)), where 𝜇fd (𝜃, t) = 𝜇Y + ΓYZ ΓZT (t − 𝜇T ), ⊤ ⊤ Σfd (𝜃) = ΣY|T,Z + ΓYT ΣTT ΓYT + ΓYZ ΣZ|T ΓYZ .
We now count the primitive operations needed to compute one scalar entry of Σfd (𝜃). Let 𝜏 := |T| and 𝜁 := |Z|. For all 𝑖, 𝑗 ∈ {1, . . . , |Y|}, let 𝑎 𝑖 and 𝑎𝑗 be the 𝑖-th and 𝑗-th rows of ΓYT , and let 𝑏 𝑖 and 𝑏𝑗 be the 𝑖-th and 𝑗-th rows of ΓYZ . Then ⊤ Σ𝑖fd𝑗 (𝜃) = (ΣY|T,Z )𝑖 𝑗 + 𝑎 ⊤ 𝑖 ΣTT 𝑎 𝑗 + 𝑏 𝑖 ΣZ|T 𝑏 𝑗 .
For 𝑟 ∈ N, a scalar bilinear form 𝑢 ⊤ 𝑀𝑣, with 𝑢, 𝑣 ∈ R𝑟 and 𝑀 ∈ R𝑟 ×𝑟 , can be computed by first computing 𝑀𝑣 and then multiplying by 𝑢 ⊤ . Computing 𝑀𝑣 requires 𝑟 2 scalar multiplications and 𝑟 (𝑟 − 1) scalar additions. Multiplying the result by 𝑢 ⊤ requires 𝑟 scalar multiplications and 𝑟 − 1 scalar additions. Hence one such bilinear form requires 𝑟 2 + 𝑟 (𝑟 − 1) + 𝑟 + (𝑟 − 1) = 2𝑟 2 + 𝑟 − 1 2 scalar primitive operations. Therefore, for all 𝑖, 𝑗 ∈ {1, . . . , |Y|}, the term 𝑎 ⊤ 𝑖 ΣTT 𝑎 𝑗 requires 2𝜏 +𝜏−1 ⊤ 2 scalar primitive operations, and the term 𝑏 𝑖 ΣZ|T 𝑏𝑗 requires 2𝜁 + 𝜁 − 1 scalar primitive operations. Adding the three scalar terms in Σ𝑖fd𝑗 (𝜃) requires two additional scalar additions. Thus, after the two
37
Gaussian conditioning operations used to obtain ΣY|T,Z and ΣZ|T , the number of scalar primitive operations, also accounting for the final 2 additions, needed for one covariance entry is (2𝜏 2 + 𝜏 − 1) + (2𝜁 2 + 𝜁 − 1) + 2 = 2𝜏 2 + 𝜏 + 2𝜁 2 + 𝜁 . We now turn to the primitive operations needed to compute one mean entry. For all 𝑖 ∈ {1, . . . , |Y|}, let 𝑏 𝑖 be the 𝑖-th row of ΓYZ . Then 𝜇𝑖fd (𝜃, t) = 𝜇Y,𝑖 + 𝑏 ⊤ 𝑖 ΓZT (t − 𝜇T ). Computing t − 𝜇T requires 𝜏 scalar subtractions. Multiplying this vector by ΓZT requires 𝜁 𝜏 scalar multiplications and 𝜁 (𝜏 − 1) scalar additions. Multiplying the result by 𝑏 ⊤ 𝑖 requires 𝜁 scalar multiplications and 𝜁 − 1 scalar additions, and adding 𝜇Y,𝑖 requires one additional scalar addition. Hence one mean entry requires 𝜏 + 𝜁 𝜏 + 𝜁 (𝜏 − 1) + 𝜁 + (𝜁 − 1) + 1 = 𝜏 + 2𝜁 𝜏 + 𝜁 scalar primitive operations. Since 𝜏 + 2𝜁 𝜏 + 𝜁 ≤ 2𝜏 2 + 𝜏 + 2𝜁 2 + 𝜁, the covariance-entry count also upper bounds the number of scalar operations needed to compute one mean entry. By Equation (G.8), each primitive operation contributes a multiplicative factor describing how much it can increase the current degree bound. Gaussian marginalizations contribute a factor 1, the two Gaussian conditioning operations contribute factors 𝑛 + 1 each, and each scalar operation contributes factor 2. Thus, for both the covariance and mean entries of the front-door formula, 𝑐 Ö 2 2 𝛾𝑙 ≤ (𝑛 + 1) 2 2 2𝜏 +𝜏+2𝜁 +𝜁 . 𝑙=1
If 𝜏 = 𝜁 = 1, 𝑛 = 10 and min1≤𝑖 ≤𝑑 | 𝐴𝑖 | = 264 − 1, the upper bound in Equation (G.7) then is approximately 7.98 × 10−15 . The bound in Equation (G.7) is valid for the Gaussian parametrization using mean vector and covariance matrix. Other parametrizations can lead to different bounds, because the primitive operations may have different algebraic cost. For example, in canonical form, one represents a Gaussian by its precision matrix and information vector. In this parametrization, conditioning is comparatively cheap, while marginalization is more expensive. We can reduce the bound in Equation (G.7) by increasing the cardinalities of the sampling sets. This is possible with arbitrary precision integer sampling, but it may increase the cost of exact arithmetic, because larger sampled integers can lead to rational computations with larger bit lengths. In our examples, we did not observe a substantial slowdown, but we also provide a floating-point implementation for cases in which exact evaluation becomes computationally expensive. The bound can also be reduced by repeating the test independently. Let 𝛿 be this bound, truncated at 1. Then one run falsely accepts a non-identifying formula with probability at most 𝛿, and 𝐾 independent repetitions falsely accept it in all runs with probability at most 𝛿 𝐾 .
Appendix H. The front-door criterion The front-door criterion (Pearl, 1995a, Section 3.2) gives graphical conditions under which a candidate set Z ⊆ O \ (T ⊔ Y) allows to identify Y | do(T) with the corresponding front-door formula: ∑︁ ∑︁ 𝑝(z | t) 𝑝(y | t′ , z) 𝑝(t′ ). (H.9) z
t′
38
In particular, a set of variables Z satisfies the front-door criterion if: (i) Z intercepts all directed paths from T to Y; (ii) there is no unblocked back-door path from T to Z; (iii) all back-door paths from Z to Y are blocked by T. Whenever these conditions hold, the corresponding front-door formula is identifying for Y | do(T). H.1 Identification by a front-door formula with a set not satisfying the front-door criterion Consider the acyclic directed mixed graph in Figure 2. We show that, even though {𝑀, 𝐴} does not satisfy the front-door criterion, the corresponding front-door formula ∑︁ ∑︁ 𝜙{fd𝑀, 𝐴} = 𝑝(𝑚, 𝑎 | 𝑡) 𝑝(𝑦 | 𝑡 ′ , 𝑚, 𝑎) 𝑝(𝑡 ′ ) 𝑡′
𝑚,𝑎
is identifying for 𝑌 | do(𝑇) in the corresponding canonical directed acyclic graph, obtained by replacing the bidirected edge with a node 𝑈 such that 𝑇 ← 𝑈 → 𝑌 . The same holds for {𝑀, 𝐶} and the proof is analogous. By the truncated factorization formula (Pearl, 2009, Section 1.3), ∑︁ 𝑝(𝑦 | do(𝑡)) = 𝑝(𝑢) 𝑝(𝑏) 𝑝(𝑚 | 𝑡) 𝑝(𝑎 | 𝑏) 𝑝(𝑐 | 𝑏) 𝑝(𝑦 | 𝑚, 𝑎, 𝑐, 𝑢). 𝑚,𝑎,𝑢,𝑏,𝑐
Since 𝑀 and 𝐴 are 𝑑-separated by 𝑇 and 𝐴 and 𝑇 are 𝑑-separated by the empty set, 𝑝(𝑚, 𝑎 | 𝑡) = 𝑝(𝑚 | 𝑡) 𝑝(𝑎 | 𝑡) = 𝑝(𝑚 | 𝑡) 𝑝(𝑎). Moreover, ∑︁ ∑︁ ∑︁ 𝑝(𝑦 | 𝑡 ′ , 𝑚, 𝑎) 𝑝(𝑡 ′ ) = 𝑝(𝑦, 𝑢, 𝑏, 𝑐 | 𝑡 ′ , 𝑚, 𝑎) 𝑝(𝑡 ′ ) 𝑡′
𝑡 ′ 𝑢,𝑏,𝑐
=
∑︁ ∑︁
𝑝(𝑦 | 𝑡 ′ , 𝑚, 𝑎, 𝑢, 𝑏, 𝑐) 𝑝(𝑢, 𝑏, 𝑐 | 𝑡 ′ , 𝑚, 𝑎) 𝑝(𝑡 ′ )
𝑡 ′ 𝑢,𝑏,𝑐
∑︁ ∑︁ 𝑝(𝑢) 𝑝(𝑏) 𝑝(𝑡 ′ | 𝑢) 𝑝(𝑚 | 𝑡 ′ ) 𝑝(𝑎 | 𝑏) 𝑝(𝑐 | 𝑏) (1) = 𝑝(𝑦 | 𝑚, 𝑎, 𝑢, 𝑐) 𝑝(𝑡 ′ ) ′ ) 𝑝(𝑚 | 𝑡 ′ ) 𝑝(𝑎) 𝑝(𝑡 𝑡 ′ 𝑢,𝑏,𝑐
=
∑︁ ∑︁
𝑝(𝑦 | 𝑚, 𝑎, 𝑢, 𝑐) 𝑝(𝑢) 𝑝(𝑡 ′ | 𝑢) 𝑝(𝑏)
𝑡 ′ 𝑢,𝑏,𝑐
𝑝(𝑎 | 𝑏) 𝑝(𝑐 | 𝑏) 𝑝(𝑎)
∑︁ (2) = 𝑝(𝑦 | 𝑚, 𝑎, 𝑢, 𝑐) 𝑝(𝑢) 𝑝(𝑏 | 𝑎) 𝑝(𝑐 | 𝑏), 𝑢,𝑏,𝑐
where in (1) we used that 𝑌 is 𝑑-separated from 𝑇 and 𝐵 given {𝑀, 𝐴, 𝑈, 𝐶}, and in (2) we used Í that, for all 𝑢, 𝑡 ′ 𝑝(𝑡 ′ | 𝑢) = 1 and 𝑝(𝑏) 𝑝(𝑎 | 𝑏)/𝑝(𝑎) = 𝑝(𝑏 | 𝑎). Therefore, ∑︁ 𝜙{fd𝑀, 𝐴} = 𝑝(𝑚 | 𝑡) 𝑝(𝑎) 𝑝(𝑦 | 𝑚, 𝑎, 𝑢, 𝑐) 𝑝(𝑢) 𝑝(𝑏 | 𝑎) 𝑝(𝑐 | 𝑏) 𝑚,𝑎,𝑢,𝑏,𝑐 (3)
=
∑︁
𝑝(𝑚 | 𝑡) 𝑝(𝑢) 𝑝(𝑏) 𝑝(𝑎 | 𝑏) 𝑝(𝑐 | 𝑏) 𝑝(𝑦 | 𝑚, 𝑎, 𝑢, 𝑐)
𝑚,𝑎,𝑢,𝑏,𝑐
= 𝑝(𝑦 | do(𝑡)), 39
where in (3) we used that 𝑝(𝑎) 𝑝(𝑏 | 𝑎) = 𝑝(𝑏) 𝑝(𝑎 | 𝑏).
Appendix I. Recovering all identifying formulas in a finite class fd . The The gateway test described in Section 5 is sound and exhaustively complete relative to ΦY,T underlying idea applies more generally to any finite class of candidate observational formulas: enumerate the formulas, verify each one, and return exactly those that are verified to be identifying eY,T ⊆ ΦY,T be a finite class of observational formulas. Each for Y | do(T). More precisely, let Φ eY,T is verified in turn, and passes the test if it is verified as identifying. With an exact verifier, 𝜙∈Φ eY,T . If one instead uses the falsifier this procedure returns all and only the identifying formulas in Φ from Section 4, then the procedure is almost-surely sound while it is exhaustively complete relative eY,T for the conditional exponential family chosen in the falsification routine. to Φ eY,T may therefore be Graphical criteria that are sound and exhaustively complete relative to Φ viewed as algorithmic shortcuts to this exhaustive procedure. However, this procedure remains applicable even when the graphical criterion is sound but not complete with respect to the formula class (as is the case for the front-door criterion with respect to the class of front-door formulas; see Section 5), or when no such graphical criterion is available. For instance, as discussed in Appendix C, adj sound and exhaustively complete graphical criteria relative to the class of adjustment formulas ΦY,T defined in Equation (C.2) are available for directed acyclic graphs, maximal ancestral graphs, or their equivalence classes. For acyclic directed mixed graphs, however, no graphical criterion is currently adj known to be both sound and exhaustively complete relative to ΦY,T . Verification enables us to fill this gap.
40