Falsification-Based Verification of LLM-Generated Optimization Models: Sound Test Batteries and Their Detection Limits

Large language models now translate natural-language descriptions of decision problems into solver-ready optimization models, and they fail silently. A generated model often runs and still encodes the wrong problem, while standard evaluation compares optimal values against labeled answers that deployment does not provide. How to certify such a model without any reference is the question this paper addresses. We develop falsification-based verification. Every numeric quantity in a problem description plays a role that the text itself states, such as a capacity, a requirement, or a unit cost, and any correct model must respond to changes in these quantities as the stated roles dictate. From duality and sensitivity analysis we derive a battery of solver-based tests that are individually sound, so a violation certifies a faulty model and the false-positive rate is zero by design. We characterize the errors that no test of this kind can see, give conditions under which each canonical error class is detected with certainty, and prove that perturbation testers with tuned thresholds cannot be simultaneously sound and nontrivial. Across 326 ground-truth models, a synthetic family, and four public benchmarks with two generators, the battery flags 0.0% of faithful models while a threshold tester flags 54.9%; it detects 56.1% of core formulation errors, 70.0% under certified preconditions, and 40.4% of the errors that value-based scoring provably cannot see, and it reproduces the predicted detectability pattern including its blind spots. Every flag carries a machine-checkable certificate that localizes the defect, and a full audit costs about 25 millisecond-scale solver calls per model. Classical sensitivity analysis and duality thus offer a rigorous, label-free audit that complements existing evaluation of AI-generated optimization models.