An Execution Contract for Law-Preserving Row Eviction in Verifier-Guided Sequential Monte Carlo

A language model generating candidates in a batch may keep computing after they finish or can no longer succeed. Verifier-guided sequential Monte Carlo (SMC) weights candidates using external checks. We specify how to remove unnecessary model rows while preserving selection weights, score updates, and next-token probabilities. Under this execution contract, we prove that row removal preserves the output distribution and test agreement under shared randomness. A deterministic reference produces identical candidates with positive weight and identical selected outputs across four execution policies on 219 of 256 Python tasks. None of the policies retains a candidate with positive weight on the other 37 tasks. Across four benchmarks, removing finished rows saves 32.4 to 45.4% of model-row evaluations. Removing candidates whose zero weight cannot be repaired adds statistically resolved savings on arithmetic tasks, including fresh problems and harder variants. Additional savings remain unresolved on code and database queries. Throughput comparisons are descriptive because the policies reach different peak numbers of resident rows.