Right Answer, Wrong Model: Verifying LLM-Generated Optimization Models

LLMs are increasingly used to translate natural-language problems into mathematical optimization models and are typically evaluated by whether the generated model attains the reference optimal objective value. This paper studies silent errors: generated models that return the correct optimal value while encoding an incorrect feasible region. Across 7 LLM generators on 40 problems selected to stress formulation correctness, 14.9% of objective-matching outputs contain silent errors; among the six generators that produce correct formulations, rates range from 7.2% (GPT-5 Mini) to 25%. These errors concentrate in constraints and variable domains, so objective-value accuracy can overstate formulation quality. Existing verifiers typically return a verdict or a relation-level profile rather than naming the violated requirement with checkable evidence. This paper introduces SILENTOR, a solver-backed verifier that checks a candidate model one requirement at a time. Behavioral requirements are compiled into executable probes, and a solver searches for a witness: a solution the candidate admits but the requirement forbids. Declared-type requirements that can be decided directly from the candidate's declarations bypass probe generation and are checked structurally. A violation is reported only with a confirmed witness or an offending declaration; otherwise the requirement is unresolved. On 49 silent-error cases with 89 requirement violations, SILENTOR raises requirement precision from 66.4% to 96.2% over a single-agent baseline at comparable recall, reaching 98.1% on naturally occurring errors. On 36 certified-correct models, false-positive rates fall from 33.3% for direct inspection to 16.7% with supplied requirements and 5.6% for SILENTOR. SILENTOR turns requirement-level predictions into localized, solver-checkable evidence.