When Many Answers Are Valid, Voting Fails: Symbolic Verification for Best-of-K Causal Reasoning in LLMs
Omatharv Bharat Vaidya, Connor Thomas Jerzak, Zayne Rea Sprague, Fangcong Yin, Nhat Ho
cs.AI, stat.ML
2026-08-04
Voting fails in causal reasoning: valid answers fragment and a repeated error wins. CALVER scores traces on causal axioms for 42.1% on CLEAR queries, vs ~30% for voting and judges.
Self-consistency voting is a cheap way to squeeze more out of a model at inference: sample K reasoning traces and take the most frequent answer. It rests on one assumption, that the most frequent answer is the most reliable. That assumption fails systematically in causal reasoning, in two ways. The same confounding error gets sampled repeatedly and becomes the plurality winner. Or the correct answer is genuinely non-unique (several adjustment sets can satisfy the backdoor criterion), so valid votes fragment and an invalid answer wins simply by being the single largest mode. The paper's example: valid probability mass 0.70 splits across seven strings while the invalid answer is the single largest mode.
CALVER (Causal Axiom-Level VERification) is a training-free symbolic verifier. It does not touch the model; it only changes which of the K sampled traces is selected. Each trace is forced into a six-slot schema (graph, query, strategy, derivation record, computed result, answer) and scored by six deterministic binary checks: whether the graph parses and binds; whether the query binds to the asked question; whether the strategy is graphically valid (d-separation for backdoor, correct intervention); whether the derivation is well-formed; whether the reported number survives recomputation (for instance the average treatment effect can be recomputed); and whether the answer matches the recomputed result. The earliest trace with the maximum score wins. The whole thing runs in milliseconds on CPU using Pearl's causal-graph criteria, with no reference answer.
The main test is CLEAR find-one-valid queries, the kind with several graph-valid answers. On identical frozen sample pools:
| Selector | Accuracy |
| Plurality | 30% |
| Reward model (Skywork V2 8B) | 30.5% |
| LLM judge (Qwen2.5-72B) | 30% |
| Model confidence | 30% |
| CALVER | 42.1% |
Scaling the judge to 72B does not close the gap. By model, CALVER lifts Qwen-14B from 44.4% to 68.5% (+24.1pp) and Mistral NeMo 12B from 28.3% to 47.4%. The lead widens with the sampling budget: 7.7pp at K=2, 25.4pp at K=32. In an audited clean-core subset, 11 of 21 graph-valid CALVER selections differ from the benchmark's listed answer yet still satisfy the requested predicate, which shows the reference answer was never the unique correct one and scoring by it was unfair to begin with. Transfer is strong: 10 bnlearn Bayesian networks go from 39.8% (plurality) to 56.8% (CALVER); building the graph from text at three difficulty levels adds +24.2 / +14.2 / +17.6pp; K&K logic puzzles move from 50% to 77% (3-person) and 22% to 38% (5-person). Across 576 pools with at least one valid trace, an invalid answer wins plurality in 226; CALVER repairs 197 and introduces 54, a net of 24.8pp.
Best-of-K is the cheapest inference-time lever, but on tasks with non-unique answers a wrong vote is a failure of the voting rule, not the model. CALVER gives such tasks a selection layer that needs no retraining and costs effectively nothing (milliseconds on CPU). Its regime is well-defined: when answers are nearly unique, best-of-K already suffices; when text-to-graph extraction is reliable, extract once and solve directly. CALVER owns the middle ground, where many answers are valid and no single extraction is dependable.
The advantage is bounded. The authors concede that near-unique answers do not need CALVER and that reliable extraction makes direct solving better. There is a hard prerequisite: validity must be algorithmically decidable through graph computation, so the causal structure has to be formalizable; open-domain reasoning that cannot be written as a causal graph is out of scope. One telling comparison: against extract-then-solve on the executable subset, CALVER does not always win (L1/L2 direct extraction hits 92.8% / 96.7% versus CALVER's 83.7% / 82.4%). When extraction itself is accurate, bypassing the symbolic check and solving directly is sharper. CALVER's sweet spot is exactly the unreliable-extraction middle ground, and the paper states this honestly.