A Gimle Labs working paper — Simulation Learning: Agent-Guided Proof Search in Traced Monoidal Categories. Read the full paper (PDF). It builds on Asgard, the circuit language, and Hugin, the agent framework.

A mathematical proof is a symbolic object, and constructing one is, in large part, an activity of symbolic manipulation. Whatever the claim — that an expression solves an equation in closed form, that two programs compute the same function, that a bound holds for every input — to prove it we must construct a formal derivation, a chain of steps each based on the strict application of a rule from the underlying proof system or the result of previous derivation or sub-proof.

Automated theorem proving is the discipline of automating this process, and as such it lives wholly inside that symbolic world, where the task essentially comes down to a search task within the space of possible derivations. Recently a lot of work has gone into applying LLMs to this search problem through their use as proof agents, but whatever intuition they might carry, they mostly end up as search agents, running a variation of smarter tree-search over the space of proof trees.

But this isn’t how a mathematician typically works. Terence Tao recently put it well: “I don’t have any magical ability. I look at a problem, play with it, work out a strategy.” We are not proof machines, automatically grinding away at the problem. In fact, the hard part is rarely the grinding — brute-forcing cases, marching through proof rules — which is laborious but ultimately a mechanical search problem.

Instead, in our heads we move up and down a ladder of fidelity. We start coarse, trying ideas at a high level, then focus on particular parts and work down into the details. Realising we’re on the wrong track, we retreat back up the ladder, reshape the idea, and continue. We think out-of-order and at mixed levels of fidelity — all guided by intuition and by the evidence we discover as we dig into the details.

The truly novel work comes not from the grind but from unexpected moments of lateral thinking — what I like to call a jump: an out-of-nowhere step that completely changes the setting of the proof.

The classic example is a loop invariant — a formula you conjure from nothing, easy to check once you have it but with no symbolic trail leading there. In principle, finding one is a search problem, the same shape as folding a protein or picking the next move in Go. In practice, it is a far harder one: the space of candidate formulas is unbounded, there is no fixed move set, and no score to climb toward — nothing for the usual search machinery to grip. The jump isn’t deduced, it is found.

The human approach is to search experimentally: sketch a picture, run a few numbers, simulate a special case — coarse play at first, taking a gradually more formal shape as the idea firms up. That experimental work is the real mathematics: none of it survives into the finished proof, and it is exactly what the purely symbolic approach cannot do.

Simulation learning tries to formalize this mix of experimentation and formalism by introducing a way for the proof agent to use a weaker simulation step to then inform future steps in a parallel strict proof derivation. In this setting, at any point the proof search can branch off into a simulation, watch how the system actually behaves, and let that propose the jump the symbols can’t reach. The formal mechanism for this detour is a weakening rule. A proof rule that that accepts simulation evidence where the strict rules demand a derivation. Sometimes this turns up an exact step that the rules can then confirm and the finished proof is exact. Sometimes no exact step exists and the best the branch can justify is an approximate jump, folded back into the proof with a measured error attached.

The Weakening rule

Our weakening rule isn’t novel itself. We borrow it from program verification, where versions of it has been around for decades. In particular, in Hoare Logic where it is known as the rule of consequence:

The rule states that if you can strengthen the precondition or weaken the postcondition and the proof is still valid. It is in many ways this rule that makes Hoare logic usable, since it enables us to not track the exact state of a program but only the properties of it. It trades exactness for a weaker form of conditions but one which you can more easily formally prove.

Simulation Learning centers on a similar concept but in this case the weakening is not a subset or superset relation but an equivalence under some distance measure. So we give up precision in order to progress the proof, ie instead of proving \(C_1 = C_2\) exactly, we prove \(C_1 \approx_\epsilon C_2\) — the two terms agree to within a measured tolerance \(\epsilon\).

However, there is another much big difference between Simulation Learning and Program Logics. In Program Logics the weakening steps — \(P \Rightarrow P’\) and \(Q’ \Rightarrow Q\) — are proven. They have the same epistemic standing as the rest of the proof. In Simulation Learning, the weakening is justified by simulation evidence: finitely many samples from a computational experiment. That is a genuinely weaker certificate but proving the approximation above is valid is usually as hard as solving the original problem, whereas a simulation is typically cheap.

Two kinds of move

In a Simulation Learning style proof we can divide the steps into two categories:

A strict rewrite turns a term \(C\) into an exactly equivalent \(C’\) by applying a rule you already trust from the underlying proof system — associativity, interchange, naturality, scalar fusion, etc. It’s syntactic, it’s unconditional, and it preserves meaning by construction.

An approximate rewrite swaps a subterm \(S\) inside \(C\) for a candidate \(S’\), giving \(C’ = C[S \mapsto S’]\). Nothing in the proof system licenses this, instead we simulate both \(C\) and \(C’\) over a set of inputs and check that \(\|C(x) - C’(x)\| < \epsilon\) across the samples. That gives a simplification the strict rules can’t reach but breaks the strictness of the proof. This is simply a possible derivation without any guarantee, beyond the simulation, that it is true.

The slogan is that strict rewrites are free and approximate rewrites are expensive. Most of a proof should be strict. The approximate moves are reserved for the places where exactness has nothing left to offer and we called a jump, that is what an approximate move can help us unlock.

Combining these two moves we end up with a mixed proof: a chain of moves, some exact, some approximate, ending in a simplified term and a ledger of which steps cost what in terms of correctness. This is a Hoare proof with weakening, with its loss of precision recorded at each step and the whole is only as strong as its weakest approximate step.

Approximations and proof branches

The most useful approximate moves are often the ones that don’t survive but do their work and then vanish, leaving a proof that is exact from end to end. Almost always, what we really want is a strict proof and not a weaker approximate statement. Instead we then use the approximate moves to inform the strict proof.

We do this by using our form of weakening to branch off the strict proof path, run a series of simulations to introduce approximate deduction steps and then use that to discover candidate proof steps to be introduced in the strict main path.

The perfect example is trace elimination, i.e. the elimination of feedback in a proof. To remove a feedback loop you must exhibit a generator — a closed-form expression for the fed-back wire that satisfies the loop’s fixed-point equation. Finding one is like finding a loop invariant, or a closed-form antiderivative in calculus, easy to check but generally intractable to discover. And this is precisely where the strict proof search falters, because the space of candidate expressions is simply too big, with no obvious paths for the search to progress along.

Simulation Learning narrows that by running two, or more, proof threads in parallel. An exploratory thread simulates the trace, watches the values flowing around the feedback wire, and fits an approximate generator \(\hat{g}\) to the outputs. A verifiable thread then takes \(\hat{g}\) as a starting point for searcheing its neighbourhood in expression space for an exact generator that the strict rules can confirm. Once found, trace elimination proceeds by strict rewrites alone.

Much more on this topic in the papers and writings below:

• Read the full paper (PDF) — the formal development, the error-composition propositions, and the worked examples.
• Asgard: a programming language for dynamical systems — a circuit algebra for dynamical systems build around a proof system for simulation learning.
• The Smoothness Hypothesis — why rough domains have to learn from simulation in the first place.
• Hugin on GitHub — the agent framework that runs the interleaved search.