pith. machine review for the scientific record. sign in

arxiv: 2604.22041 · v1 · submitted 2026-04-23 · 💻 cs.PL

Recognition: unknown

Causality and Semantic Separation

Adam Chlipala, Anna Zhang, Eunice Jun, London Bielicke, Qinglan Luo

Authors on Pith no claims yet

Pith reviewed 2026-05-08 12:42 UTC · model grok-4.3

classification 💻 cs.PL
keywords causalityd-separationnoninterferencesemantic separationcausal graphsexperiment designformal verification
0
0 comments X

The pith

d-separation exactly coincides with a semantic definition of noninterference inspired by security theory.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper proves that d-separation, the standard graph-based test for whether an experiment adequately controls for confounding variables, is equivalent to a semantic notion of variable separation drawn from noninterference in computer security. The proof is mechanized in the Rocq proof assistant and does not rely on any probabilistic assumptions about the data. A reader should care because it gives a rigorous, semantics-first explanation for why the graph condition succeeds, allowing scientists to verify experiment designs more formally and to identify when their causal model of the world might be wrong.

Core claim

Our central result is that d-separation exactly coincides with a novel semantic definition inspired by noninterference from the theory of security. This characterization provides a structural semantic foundation for d-separation and helps explain why the graph-theoretic condition is correct, independently of probabilistic assumptions. For each given automated test on the quality of an experiment design, our theorem justifies an associated method for falsifying the world-modeling hypothesis behind the experiment.

What carries the argument

The exact match between d-separation on causal graphs and a noninterference-inspired semantic separation that captures causal independence under interventions.

If this is right

  • The theorem justifies a falsification method for the world-modeling hypothesis of any automated test on experiment design quality.
  • The equivalence supplies a semantic foundation that makes the graph condition intuitive even when probabilities are absent.
  • It applies directly to experiment designs that use d-separation to control confounders.
  • Mechanization confirms the coincidence holds rigorously in a formal proof assistant.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Formal verification tools for experiment design could adapt existing program-analysis methods to check causal graphs against semantic models.
  • The connection to noninterference may let researchers import techniques from information-flow security to analyze causal dependencies in programs.
  • Scientists facing graphs too complex for manual d-separation checks could fall back to the semantic definition for validation.

Load-bearing premise

The chosen semantic definition of noninterference correctly captures the intended notion of causal independence without probabilistic assumptions.

What would settle it

A concrete causal graph and variable sets where d-separation declares two variables independent but the semantic noninterference definition shows dependence under intervention, or the reverse.

Figures

Figures reproduced from arXiv: 2604.22041 by Adam Chlipala, Anna Zhang, Eunice Jun, London Bielicke, Qinglan Luo.

Figure 2.1
Figure 2.1. Figure 2.1: These causal models illustrate examples of mediators, confounders, and colliders in academic view at source ↗
Figure 2
Figure 2. Figure 2: b view at source ↗
Figure 3
Figure 3. Figure 3 view at source ↗
Figure 3.1
Figure 3.1. Figure 3.1: (Left) This causal model encodes the intuition view at source ↗
Figure 3
Figure 3. Figure 3 view at source ↗
Figure 3
Figure 3. Figure 3 view at source ↗
Figure 3.3
Figure 3.3. Figure 3.3: (Left) Catalyst update: modifying𝑈 (𝑢) (highlighted) changes 𝑢, propagating to 𝑤 and violating its conditioned value. (Right): Reparative propagation: restoring 𝑤 may use either 𝑈 (𝑤) or 𝑈 (𝑣) (highlighted). Here, repair is performed via 𝑈 (𝑣), forcing a change in 𝑣. value of 𝑢 from 0 to 1. To preserve the conditioned value of 𝑤, the value of 𝑣 must change from 1 to 0. Thus, the values of 𝑢 and 𝑣 are dep… view at source ↗
Figure 3
Figure 3. Figure 3 view at source ↗
Figure 3.4
Figure 3.4. Figure 3.4: (Left) Catalyst update: modifying 𝑈 (𝑢) (highlighted) changes 𝑢, propagating through 𝑧1 to 𝑧2 and violating both condi￾tioned nodes. (Right): Reparative propagation: restoring 𝑧1 may only use 𝑈 (𝑧1) (highlighted), which also restores 𝑧2. Proc. ACM Program. Lang., Vol. 10, No. PLDI, Article 196. Publication date: June 2026 view at source ↗
Figure 2
Figure 2. Figure 2: b view at source ↗
Figure 5
Figure 5. Figure 5 view at source ↗
Figure 5.1
Figure 5.1. Figure 5.1: (Left) Assuming the path high￾lighted in blue is 𝑑-connected, then 𝑐 must have a descendant in 𝑍. Assuming 𝑐 ∉ 𝑍, it must have a descendant 𝑑 ∈ 𝑍 and a de￾scendant path to 𝑑 view at source ↗
Figure 5
Figure 5. Figure 5 view at source ↗
Figure 6
Figure 6. Figure 6: a view at source ↗
Figure 6.1
Figure 6.1. Figure 6.1: For any 𝑢, 𝑣 such that 𝑣’s value is affected by a change in 𝑢 with a sequence of unobserved-terms assignments 𝑈0,𝑈1,𝑈2, we can construct a 𝑑-connected path from 𝑢 to 𝑣 using 𝑧 ∈ 𝑍 and shared ancestors 𝑎 ′ , 𝑎. arbitrary-length sequences that satisfy the constraints in Definition 3.3, thereby leveraging the full expressive power of 𝑑-connectedness. 6.3 Generalizing to Arbitrary-Length Sequences Intuitivel… view at source ↗
read the original abstract

