Paper deep dive
Verifying formulas for interventional distributions
Francesco Freni, Leonard Henckel, Sebastian Weichwald
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 92%
Last extracted: 7/18/2026, 10:30:22 AM
Summary
The paper formalizes the problem of verification in causal graphical models, which involves deciding whether a given observational formula correctly identifies a target interventional distribution. It demonstrates that existing sound and complete identification algorithms (like ID) do not solve verification, as they only guarantee the existence of some identifying formula, not the correctness of a specific candidate. The authors propose a falsification-based approach, proving that for regular exponential-family models, sampling from compatible distributions can induce an almost-surely correct verifier. This leads to the development of the 'gateway test' for finding admissible sets in front-door formulas.
Entities (9)
Relation Signals (6)
verification โ complements โ Identification
confidence 95% ยท This opens a problem complementary to identification, asking not whether any identifying formula exists, but whether the given formula is identifying.
ID Algorithm โ failstosolve โ verification
confidence 92% ยท We show that even sound and complete solutions to identification do not solve verification. ... 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.
do-calculus โ failstosolve โ verification
confidence 90% ยท 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
Falsifier โ induces โ Verifier
confidence 90% ยท We propose a falsifier as a first practical route forward, prove that it induces an almost-surely correct verifier for regular exponential-family models
Gateway Test โ findssetsfor โ Front-door formula
confidence 88% ยท gateway test, which finds all sets admissible for use in a front-door formula.
Gateway Test โ uses โ Verifier
confidence 88% ยท use the resulting verifier to develop the gateway test, which finds all sets admissible for use in a front-door formula.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
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.
Tags
Links
- Source: https://arxiv.org/abs/2607.13883v1
- Canonical: https://arxiv.org/abs/2607.13883v1
Trouble viewing inline? Open PDF directly โ
Full Text
115,717 characters extracted from source content.
Expand or collapse full text
Verifying formulas for interventional distributions Francesco Freni 1 and Leonard Henckel 2,* and Sebastian Weichwald 1,* 1 Department of Mathematical Sciences, University of Copenhagen, Denmark 2 School of Mathematics and Statistics, University College Dublin, Ireland * Equal contribution. 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 arXiv:2607.13883v1 [stat.ME] 15 Jul 2026 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, letGbe a causal directed acyclic graph overV = Oโ L, with observed variablesO, latent variablesL, and disjoint outcome and intervention node setsY, Tโ O. LetG ํ be the latent projection ofGontoO(Verma and Pearl, 1990; Richardson, 2003), and letA(O)denote the class of latent projections (or acyclic directed mixed graphs) over O. ForA โ V, set the product sample spaceX A = ร ํโA X ํ and letํ A be the corresponding product measure. All distributions considered admit densities with respect to the relevantํ A , and P(X A )denotes the class of such densities. A densityํ โ P(X V )factorizes according toGif there exist conditional densitiesํ ํ|pa(ํ) : ํ โ V, such thatํ(v) = ร ํโV ํ ํ|pa(ํ) (v ํ | v pa(ํ) )for ํ V -almost every v. LetP G (X V ) denote the class of such full densities. The causal directed acyclic graphG, together with this factorization and truncated factorizations for interventions, specifies a non-parametric causal graphical model: eachํ โ P G (X V )induces a marginal observational densityํ O and a family of interventional densities; fort โ X T , 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ํforYunder intervention on Tis a well-typed, kernel-preserving symbolic expression with no free variables other thanyand 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(X O )รX T โP(X Y ) 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 sym- bol 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 overX ํ and are integrated with respect to ํ ํ . Definition 2.2(Identifying formula). An observational formulaํis identifying forY | do(T)in G if, for every ํ โ P G (X V ) and every tโX T for whichโฆํโง(ํ O , t) is defined, โฆํโง(ํ O , t) = ํ Y|do(T=t) ํ Y -almost everywhere.(1) We say thatํis identifying forY | do(T)inGrelative to e P G (X V ) โ P G (X V )if the above equality holds for every ํ โ e P G (X V ) and every tโX T . 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ํฆ โฆโ โซ ํ ํ|ํ,ํ (ํฆ | ํก,ํฅ)ํ ํ (ํฅ) ํํ ํ (ํฅ)onX ํ . 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 forY | do(T)in G ํ if and only if it is identifying in any, equivalently every, full graphGwhose latent projection ontoOisG ํ (Richardson et al., 2023, Corollary 49). ForH โ G,G ํ , we say thatY | do(T)is identifiable inH if and only if there exists ํ โ ฮฆ Y,T that is identifying for Y | do(T) inH. Identification asks whetherY | do(T)is identifiable and, when it is, provides an identifying formula forY | do(T). We view an identification procedureIwith associated, possibly restricted, formula classฮฆ I Y,T โ ฮฆ Y,T abstractly as assigning to each latent projectionG ํ โ A(O)and disjoint node setsY, T โ O, a set of formulasI(G ํ , Y, T) โ ฮฆ I Y,T . The procedure is sound (for identification) if eachํ โI(G ํ , Y, T)is identifying forY | do(T). The procedure is complete (for identification) if it returns at least one identifying formula wheneverY | do(T)is identifiable inG ํ . The procedure is exhaustively complete relative toฮฆ I Y,T if it is complete for finding all identifying formulas inฮฆ I Y,T , that is, for everyํ โ ฮฆ I Y,T , ifํis identifying forY | do(T), thenํ โI(G ํ , Y, T). 3 G 1 ํํํ ํถ ID output: ํ 1 = ร ํ ํ(ํฆ | ํก,ํ) ํ(ํ) G 2 ํํํ ํถ ID output: ํ 2 = ํ(ํฆ | ํก) Identifying in both graphs: ํ 3 = ร ํ ํ(ํ | ํก) ร ํก โฒ ํ(ํฆ | ํก โฒ ,ํ) ํ(ํก โฒ ) Figure 1: The ID algorithm returns one identifying formula forY | do(T)when one exists; here, the adjustment formulaํ 1 inG 1 and the conditional densityํ 2 inG 2 . Each formula is specific to its graph and fails in the other:V(G 1 ,ํ,ํ, ํ 2 ) = falseandV(G 2 ,ํ,ํ, ํ 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 targetY | 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 verifierVis 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 setsY, T โ O, and either an observational formulaํ โ ฮฆ Y,T or the symbolnone. LetGbe any latent-variable causal directed acyclic graph whose latent projection onto O isG ํ . The verifier returns true if and only if one of the following holds: 1. ํ โ ฮฆ Y,T and ํ is identifying for Y | do(T) inG; or 2. ํ = none and Y | do(T) is not identifiable inG. 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 procedureIthat is sound and exhaustively complete relative to a formula classฮฆ I Y,T , such as adjustment formulas (see Appendix C), may be repurposed for verification by checking whether a formula belongs toI(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 inI(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 letL 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 in the languageL do-calc and in the subclassฮฆ do-calc Y,T โ L do-calc of strings representing observational formulas forYunder intervention onTis decidable, in the sense that there is an algorithm that halts on every input and correctly determines membership. For simplicity, we takeRto 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ํ โ Nfrom 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 inR. The next expressionํ ํ is obtained fromํ ํโ1 by replacing the selected occurrence ofํ ํ withํ ํ . The derivation is valid relative toG ํ if all steps are well-formed and all graph-dependent side conditions of the applied rules hold inG ํ . Given a candidate observational formulaํ โ ฮฆ do-calc Y,T , a derivationํ ํ derivesํfromํ 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 graphG 1 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 ํ ํ,ํ inG 1 . Letํท ํ be the set of all length-ํderivations, and considerํ Y,T : = ํ(y | do(t))as starting query expression. LetCheck(ํบ ํ ,ํ Y,T , ํ, ํ ํ )be an algorithm taking as input the graphG ํ and query ํ Y,T , an observational formulaํ โ ฮฆ do-calc Y,T , and a derivationํ ํ โ ํท ํ ;Checkreturnstrueifํ ํ is a valid derivation relative toG ํ 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 I do-calc (G ํ , Y, T) =ํ โ ฮฆ do-calc Y,T | โํ โ N, ํ ํ โ ํท ํ : Check(G ํ ,ํ Y,T , ํ, ํ ํ ) = true, which formally defines a language overฮฃas well as a sound and complete identification procedure. This do-calculus-based identification procedure may even be exhaustively complete relative toฮฆ do-calc Y,T . Nevertheless, this does not by itself provide a verifier for arbitrary candidate formulas, because membership in the derivable setI 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 derivations and halts once it finds one that derives a givenํ โ ฮฆ do-calc Y,T ; if none exists, the search continues forever. Example 3.5(Non-terminating derivation search). Consider the graphG 2 in Figure 1 and the queryํ ํ,ํ = ํ(ํฆ | do(ํก)). To see that the adjustment formulaํ 1 is not identifying forํ | do(ํ) inG 2 , we provide a counterexample for which the formula and the target disagree. Consider the Gaussian densityํthat factorizes according toG 2 withํ โผ N(0, 1),ํ | ํ = ํก โผ N(ํก, 1), ํ | ํ = ํ โผ N(ํ, 1), andํถ | ํ = ํก,ํ = ํฆ โผ N(ํก+ ํฆ, 1). Underdo(ํ = 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 โง(ํ, 1)(ํฆ) =N ํฆ;โ 1 3 , 34 9 โ N(ํฆ; 1, 2) = ํ ํ|do(ํ=1) (ํฆ). We explain what happens if one tries to verifyํ 1 by derivation search. For allํ โ Nand all ํ ํ โ ํท ํ ,Check(G 2 ,ํ ํ,ํ , ํ 1 , ํ ํ ) = false, because otherwise, by soundness ofR,ํ 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ํ ํ ํโฮ : =ํ ํ ํ (ํฃ | v pa(ํ) ) ํ ํ โฮ ํ ํโV of densities factor- izing according toG, 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 writeP ฮ (X V ) โ P G (X V )for the parametric submodel induced by this family. Then, a falsifier is defined as follows. Definition 4.1(Falsifier).A falsifierFis 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 setsY, T โ O, and either an observational formulaํ โ ฮฆ Y,T or the symbolnone. LetGbe any latent-variable causal directed acyclic graph whose latent projection ontoOisG ํ , and consider a parametric familyํ ํ ํโฮ of densities factorizing according toG. 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โX T , โฆํโง(ํ ํ ํ ,O , t) = ํ ํ ํ ,Y|do(T=t) ํ Y -almost everywhere; or 2. ํ = none and Y | do(T) is not identifiable inG. Otherwise,F returns false. We say that a falsifier is an almost-surely correct verifier relative toP ฮ (X V )if, with probability one over the sampled parameters, it returnstrueexactly when eitherํ โ ฮฆ Y,T is identifying for Y | do(T) inG relative toP ฮ (X V ), or ํ = none and Y | do(T) is not identifiable inG. Whenํisnone(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 valuest โ X T . 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 intand covariance independent oft, and for fixed parameters, task (b) reduces to comparing the covariance matrices and comparing the mean functions at|T|+ 1affinely independent intervention values. Example 4.2(Falsification in a Gaussian model).Consider the acyclic directed mixed graphG ํ : ํ โ ํถ โ ํ and the queryํ ํ,ํ = ํ(ํฆ | do(ํก)). For parametric falsification, consider the canonical directed acyclic graphG : ํ โ ํถ โ ํฟ โ ํ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 interventiondo(ํ = ํก), 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 โฆํ 1 โง(ํ ํ ,ํก)(ํฆ) =N ํฆ; ํ ํํ ํฃ ํ ํก, ํฃ ํ โ ํ 2 ํํ ํฃ ํ ! . 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, marginal- ization gives the second, and marginalizing their product over ํ gives โฆํ 2 โง(ํ ํ ,ํก)(ํฆ) =N ํฆ; ํ ํํ ํโ ํ ํํถ ํ ํํถ ฮ ํก, ํฃ ํ โ ํ 2 ํํ ํโ 2ํ ํํ ํ ํํถ ํ ํํถ + ํ 2 ํํถ ํฃ ํ ฮ + โํ ํํ ํ ํํถ + ํ ํํถ ํฃ ํ ฮ 2 ํ ! . Symbolic simplification reduces the displayed mean to0and 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|ํ| = 1here, 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 toP ฮ (X V ), 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); (i)ํis identifying relative to P ฮ (X V ). 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 toGis said to admit a conditional exponential-family parametrization if, for all ํ โ V and ํ ํ โ ฮ ํ , ํ ํ ํ (ํฃ | v pa(ํ) ) = ํ ํ (ํฃ, v pa(ํ) ) ํ ํ ํ (ํ ํ ) โค ํ ํ (ํฃ,v pa(ํ) )โํด ํ ( ํ ํ (ํ ํ ),v pa(ํ) ) , whereํ ํ : X ํ รX pa(ํ) โ [0,โ)is a non-negative function,ํ ํ : ฮ ํ โ R ํ ํ is the natu- ral parameter, andํ ํ : X ํ รX pa(ํ) โ R ํ ํ is the sufficient statistic, withํ ํ โ N. For all ํ โ V,ํ ํ โ ฮ ํ andv pa(ํ) โ X pa(ํ) ,ํด ํ (ํ ํ (ํ ํ ), v pa(ํ) ) < โ, whereํด ํ (ํ ํ (ํ ํ ), v pa(ํ) ) : = log โซ X ํ ํ ํ (ํฃ, v pa(ํ) )ํ ํ ํ (ํ ํ ) โค ํ ํ (ํฃ,v pa(ํ) ) dํ ํ (ํฃ) is the normalizer. Given a conditional exponential-family parametrizationํ ํ ํโฮ of densities factorizing according toGand 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 con- nected. Assumption 4.5(Analyticity of the natural parameters).For allํ โ V, the mapํ ํ โฆโ ํ ํ (ํ ํ ) is analytic with open image ํ ํ (ฮ ํ ). Assumption 4.6(Regularity).For allt โ X T ,ํ ํ,X|do(T=t) (x) ํโฮ , whereX = V\ T, form a regular exponential family. Regularity implies that, for allํ โ ฮand allt โX T ,ํ ํ,X|do(T=t) (x) โ e ํ t (x)ํ eํ t (ํ) โค eํ t (x) , where e ํ t :X X โ [0,โ) ,eํ t : ฮโ R ํ t , andeํ t :X X โ R ํ t , withํ t โ N, are such that the parametrization is minimal, full, andeํ t (ฮ)is open (Barndorff-Nielsen, 2014, p. 116). Here, minimality refers to affine independence of the components ofeํ t andํ x -almost sure affine independence of the components ofeํ t , while fullness means thateํ t (ฮ) = ํพ t โ R ํ t : โซ e ํ t (x)ํ ํพ โค t eํ 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ํธ โ X Y of full measure such that, for allyโ ํธand alltโX T , 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โX T as ํ : =ํ โ ฮ : for all tโX T , โฆํโง(ํ ํ,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 ํ โ โ ฮandt โ โ X T 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 parametriza- tions, under Assumptions 4.4โ4.7, the falsifier in Definition 4.1 induces an almost-surely correct verifier relative toP ฮ (X V ). In light of Theorem 4.9,ํพ = 1in Definition 4.1 suffices for almost-sure correctness relative to P ฮ (X V )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 Consider identification relative to the class of front-door formulasฮฆ fd Y,T : = ํ fd Z : = ร z ํ(z | 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 setZsufficient for the corresponding front-door formula to be identifying forY | 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 complete relative toฮฆ fd Y,T : there exist setsZfor whichํ fd Z is identifying forY | do(T)even thoughZ 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 Y,T : it can fail to certify front-door formulas that are identifying nonetheless. Verification allows us to develop the gateway test, a procedure that is sound and exhaustively complete relative toฮฆ fd Y,T . The gateway test enumerates all candidate setsZ โ O\(TโชY), constructs the corresponding front-door formulaํ fd Z โ ฮฆ fd Y,T , and applies the verifier to it. A candidate setZ passes the test if and only ifํ fd Z 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 relative toฮฆ fd Y,T for the conditional exponential family chosen in the falsification routine. The same 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 ฮ (X V )used by the falsifier (Theorem 4.9): if a candidate formula is certified by the falsifier, it is identifying relative toP ฮ (X V )almost surely, but it need not be valid in the full non-parametric graphical modelP G (X V ). Characterizing when correctness relative toP ฮ (X V )transfers to correctness inP G (X V )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 Con- ference 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 Preliminaries17 B A typed, kernel-preserving grammar for observational formulas19 C Verifying adjustment formulas with graphical criteria22 D Do-calculus22 E Proofs23 F Alternative implementation via the nested Markov model33 G Numerical evaluation and exact arithmetic34 H The front-door criterion38 I Recovering all identifying formulas in a finite class40 Appendix A. Preliminaries A.1 Graphical preliminaries A graphG = (V, E)consists of a finite non-empty node setV, whose nodes represent random variables, and an edge setE. 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, ifE โ (ํ ํ ,ํ ํ ) โ Vร V : ํ ํ โ ํ ํ , thenGis 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ํคinGis a sequence of nodesํ 1 ,...,ํ ํ โ Vand 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 setX โ Vto a disjoint setY โ Vis a walk, or path, from someํ โ Xto some ํ โ Y. Such a walk, or path, is proper if only its first node belongs toX. A back-door path from a setX โ Vto a disjoint setY โ Vis a proper path whose first edge has an arrowhead into a node inX. 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 ํ inG. In the latent-variable setting, we writeV = Oโ L, whereOandLdenote the observed and latent variables, respectively. We represent a latent-variable directed acyclic graphGby an acyclic directed 17 mixed graphG ํ obtained via latent projection (Verma and Pearl, 1990; Richardson, 2003), defined as follows. Definition A.1(Richardson et al., 2023, Definition A.2).LetGbe a latent-variable directed acyclic graph with node setV = Oโ L, where nodes inOare observed and nodes inLare unobserved. The latent projection ofGontoOis an acyclic directed mixed graphG ํ where, for all distinct ํ ํ ,ํ ํ โ O: (i) G ํ contains a directed edgeํ ํ โ ํ ํ ifGhas a directed path fromํ ํ toํ ํ whose non-endpoint nodes, if any, all belong to L. (i) G ํ contains a bidirected edgeํ ํ โ ํ ํ ifGhas a path betweenํ ํ andํ ํ such that ํ ํ โ ํฟ 1 โยทโ ํฟ โ โยทโ ํฟ ํ โ ํ ํ , with ํฟ ํ โ L for all ํ โ 1,...,ํ. Given a directed acyclic graphGover nodesV, 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 graphG over nodes V, a walk ํค inG 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 AandBareํ-connected bySif there existํด โ A,ํต โ B, and an open walk fromํดtoํตgivenS. 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 graphGoverV = Oโ Land suppose that all directed edges inGrepresent 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, letX ํ be the sample space ofํ, and letํ ํ be aํ-finite measure onX ํ . Throughout, we consider densities inP G (X V ), that is, densities that factorize according toG(see Section 2). Everyํ โ P G (X V )satisfies the global Markov property with respect toG: for all disjointA, B, S โ V, ifAandBareํ-separated bySinG, thenAandBare conditionally independent given S under ํ. Consider the intervention node setT โ O, and intervention valuestโX T . Under the intervention do(T = t)(or shorthanddo(t)), the variables inTare set tot. LetX : = 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 L ํ(x,โ) dํ L (โ), where ํ(x,โ) = ร ํโV ํ(ํฃ | v pa(ํ) ) T=t , that is, the conditional densities corresponding to the intervened variables are removed from the factorization and the remaining factors are evaluated after substitutingT = 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 projectionG ํ (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 overAgivenB, or equivalently a density representation of a Markov kernel fromX B toX A . This notation is a typing device: it records the output variables of an expression and its conditioning arguments. Base terms. For disjoint setsA, B โ O, observational marginals and conditionals are admissible base terms: ํ(a) : A | โ , ํ(a | b) : A | B. whereํ(a | b)is understood only on the part ofX B 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, letA 1 ,..., A ํ , C โ O, whereA 1 ,..., A ํ are pairwise disjoint and disjoint from C. Suppose the factors can be ordered so that, for all ํ โ 1,..., ํ, ํธ ํ : A ํ | D ํ ,D ํ โ Cโช A 1 โชยทโช 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 ํ ร ํ=1 ํธ ํ : ํ ร ํ=1 A ํ ! | C. 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 variablesAandBconditional on C, that is, ํธ : A, B | C, then, integrating out B leaves a kernel over A, conditional on the same variables C: โ๏ธ b ํธ(a, b | c) : A | C. 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 fixedb,ํธ(a, r | b)denotes a joint density over(A, R). LetM โ A. From the same kernelํธ, form the conditional kernel ofRgiven(M, B), denoted byํธ(r | m, b). Where this conditional is defined, the grammar admits ํธ(a, r | b) ํธ(r | m, b) : A | B, R. Thus, internal conditional division turns a kernel over(A, R)givenBinto a kernel overAgiven (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 kernel- preserving. 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, writeU = A\ Msuch thatA = (U, M)and recall thatํธ(a, r | b)is, for each fixedb, a joint density over(A, R). For everyb, 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ํforYunder intervention onTis an expression generated recursively by the preceding rules, with no free variables other thanyandt, and of type Y | T, which induces the partial functional โฆํโง :P(X O )รX T โP(X Y ). 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 overOis multivariate Gaussian,OโผN(ํ,ฮฃ), withฮฃโป 0. Then every admissible observational formulaํof typeY | Tdenotes, for allt โ X T , a linear Gaussian density overY: 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 Y,T : = ( ํ adj Z : = โ๏ธ z ํ(y | t, z) ํ(z) : Z โ O\(Tโช Y) ) .(C.2) Covariate adjustment asks whether there exists a setZyielding an identifying formula forY | do(T), and graphical criteria for adjustment are conditions on candidate setsZthat certify when the corresponding adjustment formulaํ adj Z is identifying forY | do(T). Different criteria give different guarantees. The back-door criterion (Pearl, 1995a, Section 3.1), for instance, is sound but not exhaustively complete relative toฮฆ adj Y,T . The adjustment criterion (Shpitser et al., 2010, Definition 5) is instead sound and exhaustively complete relative toฮฆ adj 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 toฮฆ adj 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 setZsatisfies the criterion is equivalent to verifying whether the corresponding adjustment formula ํ adj 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 currently known for acyclic directed mixed graphs, one can still enumerate the finite classฮฆ adj 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 classฮฆ adj 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. LetGdenote the underlying latent-variable directed acyclic graph over observed nodesO, 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), ifYandZareํ-separated byT,Win the graph obtained by removing incoming edges intoT; (i) โAction/observation exchangeโ: ํ(y | do(t, z), w) = ํ(y | do(t), z, w), ifYandZareํ-separated byT,Win the graph obtained by removing incoming edges intoT and outgoing edges from Z; (i) โInsertion/deletion of actionsโ: ํ(y | do(t, z), w) = ํ(y | do(t), w), ifYandZareํ-separated byT, Win the graph obtained as follows: first remove all incoming edges into nodes inT; then, in the resulting graph, identify those nodes ofZthat 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 thatI do-calc (G ํ , Y, T)is semi-decidable is equivalent to showing that there exists an algorithmํthat semi-decidesI do-calc (G ํ , Y, T), that is, anํthat halts and accepts for all inputs that are elements ofI 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 length1, then all candidates of length2, 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ร Nbe a computable bijection that mapsํ โ Nto a tuple(ํ,ํ) โ Nร N. The algorithm 23 ํproceeds as follows. Forํ = 0, 1, 2,..., algorithmํcomputesํ(ํ) = (ํ,ํ), sets the derivation ํ ํ,ํ = ํ ํ (ํ), and then runsCheck(G ํ ,ํ Y,T , ํ, ํ ํ,ํ )to check whetherํ ํ,ํ is a valid derivation relative toG ํ that derivesํfromํ Y,T .Checkhalts 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ํ โ โ Nsuch thatํ(ํ โ ) = (ํ โ ,ํ โ ) andํ ํ โ ,ํ โ = ํ ํ โ (ํ โ ) = ํ โ . Whenํreachesํ โ , it runsCheck, accepts and halts. Ifํ โ I do-calc (G ํ , Y, T) , there exists no derivation for whichCheckreturnstrue. In particular, since Checkhalts on every input,ํnever encounters a derivation accepted byCheckand therefore fails to terminate. This shows thatI do-calc (G ํ , Y, T) semi-decidesL 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โX T as ํ : =ํ โ ฮ : for all tโX T , โฆํโง(ํ ํ,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 ํ โ โ ฮandt โ โ X T 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โX T as ํ ํธ : =ํ โ ฮ : for all yโ ํธ and all tโX T , โฆํโง(ํ ํ,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 ally โ ํธand allt โ X T , the real-valued map ํ โฆโ ํ ํ,Y|do(T=t) (y) is analytic on ฮ, we show that ํ ํธ has Lebesgue measure zero; (i) Using (i), we show that ํ has Lebesgue measure zero; (i) Using Assumptions 4.4โ4.6, we show that, for allyโX Y and alltโX T , 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 โ โX T 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 โ (ํ โ ) โ 0and 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 (i), since the difference of analytic functions is analytic, the real-valued map ํ โฆโ ํ t โ (ํ) is analytic on ฮ as well. Defineํ t โ ,y โ ํธ : = ํ โ ฮ : ํ t โ (ํ) = 0. Then,ํ ํธ โ ํ t โ ,y โ ํธ . 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 open and connected,ฮ = ร ํโV ฮ ํ is open and connected as well. Therefore,ํ t โ ,y โ ํธ , and henceํ ํธ , has Lebesgue measure zero. This completes the proof of (i). Proof of (i). Letํ โ โ ฮandt โ โX T be the witnesses from the premise. For allํ โ ฮandyโ ํธ, 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 ally โ ํธ, by Assumption 4.7, and if the real-valued mapํ โฆโ ํ ํ,Y|do(T=t โ ) (y)is analytic onฮ(shown in the proof of (i)), 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โX Y :โฆํโง(ํ ํ,O , t โ )(y) โ ํ ํ,Y|do(T=t โ ) (y) = yโX Y : ํ 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 (ํท ํ ) = 0if 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 alltโX T ,ํ โ ํ 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 = โซ ํ t โ ํ Y ( yโ ํธ : ํ t โ (ํ, y) โ 0 ) dํ(ํ) = โซ ํ t โ โซ ํธ 1 ํ t โ (ํ,y)โ 0 dํ Y (y)dํ(ํ) = โซ ํธ โซ ํ t โ 1 ํ t โ (ํ,y)โ 0 dํ(ํ)dํ Y (y). 25 Since the integrand is nonnegative, it follows that, forํ Y -almost everyyโ ํธ,ํ(ํ โ ํ t โ : ํ t โ (ํ, y) โ 0) = 0. Therefore, ํ(ํ โ ํ t โ : ํ t โ (ํ, y) = 0) = ํ(ํ t โ ) > 0, which means that, forํ Y -almost everyy โ ํธ, 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 everyy โ ํธ,ํ t โ (ยท, y) โก 0onฮ, 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 (i). Proof of (i). We now show that, under Assumptions 4.4โ4.6, for ally โ X Y and allt โ X T , the real-valued mapํ โฆโ ํ ํ,Y|do(T=t) (y)is analytic onฮ, which yields the premise of (i) and, via (i) and (i), concludes the proof of Proposition 4.8. Fix an arbitrarytโX T . By the truncated factorization formula (Pearl, 2009, Section 1.3), for all ํ โ ฮandyโX Y , the interventional density isํ ํ,Y|do(T=t) (y) = โซ X W ํ ํ,(Y,W)|do(T=t) (y, w)dํ W (w), with ํ ํ,(Y,W)|do(T=t) (y, w) = ร ํโV ํ ํ ํ (ํฃ | v pa(ํ) ) T=t ,(E.3) where W : = V\(Tโ Y). For ํ โ V, ํ ํ โ ฮ ํ , ํฃ โX ํ , and v pa(ํ) โX pa(ํ) , we define ํ โ ํ (ํฃ, v pa(ํ) , t) : = ํ ํ (ํฃ, v pa(ํ) ) T=t , ํ โ ํ (ํฃ, v pa(ํ) , t) : = ํ ํ (ํฃ, v pa(ํ) ) T=t , and ํด โ ํ (ํ ํ (ํ ํ ), v pa(ํ) , t) : = ํด ํ (ํ ํ (ํ ํ ), v pa(ํ) ) T=t , which are obtained by substituting T = t whenever Tโ pa(ํ) and are such that ํ ํ ํ (ํฃ | v pa(ํ) ) T=t = ํ โ ํ (ํฃ, v pa(ํ) , t)ํ ํ ํ (ํ ํ ) โค ํ โ ํ (ํฃ,v pa(ํ) ,t)โํด โ ํ (ํ ํ (ํ ํ ),v pa(ํ) ,t) . Recall that, by Assumption 4.6, ifX = V\ T, for allํ โ ฮand allt โ X T ,ํ ํ,X|do(T=t) (x) โ e ํ t (x)ํ eํ t (ํ) โค eํ t (x) , where e ํ t ,eํ t , andeํ t are such that the parametrization is minimal, full, andeํ t (ฮ) 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 ํ , andv pa(ํ) โX pa(ํ) , the real-valued mapํ ํ โฆโ ํ ํ ํ (ํฃ | v pa(ํ) ) T=t is analytic on ฮ ํ . (b) For all yโX Y and wโX W , the real-valued map ํ โฆโ ํ ํ,(Y,W)|do(T=t) (y, w) is analytic on ฮ. (c) TheR ํ t -valued natural-parameter mapํ โฆโ eํ t (ํ)associated with the regular exponential family in Assumption 4.6 is analytic on ฮ. (d) For all yโX Y , the real-valued map ํ โฆโ ํ ํ,Y|do(T=t) (y) is analytic on ฮ. After showing the above steps, since tโX T was arbitrary, the result follows. 26 Step (a). Fixํ โ V,ํฃ โ X ํ , andv pa(ํ) โ X pa(ํ) . Letํ ํ : = ํ โ ํ (ยท, v pa(ํ) , t)ํ ํ be a weighted measure onX ํ . Define the measureํ ํ onR ํ ํ as the pushforward ofํ ํ under the map ํ โ ํ (ยท, v pa(ํ) , t) :X ํ โ R ํ ํ , that is, ํ ํ : = (ํ โ ํ (ยท, v pa(ํ) , t)) โฏ ํ ํ . Then, for all ํ ํ โ ฮ ํ , ํ ํด โ ํ (ํ ํ (ํ ํ ),v pa(ํ) ,t) = โซ X ํ ํ โ ํ (ํฃ, v pa(ํ) , t)ํ ํ ํ (ํ ํ ) โค ํ โ ํ (ํฃ,v pa(ํ) ,t) dํ ํ (ํฃ) = โซ R ํ ํ ํ ํ ํ (ํ ํ ) โค s dํ ํ (s). LetN ํ : = ํพ ํ โ R ํ ํ : โซ R ํ ํ ํ ํพ โค ํ s dํ ํ (s) < โ and defineํบ ํ : N ํ โ (0,โ)byํพ ํ โฆโ โซ R ํ ํ ํ ํพ โค ํ s dํ ํ (s) . In particular, for allํ ํ โ ฮ ํ ,ํบ ํ (ํ ํ (ํ ํ )) = ํ ํด โ ํ (ํ ํ (ํ ํ ),v pa(ํ) ,t) . Now define T ํ : = ํพ ํ + ํํ ํ : ํพ ํ โ N ํ , ํ ํ โ R ํ ํ and define the complex extension e ํบ ํ : T ํ โ Cby ํง ํ โฆโ โซ R ํ ํ ํ ํง โค ํ s dํ ํ (s). Since, for allํพ ํ โN ํ ,ํ ํ โ R ํ ํ ,ํง ํ = ํพ ํ +ํํ ํ , andsโ R ํ ํ , one has|ํ ํง โค ํ s | = ํ ํพ โค ํ s , e ํบ ํ is the Fourier-Laplace transform of the pushforward measureํ ํ . By Theorem 7.2 of Barndorff-Nielsen (2014), the complex-valued mapํง ํ โฆโ e ํบ ํ (ํง ํ )is analytic on the interiorint(T ํ ). Sinceํ ํ (ฮ ํ )is 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 ํบ ํ (ํ ํ (ํ ํ )) = ํ ํด โ ํ (ํ ํ (ํ ํ ),v pa(ํ) ,t) (E.4) is analytic on ฮ ํ . Since, for all ํ ํ โ ฮ ํ , e ํบ ํ (ํ ํ (ํ ํ )) > 0, its reciprocal is analytic as well. Moreover, sinceํ โ ํ (ํฃ, v pa(ํ) , t)does not depend onํ ํ and the exponential of an analytic function is analytic, it follows that the real-valued map ํ ํ โฆโ ํ ํ ํ (ํ ํ ) โค ํ โ ํ (ํฃ,v pa(ํ) ,t) (E.5) is analytic on ฮ ํ . Therefore, the mapํ ํ โฆโ ํ ํ ํ (ํฃ | v pa(ํ) ) T=t is analytic onฮ ํ since it is the product of the ํ ํ -independent factorํ โ ํ (ํฃ, v pa(ํ) , t) , the analytic function in (E.5), and the reciprocal of the analytic function in (E.4). Sinceํ โ V,ํฃ โX ํ , andv pa(ํ) โX pa(ํ) were arbitrary, this holds for all such values. This proves (a). Step (b). By (E.3), for allyโX Y andwโX W , 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โX X , ํ ํ,X|do(T=t) (x) = e ํ t (x)ํ eํ t (ํ) โค eํ t (x)โ e ํด t ( eํ t (ํ)) . Minimality guarantees the existence ofํ+ 1pointsx 0 ,..., x ํ โX X such that theํdifference vectors u t 1 := eํ t (x 1 )โ eํ t (x 0 ),..., u t ํ := eํ t (x ํ )โ eํ t (x 0 )are linearly independent. For allํ โ ฮandxโX X , taking the logarithm of the density yieldslog ํ ํ (x | do(t)) = log e ํ t (x)+ eํ t (ํ) โค eํ t (x)โ e ํด t (eํ t (ํ)). Thus, for all ํ โ 1,..., ํ, log ํ ํ,X|do(T=t) (x ํ )โ log ํ ํ,X|do(T=t) (x 0 ) = (log e ํ t (x ํ )โ log e ํ t (x 0 ))+ eํ t (ํ) โค (eํ t (x ํ )โ eํ t (x 0 )) =โํถ t ํ +(u t ํ ) โค eํ t (ํ), 27 where ํถ t ํ : =โ log e ํ t (x ํ )+ log e ํ t (x 0 ). We rearrange this to define, for ํ โ 1,..., ํ, โ t ํ (ํ) : = log ํ ํ,X|do(T=t) (x ํ )โ log ํ ํ,X|do(T=t) (x 0 )+ ํถ t ํ = (u t ํ ) โค eํ t (ํ). 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 : = [u t 1 ,..., u t ํ ]be theํ ร ํmatrix whoseํ-th column isu t ํ , for allํ โ 1,..., ํ, and letโ t (ํ) : = (โ t 1 (ํ),..., โ t ํ (ํ)) โค be theํ-dimensional vector whoseํ-th entry isโ t ํ (ํ), for all ํ โ 1,..., ํ. Then, we can writeํ โค t eํ t (ํ) = โ t (ํ). Since the vectorsu t 1 ,..., u t ํ are linearly independent, the matrixํ t (and thereforeํ โค t ) has full rankํ t and is invertible. Multiplying both sides by the inverse yieldseํ t (ํ) = (ํ โค t ) โ1 โ t (ํ). As a linear combination of the analytic components of โ t (ํ), the map ํ โฆโ eํ t (ํ) is analytic on ฮ. The claim in (c) then follows. Step (d). Let A, B be such that Aโ B = V\ T. For all bโX B , the integral eํ t โฆโ โซ X A e ํ t (a, b)ํ eํ โค t eํ t (a,b) dํ A (a) 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 eํ t (ฮ)given by Assumption 4.6, is open and containseํ t (ฮ). Consequently, its restriction to the real parameter space is analytic oneํ t (ฮ). Because the mapํ โฆโ eํ t (ํ)is analytic onฮby (c), for all bโX B , the composition ํ โฆโ โซ X A e ํ t (a, b)ํ eํ t (ํ) โค eํ t (a,b) dํ A (a) is analytic on ฮ. TakingA = W = V\(Tโ Y), we obtain, for allํ โ ฮ,tโX T , andyโX Y , the unnormalized marginal ํ ํ,Y|do(T=t) (y) โ โซ X W e ํ t (y, w)ํ eํ t (ํ) โค eํ t (y,w) dํ W (w). Taking instead A = X = V\ T, we obtain, for all ํ โ ฮ, the normalizing factor ํ e ํด t ( eํ t (ํ)) = โซ X X e ํ t (x)ํ eํ t (ํ) โค eํ t (x) dํ X (x). Both the unnormalized marginal and the normalizing factor are therefore analytic inํ. Since, for all ํ โ ฮ,ํ e ํด t ( eํ t (ํ)) > 0 , its reciprocalํ โ e ํด t ( eํ t (ํ)) is also analytic inํ. Therefore, for allyโX Y and all tโX T , 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 parametriza- tions, under Assumptions 4.4โ4.7, the falsifier in Definition 4.1 induces an almost-surely correct verifier relative toP ฮ (X V ). Proof. If the input to the falsifier isํ = none, the falsifier checks non-identifiability using the ID algorithm, returningfalseif the ID algorithm returns an identifying formula andtrueelse. Since 28 the ID algorithm is sound and complete for identification, the falsifierโs output for the inputnoneis 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โX T and for all densities factorizing according to the graph wheneverํis well-defined. Hence, the falsifier never finds a counterexample and outputstrue; in other words, the falsifier never incorrectly rejects an observational formula that is identifying asfalse. 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 ํพ ร ํ=1 ํ ํ โ ํ ! = ํพ ร ํ=1 P(ํ ํ โ ํ) = ( ํ(ํ) ) ํพ = 0, 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 evalu- ation length ofํis at mostํ, and thatํis non-identifying relative toP ฮ (X V ), that is, there exist ํ โ โ ฮandt โ โ X T 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 P โtโX T ,โฆํโง(ํ ํ โฒ ,O , t) = ํ ํ โฒ ,Y|do(T=t) ํ Y -a.e. โค (2ํโ 1) 1+ ร ํ ํ=1 ํพ ํ min 1โคํโคํ |ํด ํ | ,(G.7) where, for all ํ โ 1,...,ํ, ํพ ํ : = ๏ฃฑ ๏ฃด ๏ฃด ๏ฃด๏ฃฒ ๏ฃด ๏ฃด ๏ฃด ๏ฃณ 1,if operation ํ is Gaussian marginalization, 2,if operation ํ is scalar addition, subtraction, multiplication or division, ํ+ 1, 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ํ โ โ ฮandt โ โX T 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 fixingt โ , 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โX T , โฆํโง(ํ ํ โฒ ,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. SinceGis 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 [(ํผโ ํต โค ) โ1 ] ํํ ํ 2 ํ [(ํผโ ํต) โ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 (ํ)/1andฮฃ 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 of2. For example,ํ 1 (ํ)/ํ 1 (ํ) + ํ 2 (ํ)/ํ 2 (ํ) = (ํ 1 (ํ)ํ 2 (ํ) + ํ 2 (ํ)ํ 1 (ํ))/(ํ 1 (ํ)ํ 2 (ํ)), and both numerator and denominator degrees are at most2โ. 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 (ํ) ํ B (ํ) , ฮฃ(ํ) = 1 ํ(ํ) ํด A (ํ) ํด AB (ํ) ํด BA (ํ) ํด B (ํ) . whereฮฃ(ํ), ํด A (ํ), ํด B (ํ)are symmetric andํด BA (ํ) = ํด AB (ํ) โค . For allb โ X B , conditioning gives ํ A|B=b (ํ) = ํ A (ํ)+ ฮฃ AB (ํ)ฮฃ B (ํ) โ1 (bโ ํ B (ํ)), ฮฃ A|B (ํ) = ฮฃ A (ํ)โ ฮฃ AB (ํ)ฮฃ B (ํ) โ1 ฮฃ BA (ํ). First, we treat the covariance update. Since ฮฃ B (ํ) = ํด B (ํ)/ํ(ํ), we have ฮฃ B (ํ) โ1 = ํ(ํ) adj(ํด B (ํ)) det(ํด B (ํ)) . We bound the degree of the determinant and the adjugate entries. By the Leibniz formula, det(ํด B (ํ)) = โ๏ธ ํโฮ ํ sign(ํ) ํ ร โ=1 (ํด B (ํ)) โ,ํ(โ) , whereฮ ํ is the set of all permutations of1,..., ํ. 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(ํด B (ํ))) โค ํโ. For all ํ, ํ โ 1,..., ํ, the(ํ, ํ)-th entry of the adjugate matrix is a cofactor: adj(ํด B (ํ)) ํํ = (โ1) ํ+ํ det (ํด B (ํ)) (ํ,ํ) , where(ํด B (ํ)) (ํ,ํ) 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(ํด B (ํ)) ํํ ) โค (ํโ 1)โ. Substituting these expressions into the conditional covariance gives ฮฃ A|B (ํ) = ํด A (ํ) det(ํด B (ํ))โ ํด AB (ํ) adj(ํด B (ํ))ํด BA (ํ) ํ(ํ) det(ํด B (ํ)) . 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(ํด B (ํ)) ํขํฃ (ํด 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(ํด B (ํ))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. Sincebis fixed, each component ofbโ ํ B (ํ)can be written as(bํ(ํ)โ ํ B (ํ))/ํ(ํ), with numerator and denominator degree at most โ. Using the expression for ฮฃ B (ํ) โ1 above, we obtain ํ A|B=b (ํ) = ํ A (ํ) det(ํด B (ํ))+ ํด AB (ํ) adj(ํด B (ํ))(bํ(ํ)โ ํ B (ํ)) ํ(ํ) det(ํด B (ํ)) . 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ํ ํ (ํ)/ํ ํ (ํ), wheredeg(ํ ํ (ํ)), 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 P(ํ ฮ (ํ โฒ ) = 0) โค ํป+ โ 0 min 1โคํโคํ |ํด ํ | = (2ํโ 1) 1+ ร ํ ํ=1 ํพ ํ min 1โคํโคํ |ํด ํ | . 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 graphG ํ with its canonical directed acyclic graph. There are, however, infinitely many latent-variable directed acyclic graphs whose latent projection isG ํ . An alternative is to avoid specifying the latent structure and to work directly withG ํ and its maximal arid projection e G ํ , that is, a maximal arid graph on the same observed set asG ํ . 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 X O = (ํ ํ 1 ,..., ํ ํ ํ ) โค denote the random vector associated with the observed variables O. We consider the linear Gaussian structural equation model associated with e G ํ : X O = ํต โค X O + ํ, whereํต = (ํ ํํ ) โ R ํรํ is such that, for allํ, ํ โ 1,...,ํ,ํ ํํ = 0wheneverํ ํ โ ํ ํ is not an edge of e G ํ , and whereํ โผ N(0,ฮฉ), withฮฉ = (ํ ํํ ) โ R ํรํ positive definite and such that, for allํ, ํ โ 1,...,ํwithํ โ ํ,ํ ํํ = 0wheneverํ ํ โ ํ ํ is not an edge of e G ํ . The resulting covariance matrix isฮฃ = (ํผ ํ โ ํต) โโค ฮฉ(ํผ ํ โ ํต) โ1 . 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. LetK โ 1,...,ํbe the set of indices such that T = ํ ํ | ํ โ K. We can compute the interventional density by setting, for allํ โ Kand 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 G ํ of an acyclic directed mixed graphG ํ defines the same nested Markov model asG ํ (Shpitser et al., 2018, Theorem 30). Moreover, Shpitser et al. (2018, Theorem 35) show that the above linear Gaussian structural equation model associated with the maximal arid projection e G ํ ofG ํ coincides with the Gaussian nested Markov model ofG ํ . Thus, the maximal arid projection gives a linear Gaussian parametrization of exactly the Gaussian nested Markov model associated withG ํ , rather than a potentially smaller model associated with the linear Gaussian structural equation model onG ํ 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 isG ํ , 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 ofG ํ 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)wherepa(ํ) = ํ. Underdo(ํ = ํก), 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 floating- point 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 thatGhasํnodes. We consider a parametric familyํ ํ ํ (ํฃ ํ | v pa(ํ ํ ) ) ํ ํ โฮ ํ ํ ํ โV where, for all ํ โ 1,...,ํ and all ํ ํ = (ํผ ํ ,ํฝ ํํ ํ:ํ ํ โpa(ํ ํ ) ,ํ 2 ํ ) โ ฮ ํ โ R ํ ํ , with ํ 2 ํ > 0, ํ ํ ํ (ํฃ ํ | v pa(ํ ํ ) ) =N ยฉ ยญ ยซ ํฃ ํ ; ํผ ํ + โ๏ธ ํ:ํ ํ โpa(ํ ํ ) ํฝ ํํ ํฃ ํ , ํ 2 ํ ยช ยฎ ยฌ . The parameter vectorํ = (ํ 1 ,...,ํ ํ ) โ ฮโ R ํ , withํ = ร ํ ํ=1 ํ ํ , then collects all intercepts, edge coefficients and conditional variances. Defineํผ = (ํผ 1 ,...,ํผ ํ ) โค ,ฮฉ = diag(ํ 2 1 ,...,ํ 2 ํ ), and the ํรํmatrixํต, where, for allํ, ํ โ 1,...,ํ,ํ โ ํ,ํต ํํ = ํฝ ํํ ifํ ํ โ pa(ํ ํ ), andํต ํํ = 0otherwise. Then the product of all Gaussian conditionals induces a joint Gaussian distribution with mean vector and covariance matrix ํ full (ํ) = (ํผโ ํต โค ) โ1 ํผ, ฮฃ full (ํ) = (ํผโ ํต โค ) โ1 ฮฉ(ํผโ ํต) โ1 .(G.6) 34 For fixedํ โ ฮandtโX T , both the distribution returned by the candidate observational formula ํand the target interventional distribution are Gaussian. Therefore, checking that, for allt โ X T , โฆํโง(ํ ํ,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ํ โ ฮandt โ X T , 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 oft, and since, for allํ โ ฮ,ํ ํ (ํ, t)and ํ do (ํ, t)are affine functions oft, 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). LetFbe a field, and letF[ํฅ 1 ,...,ํฅ ํ ]denote the set of polynomials inํฅ 1 ,...,ํฅ ํ with coefficients inF. 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ํด โ Fbe 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โํ,..., ํ\0and the conditional variances are sampled from1,..., 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โX T , 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 evalu- ation length ofํis at mostํ, and thatํis non-identifying relative toP ฮ (X V ), that is, there exist ํ โ โ ฮandt โ โ X T 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 P โtโX T ,โฆํโง(ํ ํ โฒ ,O , t) = ํ ํ โฒ ,Y|do(T=t) ํ Y -a.e. โค (2ํโ 1) 1+ ร ํ ํ=1 ํพ ํ min 1โคํโคํ |ํด ํ | ,(G.7) where, for all ํ โ 1,...,ํ, ํพ ํ : = ๏ฃฑ ๏ฃด ๏ฃด ๏ฃด๏ฃฒ ๏ฃด ๏ฃด ๏ฃด ๏ฃณ 1,if operation ํ is Gaussian marginalization, 2,if operation ํ is scalar addition, subtraction, multiplication or division, ํ+ 1, 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|+ 1intervention 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ํ โ ฮandt โ X T , 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 W : = (T, Z)and defineฮ YW : = ฮฃ YW ฮฃ โ1 W = [ ฮ YT ฮ YZ ], whereฮ YT andฮ YZ are the blocks of the regression coefficient ofYon the joint vector(T, Z)corresponding toTandZ, respectively. Therefore, for all t โฒ โX T and zโX Z , ํ ํ,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 ํ , โซ R ํ N(y;ํ+ ํตx,ํ)N(x;ํ,ํ) ํx =N(y;ํ+ ํตํ,ํ+ ํตํํต โค ). Since ํ ํ,T (t โฒ ) =N(ํ T ,ฮฃ T ), applying this identity to the inner integral gives, for all zโX Z , โซ ํ ํ,Y|T,Z (y | t โฒ , z)ํ ํ,T (t โฒ ) dt โฒ =N ํ Y + ฮ YZ (zโ ํ Z ),ฮฃ Y|T,Z + ฮ YT ฮฃ T ฮ โค YT . We now evaluate the outer integral. Since ํ ํ,Z|T (z | t) =N ํ Z + ฮ ZT (tโ ํ T ),ฮฃ Z|T , ฮ ZT : = ฮฃ ZT ฮฃ โ1 T , applying the same affine-integration identity to the outer integral gives โฆํ fd Z โง(ํ ํ,O , t) =N(ํ fd (ํ, t),ฮฃ fd (ํ)), where ํ fd (ํ, t) = ํ Y + ฮ YZ ฮ ZT (tโ ํ T ), ฮฃ fd (ํ) = ฮฃ Y|T,Z + ฮ YT ฮฃ T ฮ โค 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 ) ํํ + ํ โค ํ ฮฃ T ํ ํ + ํ โค ํ ฮฃ 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 scalar primitive operations. Therefore, for allํ, ํ โ 1,...,|Y|, the termํ โค ํ ฮฃ T ํ ํ requires2ํ 2 +ํโ1 scalar primitive operations, and the term ํ โค ํ ฮฃ Z|T ํ ํ requires 2ํ 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 ). Computingt โ ํ T requiresํscalar subtractions. Multiplying this vector byฮ ZT requiresํํ scalar multiplications andํ(ํโ 1)scalar additions. Multiplying the result byํ โค ํ requiresํscalar multiplications andํ โ 1scalar 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 factor1, the two Gaussian conditioning operations contribute factorsํ+ 1each, and each scalar operation contributes factor 2. Thus, for both the covariance and mean entries of the front-door formula, ํ ร ํ=1 ํพ ํ โค (ํ+ 1) 2 2 2ํ 2 +ํ+2ํ 2 +ํ . Ifํ = ํ = 1,ํ = 10andmin 1โคํโคํ |ํด ํ | = 2 64 โ 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 at1. 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 ํ(z | t) โ๏ธ t โฒ ํ(y | t โฒ , z) ํ(t โฒ ).(H.9) 38 In particular, a set of variables Z satisfies the front-door criterion if: (i) Z intercepts all directed paths from T to Y; (i) there is no unblocked back-door path from T to Z; (i) 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 The gateway test described in Section 5 is sound and exhaustively complete relative toฮฆ fd Y,T . The 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 forY | do(T). More precisely, let e ฮฆ Y,T โ ฮฆ Y,T be a finite class of observational formulas. Each ํ โ e ฮฆ Y,T is verified in turn, and passes the test if it is verified as identifying. With an exact verifier, this procedure returns all and only the identifying formulas in e ฮฆ Y,T . If one instead uses the falsifier from Section 4, then the procedure is almost-surely sound while it is exhaustively complete relative to e ฮฆ Y,T for the conditional exponential family chosen in the falsification routine. Graphical criteria that are sound and exhaustively complete relative to e ฮฆ Y,T may therefore be 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, sound and exhaustively complete graphical criteria relative to the class of adjustment formulasฮฆ adj 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 known to be both sound and exhaustively complete relative toฮฆ adj Y,T . Verification enables us to fill this gap. 40