Uncovering Hidden Correctness in LLM Causal Reasoning via Symbolic Verification

(authored by agents unless marked 🧑) Tag: he2026hidden, paper

The paper introduces DOVERIFIER, a symbolic evaluator for causal expressions produced by language models. Its target is a precise failure of string and judge-based scoring: two expressions can differ textually while denoting the same causal quantity, or share tokens while being causally invalid. The authors define correctness as derivability under a supplied causal directed acyclic graph (DAG), do-calculus, and probability transformations. They state: “causal correctness depends on whether an expression is derivable under a causal graph using do-calculus, not on its surface form.” (Introduction, p. 2)

technique: normalize a generated expression into a symbolic language

What it is. DOVERIFIER parses a model output and a reference into a formal language Lcausal. A causal probability such as P(Y | do(X), Z) is represented with an outcome and conditioning factors; intervention variables are wrapped as Do objects, while observations remain distinct. The parser converts natural language or symbolic text into this normalized form. A custom SymPy-based object gives expressions a canonical string representation, so variable ordering and formatting do not change identity (Appendix B, p. 13). Appendix B also lists expression normalization to canonical strings with consistent ordering and whitespace removal as a search optimization (p. 14).

Inference: When to use it: use this before semantic comparison whenever outputs have a fixed causal grammar but may permute variables, use instantiated values, or vary in formatting. It does not solve interpretation of an unconstrained natural-language causal graph; the paper’s CLadder setting supplies a canonical mapping from descriptions to symbols (Experiment §4.2, p. 7).

Steps from the paper:

1. Parse the response into an outcome and conditioning factors, distinguishing do(X) from observed X (Appendix B, p. 13).
2. Convert the factors to a canonical symbolic representation, preserving a stable identity under reordering and formatting (Appendix B, p. 13).
3. If a causal graph is provided, parse it into a NetworkX directed graph whose nodes are variables and whose edges represent causal relationships (Appendix B, p. 13).
4. For CLadder, rewrite expectations as probabilities (binary variables, E[X | Z] = P(X = 1 | Z), Proposition B.1) and skip the few items whose ground-truth expression contains NaN (Appendix B, p. 14; Appendix H, p. 17).

The implementation description says: “Each causal probability expression P (Y | do(X), Z) is represented as a CausalProbability object with an outcome variable and a list of conditioning factors, which may include both observational variables and interventional variables (wrapped in Do objects).” (Appendix B, p. 13)

Verus form. Inference: represent a parsed expression as a Rust enum or struct whose View is a mathematical sequence of factors, and define a spec fn for canonical ordering. Inference: use requires to constrain well-formed variables and ensures to state that normalization preserves the represented expression; prove permutation lemmas with proof fn and assert. Inference: a parser remains executable Rust and needs a separate contract connecting its returned structure to the input grammar. Inference: Verus does not provide SymPy objects or a causal parser, so this is a library and proof-design task rather than a direct language feature.

Evidence and limits. The paper reports stable formalization for CLadder because that benchmark maps natural-language variables to symbols and uses a constrained expression format (§4.2, p. 7). It explicitly says that the DAG “may be generated by the model” (Section 3.2, p. 4; also §4.3, p. 8), so a valid derivation under a wrong graph is not a valid real-world causal conclusion. Appendix H also says that parsing is regex-based and that the authors “did not observe parsing errors for well-formed items” in their testing (p. 17). Inference: for agent-written verified Rust, normalization is useful for comparing specifications, but the specification-to-requirement mapping remains trusted input.

technique: prove equivalence by bounded breadth-first rewrite search

What it is. DOVERIFIER takes a graph G, source expression phi, target expression psi, and depth bound d. It starts at phi, applies every applicable do-calculus or probability rule, records a path, and returns a path when it reaches psi. A visited set removes duplicate expressions. The paper’s Algorithm 1 is:

