Minimum-Cost Robust Evidence Certificates for Horn Reasoning under Correlated Source Failures

Yukun Yang

cs.AIOct 19, 2026

Minimum-Cost Robust Evidence Certificates for Horn Reasoning under Correlated Source Failures

Authors: Yukun Yang

Organizations: School of Management, Beijing Institute of Technology

Abstract

A small justification for a rule-based conclusion may disappear when a source is withdrawn, and multiple derivations need not provide independent evidence. We study minimum-cost certificates that preserve a Horn conclusion under every withdrawal of at most k source domains. Evidence records remain distinct from asserted facts, supporting replicated attestations and overlapping failure dependencies. Transversals of minimal-support footprints characterize robustness and explain why disjoint-proof requirements can reject valid certificates. An exact procedure alternates weighted evidence selection with a source-failure oracle. A rule-closed counterinterpretation yields a globally valid selection cut without enumerating supports or failure scenarios. We prove correctness, finite termination, and cost optimality, establish coNP-completeness of unrestricted verification and NP-completeness of synthesis for every fixed budget, and identify a tractable reachability restriction. Experiments on controlled benchmarks, reachability graphs, and ontology-derived instances demonstrate that our counterinterpretation-guided synthesis achieves up to 92% optimum coverage within practical resource bounds, outperforming scenario expansion and general abduction while confirming the necessity of transversal-based reasoning over proof-packing heuristics.

Figures & tables

Figure 1: Running-example support footprints, their shared domains, and a surviving justification for each admissible single-domain withdrawal.

Controlled Horn Systems ( $\|\mathcal{E}\|\leq 512,k\in\{1,2,3\}$ )
Method	Feasible Cost	Opt. Coverage	Proven Infeas.	Runtime (s)	Peak Mem. (MB)
Nominal ( $k=0$ ), checked at $k$	$8.4\pm 1.6^{\dagger}$	0 4.2%	–	00 $0.4\pm 0.1$	00 $24\pm 5$
Domain-disjoint packing	$26.8\pm 4.3$	31.5%	–	0 $18.2\pm 5.4$	00 $68\pm 14$
Explicit scenario synthesis	$23.2\pm 3.7$	46.8%	100.0%	$184.6\pm 42.1$	$2,840\pm 620$
Provenance compilation	$22.6\pm 3.5$	39.2%	0 85.0%	$210.4\pm 51.3$	$1,920\pm 450$
Compiled weighted abduction	$21.9\pm 3.4$	61.4%	100.0%	0 $95.7\pm 22.8$	0 $410\pm 85$

Table 1: Main performance comparison across benchmark families. Feasible cost reports mean

\pm

std over instances where methods found verified certificates ( † nominal support only satisfies

k=0

and fails robustness check on 95.8% of instances; unresolved instances for exact baselines report best verified incumbents). On the common subset of instances solved to certified optimality by all exact methods, their optimal costs are strictly identical (

16.4\pm 2.5

for Horn systems,

27.9\pm 4.1

for KB/networks). Optimum coverage and proven infeasibility percentages indicate exact resolution within the 600 s limit.

Variant	Master calls	Oracle time (s)	Cut length	Strengthening time (s)	Total time (s)
Full procedure	$\mathbf{14.2\pm 3.1}$	0 $6.4\pm 1.2$	$\mathbf{12.3\pm 2.1}$	$1.8\pm 0.4$	$\mathbf{19.4\pm 4.2}$
Raw counterinterpretations	$22.8\pm 5.2$	0 $6.1\pm 1.1$	$28.6\pm 4.5$	–	$27.4\pm 6.8$
Candidate exclusion only	$86.5\pm 18.4$	$24.8\pm 5.6$	0 $1.0\pm 0.0$	–	$94.2\pm 21.0$
Without dominance	$19.1\pm 4.0$	0 $7.2\pm 1.5$	$15.8\pm 2.6$	$2.1\pm 0.5$	$24.7\pm 5.3$
Without relevance slicing	$14.6\pm 3.2$	$14.8\pm 3.1$	$12.5\pm 2.2$	$3.9\pm 0.8$	$29.1\pm 6.2$

Table 2: Algorithmic ablation on controlled Horn benchmarks (

|\mathcal{E}|\leq 512,k=2

), showing the effect of cut strengthening, dominance pruning, and relevance slicing on master solver invocations and cumulative runtimes.

Data Provenance

Data provenance tracks where data and AI outputs come from, how they are transformed, and what evidence supports their attribution and use.

See all 191 papers

Certified by Abstention: Distribution-Free Guarantees for Chain-of-Thought Verifiers at Small Calibration Budgets
Oct 7, 2026Arjun BalajiSelective Prediction Conformal Prediction
Columbia University
Knowing When the Evidence Is Enough: Requirement-Directed Search with Horn-Closure Certificates
Oct 26, 2026Xinyu Zhang, Weiwei SunEvidence-Grounded QA Evidence Retrieval
Fudan University
From Reasoning Strings to Partial Orders: Verifier-Certified Rule Transport through Quotient Policy Optimization
Aug 20, 2026Bang Xie, Hao Liu, Zhiyuan Peng +5RL for Language Model Reasoning Reinforcement Learning with Verifiable Rewards
Shanghai Jiao Tong University, Shanghai, China · Zhejiang University, Hangzhou, China

Oct 7, 2026J/K move · Enter open · S save

Certified by Abstention: Distribution-Free Guarantees for Chain-of-Thought Verifiers at Small Calibration Budgets

Arjun Balaji

Columbia University

Selective Prediction Conformal Prediction LLM Abstention CoT Evaluation FDR Control

Open paper AskPDF arXiv

Signals that predict whether a chain-of-thought (CoT) trace is correct are compared by AUC, but deploying one requires a threshold with a guarantee. We ask what distribution-free selective guarantees deliver for CoT verifiers at realistic calibration budgets of tens to a few hundred labelled problems, using seven open models, five verifier signals and 37,000 graded traces. The central observation is validity by abstention: an

(α,δ)

-valid procedure that issues a certificate with probability

P_{\rm fire}

bounds the failure probability of an issued certificate only by

δ/P_{\rm fire}

, so a certificate that rarely fires can be valid and wrong every time it is used. In a simulation with known risk the standard certificate fails in at most 0.3% of calibration draws but in up to 69% of those in which it fires. A certification floor and a lattice condition for Benjamini-Hochberg conformal selection explain why certificates abstain at these budgets, and the data bear them out: the standard certificate returns nothing or a large accepted set, and an unreadable residual-stream probe buys two to three times the coverage of the readable signals, an edge a cross-fitted reconstruction cannot recover linearly from the readable features. We then give a floor-started fixed-sequence certificate, valid without monotonicity assumptions, that covers more than the Bonferroni certificate on every model-signal pair and raises coverage at the non-vacuous target

0.75π_0

from 0.05 to 0.16, although the floor keeps absolute coverage small. Finally, a certificate cannot see what matters after deployment: under benchmark shift the error among accepted traces tracks the new task's base error, and under best-of-

n

selection against the verifier it rises past the target while the empirical failure frequency stays below

δ

, because abstention absorbs the failures.

Abstract

Data Provenance

Explore similar work

Certified by Abstention: Distribution-Free Guarantees for Chain-of-Thought Verifiers at Small Calibration Budgets

Knowing When the Evidence Is Enough: Requirement-Directed Search with Horn-Closure Certificates

From Reasoning Strings to Partial Orders: Verifier-Certified Rule Transport through Quotient Policy Optimization