PaperlayerView exact revision on arXiv

Source-linked AI summary

Autoformulation of Mathematical Optimization Models Using LLMs

Nicolás Astorga, Tennison Liu, Yuanzhang Xiao, Mihaela van der Schaar

arXiv:2411.01679v2cs.LG

TL;DR

Translating natural-language problems into correct optimization models remains difficult and demands specialized expertise. The paper uses LLMs with hierarchical MCTS, symbolic pruning, and LLM-based evaluation to explore formulations; experiments report superior performance and gains from pruning and evaluation on real-world benchmarks.

  • Problem

    Autoformulation must search a vast, problem-dependent space under uncertainty and redundancy, while determining whether a candidate formulation faithfully captures the intended problem remains difficult.

    Source: §1 · p. 1, §2.2 · p. 3

  • Method

    The method uses LLMs to generate and evaluate partial formulations within hierarchical MCTS, with SMT-based pruning to remove equivalent hypotheses.

    Source: §1 · p. 2, §3.2.1 · p. 5, §3.2.2 · p. 5

  • Results

    The method demonstrates superior performance on real-world benchmarks containing linear and mixed-integer programming problems, with gains from search pruning and LLM-based formulation evaluation.

    Source: §1 · p. 2, §6 · p. 9

  • Takeaways & Limitations

    The benchmark findings support pruning and LLM-based correctness evaluation as useful components for improving formulation efficiency in the tested setting.

    Source: §6 · p. 9

    SMT equivalence checks may be undecidable for some mixed-integer or nonlinear functions, so uncertain cases are treated as distinct and pruning is limited to levels m2–m4.

    Source: §3.2.1 · p. 5

Abstract

from arXiv · show

Mathematical optimization is fundamental to decision-making across diverse domains, from operations research to healthcare. Yet, translating real-world problems into optimization models remains a difficult task, often demanding specialized expertise. This paper approaches the problem of $\textit{autoformulation}$: the automated creation of solver-ready optimization models from natural language problem descriptions. We identify three core challenges of autoformulation: $\textit{(1)}$ the vast, problem-dependent hypothesis space, $\textit{(2)}$ efficient and diverse exploration of this space under uncertainty, and $\textit{(3)}$ evaluation of formulation correctness against problem description. To address these challenges, we present a novel method leveraging $\textit{Large Language Models}$ (LLMs) with $\textit{Monte-Carlo Tree Search}$, exploiting the hierarchical nature of optimization modeling to generate and systematically explore possible formulations. To enhance search efficiency, we introduce symbolic pruning to eliminate trivially equivalent search paths (branches), and employ LLM-based evaluation of partial formulations to guide search. Empirical analysis on linear and mixed-integer programming benchmarks demonstrates our method's effectiveness, with significant performance gains from both LLM-based value estimation and symbolic pruning techniques.

1. Introduction

Autoformulation aims to automate the translation of natural-language problems into optimization models, a process that still relies heavily on human expertise. The paper frames this as a search problem and combines LLMs with Monte-Carlo Tree Search (MCTS), symbolic pruning, and LLM-based evaluation; experiments report superior performance and gains from pruning and evaluation.

Introduction

  • Autoformulation remains largely human-driven despite mature solving algorithms, motivating automation that could reduce modeling effort and broaden access to optimization tools.The paper notes potential benefits for rapid prototyping and iteration, and for domain experts working without deep optimization expertise.Source: §1 · p. 1
  • The search must handle a large, problem-dependent space, balance exploration under uncertainty and redundancy, and evaluate whether formulations match real-world requirements.Solvers can assess optimality and computational efficiency, but not reliably whether a formulation faithfully captures the intended problem.Source: §1 · p. 1, Figure 1 · p. 2

Key considerations

  • The method combines hierarchical MCTS exploration with LLM-generated formulations, SMT-based pruning of equivalent hypotheses, and LLM evaluation of correctness to guide search.LLMs generate diverse component formulations, while solver feedback is combined with correctness evaluation to guide exploration.Source: §1 · p. 2