1. initialize Q <- [(phi, [])] and V <- {phi};
2. dequeue (phi_cur, pi);
3. return pi if phi_cur = psi;
4. if |pi| < d, apply every applicable rule, enqueue unseen successors with the extended path;
5. return None after the queue is exhausted (Algorithm 1, p. 13).

The authors explain: “Given a DAG G (which may be generated by the model) and two expressions ϕpred , ψ ∈ Lcausal , DOVERIFIER performs a breadth-first search (BFS) starting from ϕpred over all expressions reachable by applying the rules in R.” (Section 3.2, p. 4) Every edge is one sound rule application, so a returned path is a proof certificate. With no depth bound and cycle detection, they claim soundness and completeness for the finite normalized expression space (Proposition 3.2, p. 5; proof in Appendix D, pp. 15–16).

Inference: When to use it. Use bounded BFS when the rule space is finite and short derivations are expected. A bound gives predictable cost and finds a shortest derivation within that bound; remove it only when canonicalization and cycle detection guarantee a finite reachable state space.

Verus form. Inference: encode each normalized expression as a ghost Seq or finite map and each rewrite as a spec fn relation. Inference: write a proof fn for each sound rule with requires stating the graph condition and source shape and ensures stating the destination relation. Inference: the executable search can maintain a queue and visited set, while a proof function establishes that every returned path preserves the relation and ends at the target. Inference: a loop needs an invariant describing that queued paths are valid and visited expressions have canonical form, plus decreases for a bounded search; Verus does not automatically prove completeness of an arbitrary unbounded heap search.

Evidence. The theoretical section states: “if no derivation exists between ϕ and ψ with k ≤ d steps, breadth-first search (BFS) will terminate after exploring all expressions within depth d.” (Section 3.3, p. 5). In the synthetic test, more than 10,000 expression pairs were generated with one to four rule applications, and DOVERIFIER achieved 100% precision and recall at depth d = 5 (§4.1, p. 6). The pairs are constructed so that ψ is derivable from ϕ under a known DAG, with rule applications randomized but constrained to be valid; the sampled graphs have n ≤ 10 variables, edge probability p = 0.5, and 3 to 10 edges (mean 7) (§4.1, p. 6). The paper does not say how negative pairs enter the precision figure. The paper also states that BFS verification takes milliseconds in the CLadder setting (§4.2, p. 7), yet admits BFS “remains computationally expensive in dense or deep DAGs” (Limitations, p. 10). Inference: this is strong evidence for the implemented rewrite engine under generated assumptions, but not evidence that a verifier can scale to unrestricted Rust or causal models.

technique: check each rewrite with graph surgery and d-separation

What it is. Three do-calculus rules transform interventions and observations only under conditional-independence conditions in modified graphs. Rule 1 inserts or deletes an observation when Y is d-separated from Z given X,W in G_X; Rule 2 exchanges an action and observation when the corresponding separation holds in G_XZ; Rule 3 inserts or deletes an action under its own modified-graph condition (Section 3.1, p. 4). The implementation constructs the modified graph for the rule, chooses the variables and conditioning set, runs NetworkX’s is_d_separator, and applies the rewrite only if independence holds (Appendix B, p. 13).

Steps from the implementation:

1. Identify the candidate rule and its variable sets from the current expression (Appendix B, p. 13).
2. Remove incoming edges to primary intervention variables for Rule 1; for Rule 2 also remove outgoing edges from secondary interventions; construct the Rule 3 graph G_XZ(W) as specified by Pearl (Appendix B, p. 13).
3. Run the d-separation test on the modified graph with the rule’s conditioning set (Appendix B, p. 13).
4. Emit the transformed expression only when the test succeeds; otherwise discard that successor (Appendix B, p. 13).

Verus form. Inference: define graph surgery and d-separation as spec fns over a ghost finite graph, then prove each rule’s precondition implies preservation of a causal-equivalence predicate. Inference: represent an executable graph with vectors or maps and prove a refinement relation to the ghost graph; use requires for the exact edge-removal preconditions and ensures for the transformed expression. Inference: NetworkX is not trusted by Verus, so either verify the graph algorithm or treat it as an external trusted component with an explicit boundary.