The design of scientific experiments deserves its own variation of formal verification to catch cases where scientists made important mistakes, such as forgetting to take confounding variables into account. One of the most fundamental underpinnings of science is causality, or what it means for interventions in the world to cause other outcomes, as formalized by computer scientists like Judea Pearl. However, these ideas had not previously been made rigorous to the standards of the programming-languages community, where one expects a (syntactic) program analysis to be proved sound with respect to a natural semantics. In the domain of causality, as the relevant "program analysis," we focus on $d$-separation, a classic condition on graphs that can be used to decide when the design of an experiment controls for sufficiently many confounding variables, even though the reason that this condition works is often unintuitive. Our central result (mechanized in Rocq) is that $d$-separation exactly coincides with a novel semantic definition inspired by noninterference from the theory of security. This characterization provides a structural semantic foundation for $d$-separation and helps explain why the graph-theoretic condition is correct, independently of probabilistic assumptions. For each given automated test on the quality of an experiment design, our theorem justifies an associated method for falsifying the world-modeling hypothesis behind the experiment.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The paper claims that d-separation on causal graphs exactly coincides with a novel semantic definition of causal independence, defined via noninterference-style independence of interventions and mechanized as a theorem in Rocq. This equivalence is presented as providing a structural semantic foundation for d-separation that holds independently of probabilistic assumptions, and as justifying associated methods for falsifying experiment-design hypotheses.

Significance. If the mechanized equivalence holds, the result supplies a rigorous, probability-free justification for d-separation by grounding it in a semantic notion drawn from security theory. The machine-checked proof in Rocq is a clear strength, as is the explicit framing of the semantic definition as the foundation that explains why the graph-theoretic condition is correct.

minor comments (3)
  1. The abstract states that the theorem 'justifies an associated method for falsifying the world-modeling hypothesis,' but the manuscript should include a concrete example (e.g., in §4 or §5) showing how the equivalence is applied to derive a falsification procedure from a given d-separation test.
  2. The semantic noninterference definition is described as 'inspired by' security theory; the paper should clarify in the introduction or §3 whether any adjustments were made to the standard noninterference formulation and why those adjustments preserve the intended causal reading.
  3. The manuscript should provide a pointer to the Rocq development (repository, commit hash, or supplementary archive) so that the mechanized proof can be inspected independently.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of our work and the recommendation for minor revision. The report correctly identifies the core contribution: a mechanized equivalence in Rocq between d-separation on causal graphs and a semantic noninterference property that is independent of probabilistic assumptions. As no specific major comments were raised, we have no revisions to propose.

Circularity Check

0 steps flagged

No significant circularity: mechanized equivalence between independent definitions

full rationale

The paper defines a novel semantic notion of causal independence (inspired by noninterference) and proves via Rocq mechanization that it exactly coincides with the standard graph-theoretic d-separation criterion. This is a direct formal equivalence between two separately stated concepts, with the semantic definition positioned as the foundational justification rather than being constructed from d-separation. No parameters are fitted, no self-referential equations appear, and no load-bearing steps reduce to self-citations or prior author work. The derivation is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The claim rests on standard background definitions from causality and information-flow security plus the novel semantic definition of noninterference; no free parameters or invented entities are introduced.

axioms (2)
  • domain assumption The causal graph faithfully encodes the true causal structure of the domain.
    Standard assumption in causal inference; invoked to interpret d-separation.
  • ad hoc to paper The semantic noninterference property correctly models causal independence.
    The paper's novel contribution; the equivalence proof depends on this definition being the right one.