Contributions

  • The paper formalizes autoformulation as a search problem and identifies its core challenges as contributions alongside its LLM-and-MCTS approach.The supplied contribution passage is partial and does not provide further details.Source: §1 · p. 2

Introduction

  • Experiments on two real-world benchmarks containing linear and mixed-integer programming problems report superior performance, with gains from both search pruning and LLM-based formulation evaluation.The paper also identifies LLMs’ language understanding, domain knowledge, and in-context reasoning as capabilities relevant to autoformulation.Source: §1 · p. 2

2. Autoformulation: Towards Automated Optimization Modeling

The section characterizes optimization models through objectives, constraints, and feasible regions, then defines autoformulation as transforming natural-language descriptions into mathematical formulations. It presents mathematical formulation as the first stage of the process.

2. Autoformulation: Towards Automated Optimization Modeling

  • Optimization models minimize an objective subject to constraints, and the feasible region contains the points satisfying the inequality and equality constraints.The section also notes that convexity permits global optimality from local optima and can allow specialized solvers to solve convex problems efficiently.Source: §2 · pp. 2–3

2.1. Problem Definition

  • Autoformulation is the automated transformation of natural-language descriptions of real-world problems into formal optimization models.The section motivates this automation by observing that formulation remains largely dependent on human expertise.Source: §2.1 · p. 3
  • The formal definition represents mathematical formulation as a transformation from problem descriptions into a probability distribution over mathematical formulations.The passage names this transformation pϕ: D → P(M).Source: §2.1 · p. 3

2. Computational representation pψ

The section separates mathematical formulation from computational representation and describes how autoformulation quality can be evaluated. It highlights challenges in searching a problem-dependent space and assessing whether candidate models faithfully represent requirements.

2. Computational representation pψ

  • Computational representation converts a mathematical formulation into solver-suitable formats, including a programming framework and choice of solving algorithm.The section notes that mathematical formulation is generally more challenging than computational modeling, though algorithm and hyperparameter choices remain challenging.Source: §2 · p. 3
  • Autoformulation represents the two transformations jointly as pϕ,ψ(m, c | d) = pψ(c|m)·pϕ(m|d), with an autoformulator seeking formulations that maximize an evaluation measure Q.Q assesses the quality of the mathematical and computational models relative to the problem description.Source: §2 · p. 3
  • Evaluation can measure formulation correctness, optimality gap, and computational efficiency, with efficiency potentially varying across equivalent formulations.The section treats correctness as accuracy in reflecting problem requirements.Source: §2 · p. 3

2.2. Challenges

  • The hypothesis space includes interdependent, problem-specific variables, constraints, and objectives; sparse good formulations, uncertainty, and trivial equivalences make efficient search difficult.Trivial equivalences include syntactically different but functionally identical expressions, while correctness remains difficult to assess against intended requirements.Source: §2.2 · pp. 3–4
  • Autoformulation difficulty varies with problem characteristics, particularly convexity: some problems permit direct global solutions, while others require convex reformulations or relaxation strategies balancing optimality and efficiency.Source: §2.2 · p. 4

3. LLM-Enhanced MCTS Search for Autoformulation

The paper casts autoformulation as a hierarchical search problem and uses LLM-guided Monte-Carlo Tree Search (MCTS) to explore formulations. It combines symbolic pruning with partial and complete formulation evaluation to guide that search.

3.1. Hierarchical Decomposition

  • A depth-four MCTS tree searches sequentially over parameters and decision variables, the objective, equality constraints, and inequality constraints.Each complete formulation is a path from the root to a terminal node.Source: §3.2 · p. 4, §3.1 · p. 4

3.2.1. EXPANSION

  • LLMs generate diverse next-component formulations conditioned on the problem description and the current partial formulation.Expansion samples candidate components from the LLM and prunes trivially equivalent candidates, using SMT checks for objective and constraint components.Source: §3.2.1 · p. 5
  • SMT pruning may leave redundant paths when equivalence is undecidable, and it is applied only to objective and constraint levels with shared decision variables.Undetermined equivalence is conservatively treated as distinct; variable-definition candidates are pruned using an LLM instead.Source: §3.2.1 · p. 5