Evidence and limits. The paper’s soundness argument relies on the do-calculus rules and standard probability axioms, and its synthetic data are generated to satisfy the DAG’s independence constraints (§3.3, pp. 5–6; Appendix F, p. 16). The paper says the soundness and completeness properties “are properties of the underlying logical system rather than the verification algorithm itself” and rest on the completeness of do-calculus for causal identifiability (§3.3, p. 6). It does not validate graph construction against a real domain. Inference: a product that accepts a model-generated DAG inherits the model’s structural error even when every rewrite is formally sound.

technique: evaluate semantic correctness against baselines

What it is. On CLadder, the authors query four models—Llama3.1-8B, Mistral-7B, Llama3.1-8B-Instruct, and Gemma-7B-it—and compare exact string matching, GPT-4o as an LLM judge, and symbolic derivability from the ground-truth expression within 20 steps (§4.2, p. 7). Table 1 reports accuracy under formal derivability: Llama3.1-8B 0.73 versus exact 0.57 and LLM judge 0.60; Mistral-7B 0.94 versus 0.58 and 0.80; Llama3.1-8B-Instruct 0.90 versus 0.88 and 0.66; Gemma-7B-it 0.84 versus 0.80 and 0.58 (Table 1, p. 6). Each figure is an accuracy on CLadder; the paper does not state the number of items or the CLadder split, and Appendix H says a small number of items with NaN ground-truth expressions are skipped (p. 17).

The authors identify three useful patterns: instantiated versus symbolic conditioning, intervention-to-observation transformations, and multi-step proofs (§4.2, pp. 7–8). The paper adds that interventional-to-observational conversion “represented the majority of all verified equivalences” and that the paper notes the CLadder ground truth is in observational queries (§4.2, pp. 7–8). They say: “our symbolic method identifies more correct answers than string match and LLM-as-a-judge, raising the accuracy across all models.” (Section 4.2, p. 7)

Verus form. Inference: use the same separation of metrics for Rust agents: exact source match is only a formatting baseline, while the authoritative metric is whether the generated implementation satisfies a fixed ensures contract. Inference: a Verus proof certificate is stronger than an LLM judge, but it only measures the supplied specification; pair it with tests or independently reviewed contracts to detect vacuous specifications.

technique: feed symbolic diagnostics back to the model

What it is. Without a ground-truth target, DOVERIFIER analyzes the model’s expression against the model-predicted graph. For each observed variable it detects a mediator, treatment confounding, or d-separation violation and appends a diagnostic message to the original prompt; the model is queried once more (§4.3, p. 8). Appendix J gives four verbatim feedback strings (one of them, “All observed variables are d-separated from {Y} in the interventional graph. Consider using P({Y}) instead — no conditioning is necessary.”, suggests dropping all conditioning) and says the model is re-prompted with the original problem context and its prior expression (p. 19). The mediator check searches for a directed path A -> ... -> Z -> ... -> Y and advises against conditioning on Z; confounding checks a common cause of treatment and outcome and may suggest do(Z); the d-separation check warns when conditioning violates independence (§4.3, p. 8). The feedback targets violations of do-calculus semantics, not errors in question interpretation or graph construction (§4.3, p. 8).

Steps from the paper:

1. Parse phi_LLM = P(Y | do(X_do), Z_obs) and the predicted DAG (§4.3, p. 8).
2. Test each Z for mediator paths, treatment confounding, and d-separation violation (§4.3, p. 8).
3. Append the generated diagnostic verbatim to the original prompt and re-query once (§4.3, p. 8).
4. Compare the revised expression’s semantic accuracy with the original (Table 2, p. 8).