pith-pipeline@v0.9.0 · 5534 in / 1178 out tokens · 45169 ms · 2026-05-08T12:42:45.734674+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

6 extracted references

  1. [1]

    Then, we define 𝐴2 := {𝑢 : 𝑖𝑤 } ∪ 𝐴′ 2

    Let 𝑖𝑤 be the index of 𝑤 in Pa(𝑢). Then, we define 𝐴2 := {𝑢 : 𝑖𝑤 } ∪ 𝐴′ 2. Case 2: 𝒖 → 𝒘 → · · · 𝒗. By the induction hypothesis, there is a set 𝐴′ 2 corresponding to 𝑆 ′ 2 for the path 𝑤 → · · ·𝑣. Note that 𝑤 ∈ 𝑆 ′ 1, but 𝑤 ∈ 𝑆2. Furthermore, 𝑢 ∈ 𝑆1. Thus, 𝑆2 = {𝑤 } ∪ 𝑆 ′

  2. [2]

    Then, we define 𝐴2 := {𝑤 : 𝑖𝑢 } ∪ 𝐴′ 2

    Let 𝑖𝑢 be the index of 𝑢 in Pa(𝑤 ). Then, we define 𝐴2 := {𝑤 : 𝑖𝑢 } ∪ 𝐴′ 2. Case 3a: 𝒖 → 𝒘 ← 𝒗. Consider the case of a three-node path, in which 𝑤 is a collider. Then, 𝑆2 = ∅, so let 𝐴2 := ∅. Case 3b: 𝒖 → 𝒘 ← 𝒘 ′ · · · 𝒗. Now suppose there are more than three nodes in the path. By the induction hypothesis, there is a set 𝐴′ 2 corresponding to 𝑆 ′ 2 for th...

  3. [3]

    Thus, we can define 𝐴2 as desired for a path of length 𝑛 for all cases of edge orientations

    So, we define 𝐴2 := 𝐴′ 2. Thus, we can define 𝐴2 as desired for a path of length 𝑛 for all cases of edge orientations. □ Lemma D.2. There exists 𝐴3, assignments for the nodes of 𝑆3 to N × N × X × X, satisfying that for all (𝑤, (𝑖, 𝑗, 𝑥, 𝑦 )) ∈ 𝐴3, there exist nodes 𝑎, 𝑏, such that 𝑎 and 𝑏 are the 𝑖-th and 𝑗-th nodes in Pa(𝑤 ), respectively, and 𝑎 → 𝑤 ← 𝑏 ...

  4. [4]

    Thus, we only need to add on an entry for 𝑤 to 𝐴′ 3, and we do so using the same methods as Case 1, defining 𝐴3 := {𝑤 : (𝑖𝑢, 𝑖𝑣, 𝑥, 𝑦)} ∪ 𝐴′

  5. [5]

    □ Lemma D.3. There exists 𝐴4, assignments for the nodes of 𝑆4 to N, satisfying that for all (𝑤, 𝑖 𝑎) ∈ 𝐴4, there exists 𝑖𝐷 , nodes 𝑐, 𝑑, 𝑎 and list of nodes 𝑝, such that (𝑐, (𝑝, 𝑑)) ∈ 𝐷 where 𝑐 ≠ 𝑑, 𝑤 is at index 𝑖𝐷 in path (𝑐, 𝑑, 𝑝), 𝑎 is at index 𝑖𝐷 − 1 in (𝑐, 𝑑, 𝑝), and 𝑎 is the 𝑖𝑎-th node in Pa(𝑤 ). Proof. If 𝑤 ∈ 𝑆4, then 𝑤 must belong to the descenda...

    2026

  6. [6]

    Let 𝑃 ′ be the subpath 𝑤 1 · · ·𝑣

    Suppose 𝑃 has length 𝑛 + 1, where 𝑛 ≥ 3, so 𝑃 is 𝑢 ↔ 𝑤 1 ↔ 𝑤 2 · · ·𝑣. Let 𝑃 ′ be the subpath 𝑤 1 · · ·𝑣. If 𝑃 has an arrow into 𝑢, then 𝑢 ∈ 𝑆2, so 𝑥, 𝑦 are still consecutive nodes in 𝑆 ′ 1 corresponding to 𝑃 ′. Thus, we can apply the induction hypothesis on 𝑃 ′ to get the desired 𝑧. Now consider the case that 𝑃 has an arrow out of 𝑢. If 𝑢 ≠ 𝑥, then 𝑥 and...

    2026