VeriSimpl: Robust Optimization Modeling from Natural Language using Simplification-based Verification

Natural language interfaces can greatly benefit the accessibility and usability of optimization modeling, and recent advances in large language models (LLMs) show promise in automatically translating textual problem descriptions into executable solver formulations. However, a key challenge for existing approaches is to ensure that the inferred formulation correctly implements the intended task, even if it may execute without errors. We introduce VeriSimpl, a solver–LLM framework for robust natural-language-to-optimization formalization. Our approach is based on the idea of simplification-based verification, where the optimization solver is leveraged to generate simplified diagnostic queries about a candidate formulation to allow the LLM to tractably reason about the correctness of the formulation with respect to the task description. We present such simplification strategies along different dimensions with respect to problem constraints and decision variables, which allow the LLM to reason locally under fixed global contexts. Evaluations on a range of optimization benchmarks show how our approach provides consistent improvements in accuracy over existing methods, while also providing a novel high-precision self-verification signal.

Optimization tools help people make decisions in areas such as scheduling, logistics, and resource allocation. Recent AI systems can translate problem descriptions written in everyday language into mathematical models. However, a model may still be incorrect even if it runs successfully, because it might not accurately capture the user's intended task. We introduce VeriSimpl, a framework for verifying whether AI-generated optimization models faithfully represent the original problem description. Instead of asking the AI to analyze a complex model all at once, VeriSimpl uses an optimization solver to create simpler diagnostic problems that are easier to reason about. These simplified checks allow the AI to examine specific parts of the model and identify errors that might otherwise be missed. By combining solver-generated diagnostics with AI reasoning, VeriSimpl provides a reliable way to verify optimization formulations. Experiments on multiple benchmarks show that VeriSimpl improves the accuracy of optimization formulations generated from natural-language descriptions while providing a highly reliable signal for detecting incorrect formulations, helping bridge the gap between natural-language problem descriptions and trustworthy optimization models.