OPTIMAL FOR WHICH MEANING?

An optimization solver can solve a model correctly even when the model does not match what the user means. We study when different meanings change the recommended decision and when they can be left unresolved. We make three contributions. First, we separate three checks: whether the model expresses its stated assumptions, whether it is solved correctly, and whether its answer meets the user’s requirements. Second, we give a rule for stopping clarification: the same action must satisfy every interpretation being considered and stay within an agreed loss limit. For problems with the same objective, this rule can reuse an optimization bound instead of solving every interpretation separately. Third, we test these ideas on existing model outputs and small controlled studies. In one production problem, an action that was optimal under the model’s assumption earned 1,000 less under the cost rule confirmed by our collaborator. In six test cases, reusing bounds reduced verification solves from fourteen to six with the same fifteen valid stopping decisions. Giving the language model mathematical evidence helped one earlier task but did not consistently improve later corrections. Our results show why evaluation should check assumptions and decisions, not only the final objective value. Guarantees remain limited to the interpretations that were checked.