3.2.2. EVALUATION

  • LLMs rank newly expanded partial formulations on correctness, feasibility, and alignment with the problem, and normalized scores initialize child values.The search retains the top I candidates by normalized rank.Source: §3.2.2 · p. 5, Figure 2 · p. 5

3.2.3. DUAL REWARDS AND BACKPROPAGATION

  • Complete formulations receive a dual reward combining LLM-assessed mathematical correctness with binary solver feedback on whether the computational model solves optimally.Solver success is imperfect evidence: an incorrectly formulated model can still solve optimally.Source: §3.2.3 · pp. 5–6
  • For terminal-model correctness, comparative LLM scoring against consistent baseline models replaces independent scoring, which showed mixed results and scoring inconsistencies.A score above 0.5 indicates preference for the candidate over the baseline.Source: §3.2.3 · p. 6

3.2.4. SELECTION

  • Terminal rewards update node values by backpropagation, while UCT selection balances high-value nodes against less-visited nodes during subsequent exploration.Selection uses a value combining the LLM-initialized prior and the backpropagated estimate.Source: §3.2.3 · p. 6, §3.2.4 · p. 6
  • After T iterations, the algorithm returns up to T functionally distinct models; its deterministic parser handled experimental problems, though more complex transformations may need more sophisticated approaches.Search pruning produces the functionally distinct outputs.Source: §3 · p. 4, §3.2.4 · p. 6

4. Related Work

Related work spans LLM applications in reasoning and optimization, autoformulation systems, and LLM-guided planning and search. This paper distinguishes its approach by using hierarchical MCTS, symbolic pruning, and comparative or ranking-based correctness evaluation.

Advances in LLMs

  • LLMs have been studied for reasoning, coding, optimization, and search; this work focuses on translating natural-language descriptions into formal optimization models.The cited optimization applications include Bayesian, prompt, evolutionary, and symbolic program optimization.Source: §4 · p. 6

Autoformulation

  • Prior autoformulation work includes a linear-programming competition with format-specific prediction, multi-agent LLM systems that generate and refine formulations, and an optimization-modeling LLM fine-tuned on real and synthetic data.The paper differentiates its approach through component-wise MCTS exploration, symbolic pruning, and composite rewards.Source: §4 · p. 6

Planning

  • Related planning methods generate and select among multiple plans, including LLM-guided MCTS; this work instead emphasizes hierarchical search, SMT pruning, and comparative or ranking-based correctness evaluation for autoformulation.Prior methods evaluate plans using environment feedback or LLM self-evaluation.Source: §4 · pp. 6–7

5. Experiments

The experiments benchmark autoformulation on four real-world datasets and examine benchmark accuracy, correctness evaluation, search efficiency, and performance and error patterns.

5.1. Benchmark Comparisons

  • With three rollouts, the method surpasses all baselines, including finetuned ORLM, after matching baseline performance with one rollout.Further rollouts improve accuracy, but gains taper with increased computational cost; results use Pass@N across up to 16 rollouts.Source: §5.1 · p. 7

5.2. Formulation Correctness Evaluation

  • Comparative scoring separates correct from incorrect IndustryOR formulations more reliably than direct scoring: biserial correlation 0.48 versus 0.23.The comparative approach yielded p-value 2.0681e−3; direct scoring yielded p-value 1.1185e−1.Source: §5.2 · p. 8
  • Greedy formulations guided by partial-formulation prior scores were significantly more accurate than random solutions, with the gap growing as tree diversity increased.The comparison used a fully expanded depth-first tree with up to three children per node.Source: §5.2 · p. 8, Figure 3 · p. 8

5.3. Gains in Search Efficiency

  • Symbolic pruning retained about 20% of candidate formulations on average, and the non-hierarchical search required 1000x more generations for the same number of unique formulations.Top-three selection by normalized rank scores further reduced the candidates after pruning.Source: §5.3 · p. 8, Figure 4 · p. 8

