The solver returned “optimal.” Who chose what optimal meant?

Three allocation plans came back from the same input.

Each satisfied every hard constraint. Each carried an optimal solver status. Each was the unique best answer to the question it had been given.

They still described three different products.

One plan maximised aggregate operational fit. It gave one organisation a fit score of 20 so that another could gain 55. A second protected the worst individual outcome and retained most of the aggregate score. A third disturbed only one previous commitment, but left a large amount of potential fit unused.

The solver had not contradicted itself. The question had changed.

That is a familiar point in operations research. Optimality is always conditional on an objective and a feasible set. It becomes a sharper product problem when a language model turns an instruction such as “schedule these migrations efficiently, keep the experience fair, and avoid unnecessary changes” into variables, constraints, coefficients and tie-breakers.

I have felt this boundary while formulating allocation models myself. A model can be mathematically clean and still make a product choice that deserves a name, an owner and an explicit alternative.

At that point, the formulation is not merely implementation detail. It is executable product policy.

An agent can help draft that policy. A solver can optimise it. Neither should silently become the authority on what the product meant. The missing object is a decision contract that records the path from intended outcome to mathematical model, exposes the plausible alternatives, and keeps the solver status within its proper boundary.

Optimal is a conditional word

An optimisation solver answers a narrow and valuable question: what is the best feasible solution to the model it received?

The word model matters. Gurobi’s official status documentation defines OPTIMAL as the model being solved to optimality, subject to tolerances, with an optimal solution available. It does not claim that the objective represents the right outcome, that a missing rule was inferred, or that the people affected would endorse the trade-off.

The solver should not be the villain in this story. It is often the component behaving most precisely.

The ambiguity lives upstream. A product request has to be translated into at least four decisions:

• which assignments are feasible at all;
• which outcomes are prohibited and which are merely undesirable;
• which measurable proxy should be improved;
• how conflicts between aggregate value, minimum service and stability should be resolved.

Even a tie-breaker can become policy. If two schedules share the same primary score, selecting the one with fewer changed commitments is different from selecting the one that improves the lowest individual result. Both choices can hide behind the same headline metric.

Current research is making this translation boundary increasingly visible. OPT-Engine, a 2026 benchmark spanning ten canonical operations-research problem families, found that constraint formulation was the primary bottleneck in its solver-integrated experiments. Adding mathematically simple conditions caused formulation fidelity to fall even though the solver remained available.

A February preprint, CIR, takes a structural approach: it inserts a canonical intermediate representation between operational rules and mathematical instantiation. The representation makes rule intent, constraint archetypes and modelling paradigms more explicit. That is useful progress, but the paper is careful about the boundary. Its soundness result depends on semantically correct templates and sound instantiation, while the authors note that the representation can remain incomplete and its knowledge coverage is bounded.

The gap also appears after code generation. In the MM-OptBench preprint, a 780-instance multimodal benchmark, GPT-5.4 produced runnable code on 91.8 per cent of samples but reached 52.1 per cent pass@1 under the benchmark’s solver-grounded check. Gemini 3.1 Pro Preview produced runnable code on 92.5 per cent and reached 51.3 per cent pass@1. Those are benchmark results, not production failure rates. Their narrower lesson is that executable-looking code is weak evidence that the intended optimisation problem survived translation.

A July preprint on multi-warehouse formulation selection goes one step further. Its candidate MIP formulations share an allocation setting but encode four different priorities. The system selects among them using historical solver evaluation and realised allocation quality. Formulation choice is treated as an instance-level utility decision, not a fixed technical prelude.

These papers improve extraction, representation, formulation and verification. They do not remove the product decision underneath them: which defensible formulation should become active policy?

Same constraints, three policies

The counterexample here is deliberately small enough to inspect completely.

Six synthetic organisations each need one assisted migration window. There are three windows, with capacity for two migrations apiece. An earlier provisional plan placed three organisations in the first window, so it is no longer feasible under current capacity. At least one commitment must move.

