Cross-Family Symbolic Verification for Contamination-Robust Selective Prediction on LLM Math Reasoning
Aayan Alwani ⋅ Ethan Y Wang
Abstract
Trustworthy mathematical reasoning by large language models requires a deployment-time signal indicating which answers should be trusted. Two coupled failure modes obstruct this. Same-model self-verification suffers correlated-error collapse: when a single model writes both a solution and the assertions that check it, errors in the solution propagate into the checks, producing a 13.8% false acceptance rate on MATH-500 that scales monotonically from 1.4% at Level 1 to 30.8% at Level 5. Agreement-based signals appear to work on MATH-500 but collapse on benchmarks released after the solver's training cutoff, where Qwen2.5-Math-7B reproduces 54.6% of MATH-500 verbatim. The present work introduces X-SGRV, a cross-family symbolic verifier in which a large LLM from a different family than the solver reads only the problem statement and emits a SymPy verify(answer) function executed in a sandboxed subprocess. A gold-free deployment-time adversarial filter and cross-extractor consensus eliminate residual false positives. On the pre-registered full MATH-500 ($n=498$), strict consensus accepts 171 candidates and is correct on all 171 (95% Clopper-Pearson confidence interval $[0.979, 1.000]$) at 34.3% coverage. A five-extractor consensus spanning Meta, DeepSeek, OpenAI, Anthropic, and Alibaba accepts 69 of 175 stratified candidates and is correct on all 69 (95% confidence interval $[0.948, 1.000]$). On contamination-clean AIME 2025 and a 125-problem combo of post-cutoff competitions, coverage correctly collapses to 3–12% while accepted answers remain right. At matched coverage, X-SGRV ties Skywork-o1-Open-PRM and doubles Qwen2.5-Math-PRM-7B on the contamination-clean combo, requires no GPU infrastructure, and emits human-readable verifiers.
Chat is not available.
Successful Page Load