Source-linked AI summary
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
TL;DR
Causal best-of-K selection is difficult when valid answers fragment across strings and an invalid repeated answer can win. CALVER addresses this with reference-free symbolic verification of structured traces against causal criteria, achieving stronger selection than generic comparators and retaining an explicit regime boundary. The method is most appropriate when many answers are valid and no single text-to-graph extraction is dependable.
Problem
Self-consistency can fail in causal reasoning because multiple valid answers split votes, allowing an invalid answer to become the largest mode.
Method
CALVER is a training-free candidate-wise verifier that scores structured traces against executable causal validity criteria and selects the highest-scoring candidate.
Results
Across the evaluated settings, CALVER raises selected-answer performance over voting and generic scorers; on CLEAR many-satisfier queries it reaches 42.1% versus 30.5% for the closest generic comparator.
Takeaways & Limitations
Candidate selection can aggregate causal validity across fragmented answers, with gains reproduced across graph families, graph-from-text settings, model families, and truth-table logic.
Takeaways & Limitations
CALVER’s advantage is regime-bound: exact best-of-K suffices when answers are near-unique, while reliable text-to-graph extraction favors direct solving.
Abstract
from arXiv · showhide
Self-consistency assumes the most frequent answer among sampled reasoning traces is the most reliable, but this can fail in causal reasoning: samples often repeat the same confounding error, and votes fragment across multiple valid answers, letting an invalid answer win despite a valid minority trace. We introduce CALVER (Causal Axiom-Level VERification), a training-free symbolic verifier that scores structured traces against Pearl's causal criteria, including -separation, backdoor adjustment, and intervention, and selects the highest-scoring candidate without consulting a reference answer. On CLEAR find-one-valid queries that admit multiple graph-valid answers, CALVER reaches 42.1% where plurality, a reward model, an LLM judge, and model confidence remain near 30% on identical frozen pools. Scaling the judge to 72B does not close the gap. In an audited clean-core subset, 11 of 21 graph-valid CALVER selections differ from the benchmark's listed answer while still satisfying the requested predicate. The advantage widens with the sampling budget and reproduces across ten published Bayesian networks, a second model family, and settings where the model must build the graph from text. CALVER also improves thresholded average-treatment-effect decisions against exact ground truth, generalizes to logic under a truth-table checker, and scores each candidate in milliseconds on CPU. CALVER needs only a causal structure, supplied outright or built from the text; wherever that holds, selection can aggregate via causal validity.
Introduction
Self-consistency can fail on causal queries because valid answers fragment across strings, allowing an invalid mode to win. CALVER addresses this by selecting candidates according to graph-decidable causal validity rather than answer frequency alone.
- Motivation: Multiple fully correct causal answers can split exact-agreement votes, weakening self-consistency on find-one-valid queries.Conditioning sets may d-separate the same variables, so answer multiplicity is intrinsic to the task.
- Motivation: A familiar invalid answer can become the largest mode when valid answers are distributed across sampled traces.Additional samples can reinforce the repeated invalid answer rather than resolve the fragmentation.
- Approach: CALVER scores candidates using the graphical criteria that determine whether they belong to the query’s validity class.The approach uses algorithmically decidable graph computations, including ancestral restriction, separation, and intervention-graph surgery.
- Scope: Direct solving is strongest with one reliable extracted graph, while candidate-wise verification remains effective when traces preserve different query-relevant relations.The paper positions CALVER in the intermediate regime where interpretations vary across traces.
- Approach: The paper formulates best-of-K selection as aggregation over a decidable validity class and instantiates CALVER with a six-component graph-dependent trace score.The score applies to both directed acyclic graphs and acyclic directed mixed graphs.
2. Theory.
The theory explains why plurality can become inconsistent under answer multiplicity and establishes soundness for a strict average-treatment-effect certificate. It also identifies the query-local graphical information required for verification.
- Theory: A validity-fragmentation theorem explains why exact plurality can become inconsistent when multiple valid answers divide empirical counts.The paper also proves soundness for a strict average-treatment-effect certificate used in thresholded ATE decisions.
- Theory: Theorem 1 establishes soundness for the strict ATE certificate defined by the paper’s causal verification procedure.The certificate is distinct from the maximum deployed ranking score.
- Theory: The theory characterizes the query-local graphical information needed for verification on constructed graphs.This focuses verification on relations relevant to the queried predicate rather than requiring complete graph recovery.
- Experiments: Across experiments, CALVER outperforms exact plurality, confidence, reward-model, and LLM-judge selectors, with the advantage growing through K = 32.The comparison transfers across graph families, graph representations, model families, an independently implemented do-calculus prover, and formal logic.
Related Work
CALVER connects inference-time candidate selection with learned and symbolic verification, while adapting causal proof checking into reference-free candidate-wise selection. It is contrasted with extract-then-solve, which builds one global graph instead.
- Inference-time selection: Self-consistency, soft aggregation, semantic clustering, and LLM selection aggregate sampled candidates by frequency, likelihood, meaning, or judged preference.CALVER instead applies a fixed executable predicate directly to each candidate.
- Inference-time selection: Candidate-wise verification recognizes a valid trace without requiring its answer string to match another candidate’s string.This directly addresses settings where viable outputs rarely match verbatim.
- Verification: Learned reward models and symbolic systems provide precedents for ranking or formally checking candidate solutions in other reasoning domains.Examples include execution, deduction, satisfiability, logical inference, and geometry systems.
- Causal proof checking: DoVerifier checks causal expressions against graphs, whereas CALVER treats each sampled expression as its own proof target for reference-free selection.The paper uses an independent prover as corroboration without reusing its checker.
- Alternative architecture: Extract-then-solve constructs one global graph and solves the query exactly, while CALVER selects among candidates whose interpretations may differ.The crossover study measures when each architecture is preferable.
Method
CALVER scores structured sampled traces against an executable causal specification and deterministically selects the highest-scoring candidate. Verification can use a supplied graph or each trace’s constructed graph, with task-specific checks governing semantic validity.
- Setting and trace contract: Each problem supplies a query and either a source graph or text from which the model must construct a graph, then samples K independent traces.In constructed-graph mode, the source graph remains hidden until selection and final grading.
- Setting and trace contract: On find-one-valid queries, a candidate is correct when it belongs to the full graph-valid answer set, not merely when it matches the dataset’s listed example.The listed answer is only one possible valid member.
- Verification modes: Constructed-graph verification scores a trace relative to its own proposed graph, while grading later uses the hidden source graph.The same candidate-local design extends to a truth-table engine for the Knights and Knaves study.
- Trace contract: Each trace uses six typed slots: graph, query, strategy, derivation record, computed result, and answer.The semantic certificate is carried by the graph, query, strategy, computed-result, and answer checks, while the derivation check verifies provenance and format.
- Graph-dependent verification: Task-specific checks cover backdoor adjustment, conditional independence, mediator witnesses, intervention reachability, and numerical ATE consistency.The checks are fixed before evaluation and run on the relevant verification graph.
- Selection rule: The deployed selector returns the earliest trace attaining the maximum of six deterministic check scores.The maximum score is a ranking signal, while strict ATE certification adds guards required by the soundness theorem.
- Selection rule: Score and plurality ties use fixed earliest-occurrence rules, and a mechanical firewall withholds correctness and benchmark-reference fields until selection is complete.At K = 8, symbolic verification adds about 7% over the generation cost already paid by plurality.
Theory
The theory formalizes causal best-of-K selection around decidable validity checks and proves when verification can certify threshold decisions. It also explains how fragmented valid-answer mass makes plurality inconsistent, while graph recovery need only preserve query-relevant relations.
- Theory: CALVER’s trace contract uses six deterministic checks computed from the trace and verification graph, without consulting a target label.Missing or duplicate slots fail their corresponding components.
- Theory: Any binary ATE trace satisfying the strict certificate has the correct final threshold decision when the supplied DAG and observational distribution are correct and positive.The certificate relies on treatment exclusion, d-separation, adjustment, positivity, and a strict decision margin.
- Theory: Plurality becomes inconsistent when one invalid answer has greater probability mass than every individually supported valid answer.Theorem 2 bounds each valid answer’s chance of tying or exceeding the invalid answer and applies a union bound across supported valid answers.
- Theory: With valid mass ρ = 0.6 split across M = 4 strings, exact plurality converges to an invalid answer despite valid answers being sampled with probability 0.6.An ideal validity-separating verifier instead succeeds whenever at least one valid candidate appears, with probability 1 −(1 −ρ)^K.
- Theory: Text-based graph verification need not recover every edge; it must preserve the relations determining the queried predicate.For backdoor sets, these include treatment exclusion, descendant status, and d-separation in the mutilated graph; query-irrelevant errors may leave decisions unchanged.
Experiments
Experiments evaluate CALVER on matched causal pools, external graph and logic tasks, graph-from-text settings, and mechanism audits. Across these settings, candidate-wise symbolic verification generally outperforms plurality and generic scorers, with the strongest advantage when valid answers fragment or graph extraction is unreliable.
- Error analysis: CALVER repairs 197 plurality errors and introduces 54 errors across 576 valid-containing pools, yielding 3.6 repairs per new error and a 24.8-point net gain.Invalid answers are uniquely plural in 226 of those pools, and CALVER selects a valid object in 68.6% of them.
- Matched-pool comparisons: 42.1% CALVER accuracy exceeds the reward model’s 30.5% on identical frozen CLEAR pools, while a structure-only selector reaches 23.5%.The advantage over exact plurality is 11.3 percentage points, and a 72B judge ties plurality.
- Sampling scaling: CALVER’s SFT-policy accuracy rises from 20.6% at K = 1 to 57.9% at K = 32, while plurality reaches 32.5% and stops improving after K = 16.The gap grows from 7.7 points at K = 2 to 25.4 points at K = 32.
- External transfer: On independently sourced causal structures and K&K logic puzzles, matched symbolic verification transfers across representations, graph families, model families, and truth-table checking without task-specific fine-tuning.The checker is matched to each task’s executable predicate.
- Graph construction from text: Graph-from-text recovery falls to 37% and 34% at L2 and L3, yet CALVER retains gains of 14.2 and 17.6 percentage points over plurality.At L3, candidate-wise verification slightly exceeds extract-then-solve on the common executable stratum, 85.6% versus 83.7%.
- Mechanism and ATE audits: The strict ATE audit finds no incorrect trace passing its certificate, while CALVER gains 13.7 percentage points over exact plurality on the declared-margin stratum.All 51 incorrect maximum-score traces violate at least one strict guard.
Limitations & Conclusion
CALVER aggregates candidates through executable validity predicates rather than answer-string frequency. Its benefit is regime-bound: it is most appropriate when many answers are valid and no single text-to-graph extraction is dependable.
- Conclusion: CALVER’s candidate-wise principle applies across graphical criteria and truth-table consistency when the validity predicate can be executed.The reported scope includes causal graphs and Knights-and-Knaves logic.
- Limitations: When answers are near-unique, best-of-K suffices; when text-to-graph extraction is reliable, extracting one graph and solving directly is preferable.CALVER targets the intermediate regime where many answers are valid and no single extraction is dependable.
Supplementary Document for When Many Answers Are Valid, Voting Fails: Symbolic Verification for Best-of-K Causal Reasoning in LLMs
The supplement provides proofs, complete tables, checker tests, and replication details.
- The supplement contains theorem proofs, full tables behind summary numbers, checker checks, and replication details.
Overview
The supplementary materials clarify score terminology and reporting conventions. They distinguish the deployed maximum score from the narrower strict ATE certificate and explain how gains and accuracy comparisons should be interpreted.
- Terminology: A candidate pool is the ordered set of traces sampled for one problem.
- Terminology: The maximum deployed score is the ordinary six-component score, whereas a strict ATE certificate adds treatment-exclusion and decision-margin conditions.
- Reporting conventions: Gains use unrounded values, and accuracy figures are directly comparable only when they come from the same underlying model-output sample.Results identify their source when samples differ.
The CALVER Checker
CALVER checks structured causal traces against typed graphs and query-specific predicates, then selects the highest-scoring candidate without relying on a reference answer.
- Each causal problem contains a typed graph and query, or a text description from which each trace constructs a graph.
- The checker supports DAGs with d-separation, ADMGs with m-separation, and directed-cycle queries with reachability and cycle witnesses.
- Correctness is query-specific: valid answers satisfy the declared graph predicate, while numeric answers satisfy the tolerance and decision rule.
- Each trace is parsed into six typed components, whose binary checks are summed into a score S(r).The components include the graph, query, strategy, and derivation record, followed by result recomputation and final-answer consistency checks.
- The selector returns the earliest trace attaining the maximum deployed score, using a globally fixed tie rule.The maximum score is a ranking signal; the strict ATE certificate adds additional soundness guards.
- The modular checker assigns each task a parser, semantic predicate, and result-consistency function, while unregistered tasks fail closed.
- DoVerifier independently searches for proof of each candidate’s target rather than using the reference target.
A worked example with several valid answers
The worked example shows why answer-frequency voting can select an invalid adjustment set when several distinct valid sets satisfy the query.
- Both {U} and {U, P} are valid answers for the requested backdoor adjustment query.
- The checker evaluates each candidate through parsing, graph and query binding, strategy validation, derivation checks, recomputation, and final-answer consistency.
- Candidate scores sum six binary checks, and the selector returns the earliest candidate with the highest score.
- Exact voting selects {M} from three copies even though four traces contain valid adjustment sets.The set {M} is invalid because M is a descendant of X, while the empty set leaves the X → U → Y path open.
What a selector receives
Selectors receive normalized candidate pools with answer-revealing fields removed, while paired evaluation preserves common inputs and clustered problem-level resampling.
- The export removes benchmark answers, correctness flags, canonical adjustment sets, and analysis-only fields before scoring.The stripped pool is hashed, and correctness fields are restored only after every selector returns an index.
- The six-component scoring table illustrates how distinct valid sets can be accepted without a canonical reference string.
- Bootstrap draws resample problem identities while retaining all seed observations associated with each problem.All methods in paired comparisons receive identical candidate texts in identical order.
What the checker sees and what grades it
The evaluation distinguishes the formal object available to a selector from the object used for grading, separating candidate-local verification from source-structure correctness.
- Each experiment states which formal object is available during selection and which object grades the returned answer.
- Supplied-graph CLEAR gives every selector the same graph and candidates, and both selection and grading use the published graph predicate.
- 42.1 and 23.5 measure the ranking-rule spread under one shared correctness criterion.The predicate admits more valid objects than any single reference string; 11 of 21 audited selections satisfy it while differing from the listed answer.
- In bnlearn and graph-construction experiments, candidates are verified against their reconstructed graphs but graded against an unseen source graph.In K&K, a truth-table engine checks each candidate’s restated formulas, while grading uses the benchmark’s unique solution.
Runtime
CALVER improves causal best-of-K selection while adding modest CPU overhead, with gains supported by validity-aware comparisons, scaling behavior, and audits of its causal signal.
- Runtime: 7% is the additional cost of complete symbolic scoring at K = 8, with individual traces scored in 1–8 ms on one CPU thread.Learned reward models and language-model judges require an additional neural forward pass per candidate.
- Mechanism: A score-separating verifier succeeds whenever any valid answer appears, with probability 1 −(1 −ρ)^K, whereas plurality can converge to an invalid mode.This mechanism arises when multiple valid answers fragment probability mass across answer strings.
- Comparative performance: 42.1% accuracy is achieved by CALVER versus 30.5% for the learned reward model on identical frozen candidates.Exact plurality reaches 30.9%, while the LLM judge reaches 27.4% and model confidence 30.1%.
- Ablation: The causal predicate, rather than parsing or formatting checks alone, accounts for the gain: the structure-only control reaches 23.5% versus CALVER’s 42.1%.The structure-only control removes semantic validity while retaining parsing, binding, derivation, and answer-format checks.