Each organisation also has a synthetic fit score for each window. The scores might represent a combination of staffing compatibility, operational readiness and timing preference. They are deliberately fictional. Calling them “fit” does not make them ground truth.

The instance, capacity rules and solver stay fixed. Only the objective policy changes:

1. Efficiency maximises total fit.
2. Minimum-fit protection first maximises the lowest request fit, then maximises total fit without sacrificing that proven minimum.
3. Continuity first minimises changed commitments, then maximises total fit without introducing another change.

The second and third policies use two exact lexicographic phases. The primary optimum is fixed before the secondary objective is considered, so a large secondary gain cannot quietly buy away the stated priority.

For the executable example, MiniZinc used the open-source COIN-BC solver for every phase. The published runner also enumerates all 90 feasible schedules independently in Python. Every phase returned OPTIMAL_SOLUTION; each objective matched its bound; and the independent enumeration found the same unique result for every policy.

The three outcomes were:

The minimum-fit policy retained 93.8 per cent of the efficiency policy’s aggregate score while doubling the worst result from 20 to 40. The decisive difference was a two-request swap. Under the efficiency policy, one request gained 55 points while another lost 30. Aggregate fit rose by 25, but the lowest individual fit fell by half.

That is not an error. It is the efficiency policy doing exactly what its name says.

The continuity policy made only the one change required to restore feasibility. It protected the provisional commitments, but its total fit was 285. Stability was not free. Nor was it automatically the more humane choice: its minimum fit of 35 was lower than the minimum-fit policy’s 40.

Across total fit, minimum fit and changed commitments, none of the three outcomes dominates another. Each buys something that another gives up. A further sensitivity run showed another product wrinkle. Allowing a second change raised the best total fit from 285 to 300, yet lowered the worst request from 35 to 25. More freedom improved the aggregate objective but did not improve every stakeholder monotonically.

The independent enumeration matters. The MiniZinc Handbook notes that checking a claimed optimum is difficult without solving again using a different model known to be correct. Exhaustive enumeration is practical only because this example is tiny. It is not a production verification strategy. Here it gives the argument a strong bounded claim: for this complete finite instance, the divergence comes from policy, not solver randomness or a missed schedule.

Fork the policy before freezing it

Most formulation workflows ask for one model, test it, and improve it. That can verify the answer to one interpretation while leaving the interpretation itself untested.

A policy fork asks a different question before activation: which reasonable objective interpretations of the same product intent produce materially different outcomes?

The data and hard feasibility rules remain fixed. Two or three defensible objective policies are instantiated and solved. Their scalar objectives are not compared directly because the units and meanings differ. Instead, every solution is projected into one common outcome vector, such as aggregate fit, lowest fit, number of changed commitments, cost, latency or unmet demand.

If the outcomes are materially similar, the objective choice has low leverage on that instance. If they diverge, the system has found a product decision, not a modelling nuisance. An accountable owner should choose the policy or refine the request.

This does not mean generating dozens of arbitrary objectives. The fork should be small and domain-grounded. It can come from an approved policy library, a domain expert, or an agent proposal that is reviewed before execution. The purpose is not to let several formulations vote. It is to make the consequences of ambiguity visible while they are still reversible.

A Pareto frontier helps, but it cannot make the choice. It shows that improving one reported outcome requires giving up another. It cannot decide whose loss is acceptable, whether a floor is morally or contractually required, or whether the proxy itself is valid.

The decision contract

Once a policy is chosen, its assumptions need a durable product boundary. I would make that boundary a typed decision contract rather than a prompt, notebook or unexplained coefficient file.

The contract begins with intended outcome, accountable owner, affected groups and planning horizon. It identifies the source of every hard rule and distinguishes requirements from preferences. Its objective section names each term, unit, normalisation rule, priority order and tie-breaker. It records which policy alternatives were compared and which shared outcome measures exposed their differences.

