ASTOR: Benchmarking and Improving Autoformulation for Soft-Constraint Optimization with a Formal Grammar

What it claims

ASTOR is a single-LLM-call method that turns a natural-language decision problem into a JSON-serialized abstract syntax tree (AST) under a typed formal grammar. Deterministic code then compiles the AST to Gurobi. Across the 355 instances of the new SoftOR benchmark, ASTOR reaches 88.5% solution accuracy against 84.8% for the strongest alternative. It is best on three of four SoftOR datasets; Nurse Rostering is the exception. On 435 conventional hard-constraint problems it scores 81.8%, within 0.5 percentage points of the best method. The authors prove the grammar is "adequate" (Appendix C): every well-formed formula denotes a problem in the target class, and every problem in the class is expressible.

How it works

The grammar supports two soft-constraint formulations. The lexicographic one minimizes tier-summed violations in priority order, then the base objective. The weighted-penalty one adds weighted violations to the base objective subject to hard constraints. The pipeline:

1. The prompt holds a task description, the grammar, and a JSON schema for the AST. The schema covers variable declarations, hard constraints, soft constraints and priority annotations.
2. One LLM call returns the AST-JSON.
3. Deterministic code applies only local JSON repairs, then validates the schema and symbols and parses the tree.
4. The tree compiles to Gurobi code and is solved.

ASTOR uses the same inference budget as single-request baselines (Direct, Codegen, Chain-of-Thought). It is also compared against multi-agent systems such as Chain-of-Experts, OptiMUS and ORThought. No fine-tuning is involved.

Evidence

Scoring is solution accuracy. An attempt is correct only if its solved objective value matches the gold value, a scalar or a vector, within tolerance. SoftOR has four components:

• Nurse Rostering: 15 instances, weighted penalty, explicit priority cues, gold from published optima (Curtois, 2014).
• COMPASS: 85 instances, lexicographic, explicit cues, gold by enumeration.
• TravelPlanner: 180 instances, lexicographic, modal cues ("must", "should", "may"), gold by enumeration.
• LexiBench: 75 instances, entirely new, lexicographic, mixed cues, gold by enumeration or solver code.

For Nurse Rostering, source weights of 1, 2, 3 and 100 become the phrases "slightly prefers", "prefers", "strongly prefers" and "far more serious". Methods never see the numbers and must infer preference strength from language. An appendix ablation exposes the weights. The fetched text does not give per-dataset scores, the LLM used, or per-baseline numbers.

How to use it

The paper states that code and data are available, but the fetched text has no link, licence or commands. Running ASTOR as described needs Gurobi as the backend solver. Full prompts and execution rules are in Appendix D, and worked traces are in Appendix B.

Limits

ASTOR trails another method on Nurse Rostering, the only weighted-penalty component, which has 15 instances. Lexicographic tasks make up 340 of the 355 SoftOR instances, so weighted-penalty evidence is thin. The adequacy guarantee covers only the problem class the grammar defines. It says nothing about whether the LLM picks the right formula. Solution accuracy checks the optimal value, not the formulation, so a wrong model with a matching optimum counts as correct. The fetched page is truncated partway through Section 4, so the results tables, ablations and stated limitations were not available.