Formal Optimisation & Decision Science

A language model is a plausible-answer generator and a solver is a guarantee machine. This pillar is about composing the two rather than choosing between them, and the result so far is a negative one worth stating plainly: models translate a problem statement into a formal encoding competently, and cannot be trusted to solve the encoding they produced.

Translation, not solution

The pipeline that works puts the model at the front. English goes in, a canonical constraint encoding comes out, and an exhaustive solver searches the finite domain for an assignment that satisfies it. Savanty uses Answer Set Programming with Clingo for the search, and wraps the translation step in a typed self-repair loop that handles syntax errors, unsatisfiable encodings, and empty results differently — including minimal-unsat-core localisation, which turns "no solution" into "these three constraints conflict".

The value of that split is that the guarantee comes from the solver and not from the model. If the encoding is right, the answer is optimal in a sense that can be checked. If the encoding is wrong, the failure is visible as an unsatisfiable or nonsensical result rather than as a confident wrong number. That is a much better failure mode than the one you get from asking a model to optimise directly.

Ranking under sparse human feedback

A related problem is ordering a set of items when the only available signal is human pairwise judgement, which is expensive. Exhaustive comparison is quadratic and unaffordable; random sampling wastes budget on pairs whose order is already obvious. Adaptive selection concentrates comparisons where the current ordering is least certain, which is a multi-armed bandit problem with an established solution.

The articles here are careful about the distinction between the selection algorithm and the rating model, which are separate choices that get conflated. Compere pairs UCB1 selection with Elo rating; Bradley-Terry, Thurstone and TrueSkill are different rating models that can sit behind the same selection strategy, and the comparison articles say where each genuinely wins.

Compilation as the third approach

A third thread treats the specification itself as a compilation target. In quantitative finance, a signal is usually prototyped in a notebook and reimplemented for production by a different person, which introduces a translation step where most of the errors live. Compiling a visual or declarative specification directly into a verified executable removes that step, and the interesting engineering question is what the compiler must guarantee for the removal to be safe.

The common thread across all three is that a formal artefact sits between intent and execution, and that the artefact is inspectable. Whether it is an Answer Set Programming encoding, a rating model, or a compiled signal, a reader can look at it and disagree — which is not true of a number a model produced directly.