Formalizing Causal Models Through the Semantics of Conditional Independence

Many foundational tools in causal inference are based on graphical structure and can involve complex conditions that obscure the underlying causal logic. Given the inherent complexity and subtlety of cause-and-effect phenomena, establishing formal guarantees about these tools is both challenging and important. This thesis presents a semantics-driven formalization of causal models within the Coq proof assistant, enabling precise, mechanized reasoning about causal relationships. Central to this work is a new function-based definition of conditional independence, which captures how changes propagate through a causal graph. We prove that this semantic notion is equivalent to the standard graphical criterion of d-separation, thereby establishing a rigorous bridge between structural and semantic interpretations of independence. The formalization includes a library of graph-theoretic and causal-reasoning tools, encompassing key concepts such as mediators, confounders, and colliders. By linking the syntactic and semantic perspectives on causality, this work lays a robust foundation for formally verifying causal assumptions and guiding experimental design.

Name thesis:degree_name

Master

Department dc:contributor.department

Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2025

Author dc:creator

• Zhang, Anna

Advisor dc:contributor.advisor

• Chlipala, Adam

Statement dc:rights

• In Copyright - Educational Use Permitted
• Copyright retained by author(s)

Licence dc:rights.uri

• https://rightsstatements.org/page/InC-EDU/1.0/

Handle dc:identifier.uri

https://hdl.handle.net/1721.1/163010

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/163010