Neuro-symbolic mathematical NLI combines the flexibility of language models with the exactness of formal solvers. The formal guarantee, however, applies only when selected evidence is relevant, generated constraints are faithful, and the solver actually determines the final label. We study credit assignment at this boundary.

We audit a four-stage architecture combining knowledge-infused premise selection, Llama-3-8B-Instruct autoformalization, token-likelihood gating, and Z3 verification. Using the supplied implementation, original 500-example trace, and corrected JSON, we reconstruct the executable routing logic and evaluate selection, formalization, execution, fallback, and final-label correctness as separate stages.

In this synthetic setting, premise selection attains 100.0% precision but 33.4% recall, while the gated and neural-only routes make identical predictions at 81.2 macro-F1 (p=1.0000). On the corrected JSON, a target-group-held-out hypothesis-only rule reaches 96.1 macro-F1, and the hypothesis string accounts for 89.7% of label entropy. These results expose two evaluation risks in this run: fallback can resemble verification, and hypothesis form can support premise-free prediction. We contribute an executable system account, a reproducible grouped shortcut diagnostic, and a trace-provenance checklist. The findings are scoped to the supplied benchmark and execution.