The execution receipt then binds that policy to the exact model and instance, solver status, incumbent, bound or gap, and relevant tolerances. Finally, the contract names the observations that will test the policy after deployment and the conditions that should reopen the decision.

This is intentionally narrower than a general AI governance framework. It is compatible with the lifecycle logic in the NIST AI Risk Management Framework Core, which separates governance, context mapping, measurement and management, and calls for clear roles, documented intended purposes and continuing assessment. A decision contract does not claim compliance with that framework. It gives one optimisation decision a concrete interface across those concerns.

A compact representation might look like this:

decision:
  intended_outcome: schedule assisted migrations
  owner: migration-product
  affected_groups: [R1, R2, R3, R4, R5, R6]

feasibility:
  ruleset: migration-capacity-v1
  hard_rules:
    - exactly one window per request
    - no window exceeds current capacity

objective:
  policy: max_min_fit_then_total_fit
  ordering: lexicographic
  tie_breaker: disclosed and deterministic
  alternatives_compared: [efficiency, continuity]

verification:
  model: allocation-v1
  instance: synthetic-001
  domain_checker: exhaustive-enumerator-v1
  required_status: OPTIMAL_SOLUTION

outcome:
  measures: [total_fit, minimum_fit, changed_commitments]
  revisit_if: fit semantics or capacity assumptions change

The schema is not the contribution by itself. The important property is that no single layer can silently broaden its claim. The agent may draft a policy and explain alternatives. The product owner chooses what the system is trying to achieve. The compiler and solver turn that choice into an executable result. A separate checker tests domain invariants. Observed outcomes can propose a revision, but should not silently rewrite the active objective.

Three claims, not one proof

It is tempting to call the whole pipeline “verified.” That collapses three different claims.

The first is semantic fidelity: did the formulation preserve the intended decision? Evidence can include rule provenance, domain review, counterexamples, alternative-policy comparison and independent invariants. Except in tightly formalised domains, this is not a theorem about human intent.

The second is solver correctness: did the execution solve the encoded model to the reported status and tolerances? This is where solver statuses, bounds, gaps and reproducible instance identity belong.

The third is outcome validity: did the chosen policy produce the effect the product expected? This requires observations outside the optimisation model. Forecast fit can differ from realised fit. A stable schedule can create hidden operational cost. A minimum floor can protect the reported metric while missing a stakeholder concern that was never measured.

Keeping the claims separate is not an argument for ceremony. A low-consequence allocation may need only a lightweight contract and one alternative. A consequential or repeated decision deserves stronger provenance, independent checks and a clearer revisit trigger.

Nor is this an AI-only problem. Human modellers have always chosen proxies, weights and hard constraints. AI changes the economics of formulation. More models can be generated, revised and deployed, often behind fluent explanations that make the translation feel settled before it has been examined.

“Keep a human in the loop” is therefore incomplete advice. A person cannot meaningfully approve a dense objective they cannot interpret. The useful human boundary is a product choice expressed in domain outcomes: this policy gains 25 aggregate points by reducing one request from 50 to 20; this alternative preserves five of six provisional commitments but accepts 120 fewer aggregate points. The decision may still be difficult, but it is no longer hidden in algebra.

The same caution applies to automatic feedback. Realised outcomes can improve future policy selection, as the warehouse formulation-selection work suggests. They should not be allowed to mutate hard requirements or redistribute service silently. Learning can propose a new contract. It should not erase who chose the old one.

What optimal should let us say

An optimal solver result deserves confidence within its scope. It tells us that, for the encoded model and declared tolerances, no better feasible solution exists under the chosen objective.

That is a strong statement. It is simply not the whole product claim.

Before an agent-authored formulation becomes active, the system should be able to answer four questions in plain language:

Who owns the objective? Which plausible policy alternatives were considered? What did the solver establish? Which observed outcome would show that the policy was wrong or incomplete?

When the solver returns optimal, the next question is not whether to trust it. It is whether we can account for what we asked it to optimise.