Falsification-Based Verification of LLM-Generated Optimization Models: Sound Test Batteries and Their Detection Limits
Software EngineeringArtificial Intelligence
Summary
The authors study how large language models translate natural language problem descriptions into optimization models, noting that these models can silently produce incorrect formulations. They propose a verification method that tests candidate models by running solver calls on modified instances without needing a correct reference model. Using mathematical concepts like duality and comparative statics, they design different sound tests that can reliably detect errors without false positives. Their experiments confirm that their approach detects many types of errors better than traditional threshold-based testers. They also explain what kinds of mistakes their verification method cannot catch and prove theoretical limitations.
Authors
Haifeng Li, Mo Hai
Abstract
Large language models now translate natural-language descriptions of decision problems into solver-ready optimization models, but they fail silently. A generated model often runs and still formulates the wrong problem. This paper develops a theory of falsification-based verification for this setting. Every numeric quantity in the description is a typed slot, and a candidate model is tested only through solver calls on slot-transformed instances; no reference model or label is consulted. From duality, comparative statics, and polyhedral limit arguments we derive a battery of test classes covering directions, curvature, crush probes, prohibitive limits, annihilation, and exchange. Every test is sound, so a violation certifies unfaithfulness and the false-positive rate is zero by design. We characterize what such verification can never see, give conditions under which the canonical error classes are detected with certainty, and prove that no fixed-threshold perturbation tester is simultaneously sound and nontrivial. Experiments on 326 ground-truth models from NL4OPT and four benchmark families confirm the theory. The battery attains a 0.0% false-positive rate against 54.9% for a threshold tester, detects 70.0% of certified conditional-class mutants, convicts 40.4% of the mutants invisible to execution-accuracy scoring, and reproduces the predicted detectability pattern including its zeros.