5.4. Performance Analysis

  • On IndustryOR, additional MCTS rollouts consistently found correct formulations, but the final four of 48 required 10 extra rollouts.The marginal number of discoveries per rollout decreased as search continued.Source: §5.4 · p. 8, Figure 5 · p. 8
  • Accuracy was consistent across problem categories, while lower-accuracy categories tended to have greater average tree entropy, a possible uncertainty indicator and predictor of formulation success.The fine-grained results are organized by problem type and difficulty.Source: §5.4 · pp. 8–9, Table 2 · p. 9
  • Constraint modeling, especially inequality constraints, was the most frequent error source, with constraint-related errors in over 50% of incorrect models; expert judgments agreed with the objective-value proxy 82% of the time.In two cases, experts judged models incorrect despite matching the correct objective value.Source: §5.4 · p. 9

6. Discussions

The paper frames autoformulation as search over optimization models, combining LLMs, MCTS, and symbolic pruning. Benchmark evaluations report strong formulation performance and efficiency gains; future work calls for broader benchmarks and human-in-the-loop approaches.

6. Discussions

  • The method uses hierarchical optimization structure, LLM hypothesis generation and correctness evaluation, MCTS, and SMT-based pruning to explore formulations while eliminating redundancies.The paper reports empirical performance and efficiency gains from pruning and LLM-based correctness evaluation across real-world benchmarks.Source: §6 · p. 9
  • Future work includes human-in-the-loop frameworks, retrieval-augmented generation, and extending test-time search principles to LLM finetuning.The authors also call for large, diverse benchmarks covering more problem types and complexities, including challenging problems requiring advanced or creative reformulations.Source: §6 · p. 9

Impact Statement

LLM-generated formulations may contain subtle errors, and verification becomes harder as formulations grow more complex.

Impact Statement

  • For critical applications, the authors call for clear understanding of system limits, human oversight, and expert validation before deployment.The concern is that subtle formulation errors could produce incorrect solutions.Source: Impact Statement · p. 10

A.1. Pass@N vs. Best-of-N Results

The method’s estimated-score selection identifies the best formulation on over 90% of problems, and it outperforms ORLM under Pass@N. Against additional baselines, it consistently outperforms both Tree-of-Thought and naive sequential sampling.

A.1. Pass@N vs. Best-of-N Results

  • The estimated-score selector chooses the best formulation on over 90% of problems, and the method maintains a clear Pass@N advantage over ORLM.The comparisons emphasize structured, feedback-driven search and functionally diverse candidates.Source: §A.1 · p. 13, Table 4 · p. 13, Table 5 · p. 13

A.2. Comparisons Against Additional Baselines

  • MCTS consistently outperforms Tree-of-Thought and naive sequential sampling across benchmarks.The comparisons associate MCTS's advantage with uncertainty-guided feedback and pruning; decomposition alone does not prevent invalid or redundant formulations.Source: §A.2 · p. 13, Table 6 · p. 13

B.1. Formulation Equivalence Checks

  • SMT solvers check objective equivalence by testing whether function differences are always zero over the feasible region, and constraint-set equivalence by mutual implication.The approach can also identify redundant constraints, but nonlinear or highly complex formulations may challenge current solvers.Source: §B.1 · p. 14

B.2. Prompt Design

  • Prompt templates divide formalization into components, specifying separate LLM tasks for parameters, decision variables, objectives, and equality and inequality constraints.Other templates group equivalent variable sets and rank candidate components for incremental search.Source: §B.2 · pp. 14–17

B.3. Benchmarks

The evaluation uses benchmarks spanning linear, integer, mixed-integer, and one nonlinear programming instance, with different problem counts and difficulty scopes.

