Assumption Laundering in Prover-Certified Process Rewards

Recent work supervises language-model reasoning with a theorem prover: each step is translated into first-order logic, the prover checks that the step's premises entail its conclusion, and the verdict is used as a step-level reward. When the cited premises fall short, some pipelines let the model add an assumption to close the gap. We show that this makes the certificate weaker than it looks, because the model being supervised writes its own obligation: a proof from the model's own axiom is reported as a proof of the model's step, a failure we call assumption laundering. We audit it on 15,733 steps sampled from the base model of a released pipeline on ProntoQA and ProofWriter, whose symbolic generators let us decide both whether a step is valid and whether an assumption is entailed by the problem. Where the cited premises do not entail the conclusion, 87% of accepted certificates hold only because of an assumption the model added, and the certificate cannot tell an assumption the problem entails from one it does not. A model that assumes what it needs to prove is accepted on every step, so no threshold on the verdict can repair this; the assumption has to be licensed by a reference the model does not control. Enforcing this condition raises informedness (acceptance of valid minus acceptance of invalid steps) on ProntoQA from 0.09 to 0.41, and to 0.49 after we also repair a separate compiler defect that we trace to the demonstrations in the released prompt; repairing the compiler alone leaves it at 0.09. A second pipeline that constrains assumptions differently behaves as the condition predicts. Where no reference exists, disallowing assumptions altogether does not give a usable step reward, but it does give a high-precision data filter: 13% of responses kept at 93% answer accuracy against a 72% base rate, ahead of a learned process reward model at the same yield.