Symbolic Music Reasoning Needs Checkers That Survive Rewording: What a High Score Covers

On SSMR-Bench, a template-generated benchmark of questions about sheet music in ABC notation, our hand-written music21 checker, developed on the test items, answers 70% of items at 99.8% precision. Prove-then-route systems for symbolic music reasoning build on this: the checker answers the questions it can derive and a language model answers the rest. However, a high score cannot tell whether the checker computes music theory or merely recognizes the benchmark's question templates. Our key idea is that a task-preserving rewording separates the two: a checker that computes should keep its contribution, while one that recognizes wording should lose it as the model's own accuracy stays put. Our audit therefore measures the checker's matched contribution, the system's accuracy minus the same model's alone, before and after such rewording; a normalizer that maps reworded questions back onto the known templates tests whether a loss lies in how the checker reads the question. A checker that Claude Opus 4.8 wrote with execution feedback answers 93.4% of questions at 99.67% precision, yet rephrasing only the question line removes most of its contribution (from +21 to +3–4 points over a Qwen2.5-14B model distilled from DeepSeek-R1 traces) while the model's own accuracy barely moves. Most of that gain sits on outputs the distilled model truncates, yet on the outputs it finishes the smaller gain still falls (both post hoc). Paraphrases by the checker's own writer model also cut its coverage, and mapping them back onto the templates restores every checker answer: under rewording, what breaks is the checker's reading of the question, not its music computation. In logic the failure is worse: on ProofWriter, equivalent rule rewrites make a checker built by the same loop answer wrongly on most items through a silent default “Unknown” (post hoc), pulling the system below the model alone; the published Logic-LM design, run with a Qwen translator, makes the same errors, though its precision holds under rewording. Primary tests were pre-registered with frozen programs, several after the results that motivated them. Where a checker settles part of a task, a prove-then-route result should therefore report its coverage, precision and matched contribution under rewording.