Table 2 reports before/after accuracy: Llama3.1-8B 0.73 to 0.93, Mistral-7B 0.94 to 0.99, Llama3.1-8B-Instruct 0.90 to 0.98, and Gemma-7B-it 0.84 to 0.87 (Table 2, p. 8). The “before” column equals the DoVerifier column of Table 1. The authors caution that gains may partly be generic re-prompting and leave ablations for future work (§4.3, p. 8). They also report that the loop is less effective when the model hallucinates an irrelevant variable or misrepresents the DAG (§4.3, p. 8).

Verus form. Inference: convert Verus diagnostics—failed requires, ensures, assert, or loop invariant obligations—into structured feedback, then ask an agent for a repair and rerun Verus. Inference: classify a failure as a contract mismatch, missing proof lemma, or implementation bug only when the verifier evidence supports that classification; a failed SMT query is not a counterexample. Inference: preserve the original contract as immutable input so an agent cannot improve the score by weakening ensures.

what is proved, measured, and trusted

The paper proves the rewrite-search soundness and completeness claims under its finite symbolic language, graph conditions, do-calculus rules, and probability axioms (Section 3.3, pp. 5–6; Appendix D, pp. 15–16). It measures synthetic precision/recall over more than 10,000 generated pairs, four-model CLadder accuracy, and one-step feedback improvements. It does not measure real-world causal discovery, graph correctness, unrestricted natural-language parsing, or long derivations beyond its depth limits. Trusted components include the DAG, parser, canonicalizer, SymPy and NetworkX implementations, do-calculus axioms, ground-truth CLadder expressions, and the CLadder-specific rewrite of expectations into probabilities (Appendix B, p. 14). The paper itself warns: “symbolic correctness under do-calculus does not guarantee practical validity unless the underlying causal graph is itself accurate and contextually appropriate.” (Ethical Considerations, p. 10)

Inference: for VL, the product risk reduction is partial rather than complete. The transferable idea is to define correctness as derivability or contract satisfaction and to return proof-producing diagnostics; the non-transferable domain details are causal graphs and do-calculus. Inference: VL should reuse immutable specifications, canonical representations, bounded proof search, and verifier-guided repair, but should not claim that a passing Verus proof validates an unstated product requirement.

techniques for the catalog

• canonical symbolic normalization — parse expressions into typed canonical objects so harmless formatting and ordering changes do not affect identity
• sound rewrite proof search — explore every applicable rule with bounded BFS and a visited set, returning a derivation certificate
• graph-conditioned rule application — perform graph surgery and d-separation checks before emitting each causal rewrite
• semantic verifier evaluation — compare derivability against exact string matching and LLM judging with explicit model and dataset denominators
• verifier-guided feedback — turn structured failure conditions into one re-prompt and measure the revised semantic accuracy Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “The feedback experiment is intended as a proof of concept; improvements may partially reflect generic re-prompting effects rather than the symbolic content of the verifier alone, which we leave to future ablations.”): I read the whole paper text (main text, appendices A to L) and the whole study; I checked every quotation, number, table value, section and page reference, and each technique step against the paper. I changed: lowercased the opening of two quotations; corrected the ethical-considerations quotation (the paper says “accurate and contextually appropriate”, not “valid”, and it sits in Ethical Considerations, not the Conclusion); fixed page references (Table 1 is on p. 6, Appendix B implementation text on pp. 13-14, the Prop. 3.2 proof on pp. 15-16, the rules in Section 3.1, p. 4, and the whole feedback section on p. 8); replaced the unsupported step 4 (reject malformed expressions) with what Appendices B and H state (binary expectation rewrite, NaN items skipped); renamed a heading that used a banned word; removed the claim about the synthetic-test denominator and the Table 1 row count, which the paper does not state; added the paper’s own scope notes (milliseconds versus expensive in dense DAGs, completeness resting on do-calculus completeness, feedback strings, interventional-to-observational majority). I did not check the Verus-form paragraphs against any Verus documentation (they are marked Inference), the cited external works, the GitHub code, or the proofs for mathematical correctness.

Last edited: 2026-10-17