Executable but Wrong: Verifier-Grounded Contracts and Counterexamples for LLM-Generated Music Programs

Abstract

A generated program can compile, execute, and still be wrong in the only way its user cares about. This is common in creative domain-specific languages: the artifact is partly subjective, yet requests often contain objective promises such as a tempo, onset grid, pitch range, or event count. Ordinary compilers establish executability, while self-critique leaves the model to invent its own oracle.

We present StruSpec, a verifier-grounded workflow for LLM-generated Strudel music programs. It turns explicit promises into bounded executable contracts, evaluates a deterministic Strudel subset with exact rational time and source provenance, and returns typed counterexamples to a preservation-aware repair loop. The model proposes patches; only re-execution and verification can end the loop. We validate the semantic boundary against the official runtime, an independently implemented semantics, generated oracles, metamorphic relations, controlled faults, and reviewed natural programs.

The evaluation separates four questions that are often conflated. Across 4,000 generations, 81.03% compiled but only 15.98% satisfied every hard constraint. On 600 paired failures, localized counterexamples improved strict repair success by 10.83 percentage points with GLM-5.2 (95% CI 8.17–13.67) and by 14.83 points in a protocol-matched DeepSeek V4 Pro replication (11.83–17.84). On a new 192-request, author-confirmed expert population, localized repair also beats generic feedback with both GLM (17 vs. 0 repairs) and DeepSeek (12 vs. 1), although only 67 requests reach a complete-trace semantic violation. A symbolic-first variant used 78.7% fewer model calls and 67.2% fewer output tokens, although its typical successful patch was no smaller. Conversely, supplying the same structured contract before any failure reduced first-attempt satisfaction: 23.17% for direct generation, 18.67% with a gold contract, and 17.54% with a parsed contract. The combined evidence reveals a phase asymmetry: structure is valuable when independent execution turns it into new diagnostic evidence, not when a redundant schema is merely placed in front of a generator.