Beyond Solver Acceptance: Auditing Autoformalized Biomedical Claims

A solver establishes a result for its input formula, not automatically for the scientific claim that motivated it. We audit this gap in neuro-symbolic reasoning about biomedical ordinary differential equations, separating source fidelity, target correspondence, and evidence applicability. In a controlled $24$-target experiment, constrained SMT generation makes every query executable, but only $9/24$ Qwen3-8B and $1/24$ OLMo-3-7B queries have the target counterexample set. In a source-dependent $60$-target experiment, two formalizations agree on $48$ and $37$ tasks, yet both fail to match the target on $34$ and $28$ agreeing pairs. A full audit of all $792$ frozen outputs finds target-applicable evidence for $9/44$ Qwen and $18/49$ OLMo incorrect first candidates. The audit diagnoses correspondence and evidence applicability separately. The evaluation uses controlled tasks from three sources, with exact reference targets and an explicitly bounded source-checking fragment.