Certified Contrast Explanations for Neuro-Symbolic Treatment Effect Models

We study treatment-effect models through four desiderata: predictive adequacy, intrinsic interpretability, effect-specific informativeness, and verifiable fidelity. Our models combine sparse modified Łukasiewicz logic circuits with compact symbolic refinements discovered from held-out residuals. Logic-S shares one circuit across treatment arms. Hard literal selection controls circuit complexity, while the refinement adds expressive capacity through a few permitted nonlinear terms. We introduce a contrast-aware pruning certificate that identifies shared outcome structure whose deletion preserves the fitted treatment effect throughout a declared input domain. The guarantee accounts for nonlinear clamps, outcome scaling, crossfit aggregation, and accepted symbolic corrections. We evaluate this architecture on 1,000 IHDP simulations and 135 ACIC variants; paired IHDP ablations show that symbolic refinement improves the centered effect surface. In an audit of 30 IHDP simulations, Logic-S ensembles permit a median 77.4% reduction in logically simplified base-circuit nodes at zero certified contrast error; a matched outcome-preserving control permits no further deletions. A historical stroke-trial case study illustrates how to compare estimators against randomized outcomes, inspect the learned benefit structure, and verify that the simplified explanation preserves the fitted contrast. Exact specialization of a factorial Logic-S fit separates aspirin, heparin, and interaction contrasts. It estimates a 1.55-point aspirin risk reduction against a randomized 1.99-point estimate, a near-zero net heparin effect, and aspirin–heparin interactions whose five-seed consensus is bounded throughout the input box within 0.24 percentage points of zero. A separate compact aspirin fit exposes output saturation as the source of its small displayed variation.