VeriSimpl: Robust Optimization Modeling from Natural Language using Simplification-based Verification
For users of optimization modeling, this work addresses the critical problem of ensuring correctness in natural-language-to-formulation translation, but the approach is incremental as it builds on existing LLM and solver techniques.
VeriSimpl uses simplification-based verification to improve LLM-generated optimization formulations, achieving consistent accuracy improvements over existing methods on benchmarks.
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.