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

arXiv: https://arxiv.org/abs/2607.20474 · HTML: https://mlsanity.com/paper/2607.20474/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 19 of its 31 references that are in the map.
- First posted on arXiv 24 May 2026.

## Builds on (most cited first, 19 of 19)

- [DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning](https://mlsanity.com/paper/2501.12948/) (2025)
- [Reflexion: Language Agents with Verbal Reinforcement Learning](https://mlsanity.com/paper/2303.11366/) (2023)
- [Teaching Large Language Models to Self-Debug](https://mlsanity.com/paper/2304.05128/) (2023)
- [Large Language Models as Optimizers](https://mlsanity.com/paper/2309.03409/) (2023)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [Leveraging Pre-trained Large Language Models to Construct and Utilize World Models for Model-based Task Planning](https://mlsanity.com/paper/2305.14909/) (2023)
- [NL4Opt Competition: Formulating Optimization Problems Based on Their Natural Language Descriptions](https://mlsanity.com/paper/2303.08233/) (2023)
- [OptiMUS: Scalable Optimization Modeling with (MI)LP Solvers and Large Language Models](https://mlsanity.com/paper/2402.10172/) (2024)
- [SatLM: Satisfiability-Aided Language Models Using Declarative Prompting](https://mlsanity.com/paper/2305.09656/) (2023)
- [LLMOPT: Learning to Define and Solve General Optimization Problems from Scratch](https://mlsanity.com/paper/2410.13213/) (2024)
- [A Survey of Contextual Optimization Methods for Decision Making under Uncertainty](https://mlsanity.com/paper/2306.10374/) (2023)
- [A Systematic Survey on Large Language Models for Algorithm Design](https://mlsanity.com/paper/2410.14716/) (2024)
- [Large Language Models for Supply Chain Optimization](https://mlsanity.com/paper/2307.03875/) (2023)
- [LLM-ARC: Enhancing LLMs with an Automated Reasoning Critic](https://mlsanity.com/paper/2406.17663/) (2024)
- [LLMLOOP: Improving LLM-Generated Code and Tests through Automated Iterative Feedback Loops](https://mlsanity.com/paper/2603.23613/) (2026)
- [Instantiation-based Formalization of Logical Reasoning Tasks using Language Models and Logical Solvers](https://mlsanity.com/paper/2501.16961/) (2025)
- [Validating LLM-Generated Programs with Metamorphic Prompt Testing](https://mlsanity.com/paper/2406.06864/) (2024)

## Built on by (most cited first, 2 of 2)

- [Admission Without Answers: Label-Free Certification and Experience Learning for LLM-Based Optimization Modeling](https://mlsanity.com/paper/2608.15565/) (2026)
- [OR for AI That Does OR: Routing LLMs up the Escalator inside the OSCAR Framework](https://mlsanity.com/paper/2610.00912/) (2026)

## Abstract (arXiv)

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.