B.3. Benchmarks

  • NL4OPT uses 289 linear-programming problems from a labeled problem set with expert-assisted GPT-4 optimal solutions for execution-accuracy evaluation.The original NL4OPT provides mathematical formulations only.Source: §B.3 · p. 18
  • MAMO contains 652 easy and 211 complex linear-programming problems, and the experiments use only its complex subset.The easy subset is excluded because it is relatively saturated.Source: §B.3 · p. 18
  • IndustryOR contains 100 real-world problems from 13 industries, while ComplexOR has 37 problems, including 12 MILP problems; evaluation uses all 18 publicly available problems from that dataset2.Source: §B.3 · pp. 18–19

B.4. Metrics

The paper defines evaluation measures and categorizes optimization problems by whether their original formulations are convex and whether equivalent convex reformulations exist. Its solver discussion reports improved outcomes after convex reformulation for general-purpose solvers.

B.4. Metrics

  • Execution Accuracy checks executable-code solutions against ground-truth optimal values within a 5% margin; Pass@k succeeds if any of k candidates is correct.Best of N selects the candidate with the highest average estimated V value along its root-to-final-node path.Source: §B.4 · p. 19

C. Categorization of Autoformulation Challenges by Optimization Problem Structure

  • The taxonomy distinguishes original convex problems, nonconvex problems with equivalent convex reformulations, and nonconvex problems without equivalent convex forms.Equivalent convex formulations can differ in computational complexity, making efficiency relevant across all three types.Source: C. Categorization of Autoformulation… · p. 19

D. Illustrative Examples of Problem Categorization

  • The examples section distinguishes convex reformulations equivalent to the original from convex relaxations that only approximate it.Some reformulations or relaxations may require additional assumptions.Source: D. Illustrative Examples of Problem… · p. 20

D.1. Examples of Type-I Problems

  • The Type-I wireless-channel example maximizes mutual information over the input distribution and is convex in its original form.No reformulation strategy is needed for this example.Source: §D.1 · p. 20

D.2. Example of Type-II Problem

  • The PC-MinPower example is nonconvex as written, but its SINR constraints can be transformed into linear constraints to yield a linear program.The transformation is described as straightforward, and the resulting LP is easy to solve.Source: §D.2 · p. 21

D.3. Examples of Type-III Problems

  • The Type-III beamforming example uses semidefinite relaxation by removing a rank constraint, producing a convex problem that may require approximate recovery of the solution vector.Exact recovery can be guaranteed under certain conditions, such as uniform linear arrays.Source: §D.3 · p. 22

E. Effect of Formulation on Optimality, Solution Time

  • The PC-MinPower solver comparison evaluates success rate, optimality gap, and average solve time for instances with 10 and 100 users over 100 random samples.It compares general-purpose solvers on original and reformulated versions of the problem.Source: E. Effect of Formulation on… · p. 22

E.3. Discussion

  • COBYLA’s success rate increased from 0% to 100% after reformulating the original nonconvex problem as an equivalent convex problem.The discussion also reports 100% success rates, negligible optimality gaps, and minimal solve times for convex-program solvers on the reformulated problem.Source: §E.3 · p. 23

E.1. Experimental Setup

The experiment compares general-purpose and convex-program solvers on the original and reformulated PC-MinPower problem, measuring success, optimality gap, and solve time.

E.1. Experimental Setup

  • The original PC MinPower formulation is non-convex, but reformulation converts it into an equivalent convex problem, generally making it easier for optimization algorithms to solve efficiently while minimizing total system power under constraints.Source: §E.1 · p. 22
  • The evaluated solvers include four general-purpose methods and four convex-program solvers.The general-purpose set is TRCA, SLSQP, COBYLA, and COBYQA; the convex set is CLARABEL, ECOS, SCS, and OSQP.Source: §E.1 · p. 22

E.2. Results

  • Each solver is assessed by feasible-solution success rate, optimality gap from the known optimum, and average computation time.The results are presented in Tables 7 and 8 for problem sizes n = 10 and n = 100, respectively.Source: §E.1 · p. 22, §E.2 · p. 22

Related papers

Loading 2411.01679v2…