Uncovering Hidden Correctness in LLM Causal Reasoning via Symbolic Verification
Paul He, Yinya Huang, Mrinmaya Sachan, Zhijing Jin
TL;DR
DoVerifier formalizes causal reasoning evaluation as a symbolic derivation problem under a DAG $G=(V,E)$, using the do-calculus and probability theory to verify whether a model-generated expression $\phi$ entails a target $\psi$ ($\phi \vdash_G \psi$). The method constructs a derivation graph and searches for a valid sequence of rule applications, delivering sound and complete results within a depth bound and offering semantic guarantees that surface-metrics cannot provide. Empirically, DoVerifier recovers many semantically correct outputs that surface metrics miss, improves causal reasoning evaluation on synthetic data and the CLadder benchmark, and enables symbolic feedback loops to improve LLM outputs without supervision. The work highlights the gap in current evaluation approaches and demonstrates the practical value of formal causal verification for robust, interpretable reasoning in LLMs, while noting scalability challenges and future directions such as neural-guided proof search. Overall, the framework advances principled, semantics-driven assessment of causal expressions in language models and points to broader adoption in evaluation and model-improvement workflows.
Abstract
Large language models (LLMs) are increasingly being applied to tasks that involve causal reasoning. However, current benchmarks often rely on string matching or surface-level metrics that do not capture whether the output of a model is formally valid under the semantics of causal reasoning. To address this, we propose DoVerifier, a simple symbolic verifier that checks whether LLM-generated causal expressions are derivable from a given causal graph using rules from do-calculus and probability theory. This allows us to recover correct answers to causal queries that would otherwise be marked incorrect due to superficial differences in their causal semantics. Our evaluations on synthetic data and causal QA benchmarks show that DoVerifier more accurately captures semantic correctness of causal reasoning traces, offering a more rigorous and informative way to evaluate LLMs on causal reasoning.