Gimle Papers Working Paper
Simulation Learning
Many useful transformations of dynamical systems have no purely syntactic proof. We propose an agent-based approach that extends categorical proof with simulation-guided reasoning — analogous to the weakening of pre- and postconditions in Hoare logic.
The Problem
Exact proofs end where approximation begins
Consider the Navier–Stokes equations. They can be expressed as a system of differential equations, compiled into a traced circuit, and simulated. But no closed-form solution exists — there is no chain of categorical rewrites that eliminates the trace.
The proof system is sound for exact equivalence, but the equations are not exactly solvable. Yet physicists routinely work with approximate solutions: linearisations, perturbation expansions, asymptotic regimes, empirical correlations.
Each of these is, informally, an approximate rewrite — a replacement of one subcircuit with a simpler one that behaves similarly under the conditions of interest. The approximation is justified not by a syntactic proof but by simulation.
What the proof system can do
The traced monoidal category of circuits comes equipped with a rewrite system: categorical axioms (associativity, interchange, naturality of trace) and domain-specific rules. A chain of rewrites from circuit $C_1$ to $C_2$ constitutes a proof that they compute the same function.
What it cannot do
Linearisation around an equilibrium. Truncation of a series. Replacement of a nonlinear term with an empirical approximation. These are not exact — the rewrite system cannot express them.
The Hoare Logic Analogy
Weakening makes proof systems practical — for programs and for circuits
In Hoare logic, the rule of consequence allows weakening: if the precondition can be strengthened or the postcondition weakened, the proof still goes through. You don't need to track exact state — you track properties of state.
We propose an analogous weakening for circuit equivalence. Instead of proving $C_1 = C_2$ (exact), we prove $C_1 \approx_\epsilon C_2$ (approximate to tolerance $\epsilon$), where the approximation is justified by simulation evidence.
The parallel — and the difference
Hoare logic weakens logical conditions to make proofs tractable. Simulation learning weakens equivalence to make circuit simplification tractable. In both cases, the weakening is explicit and the loss of precision is quantified.
But there is an important epistemic difference. In Hoare logic, the weakening steps ($P \Rightarrow P'$, $Q' \Rightarrow Q$) are proven. In our setting, approximate rewrites are justified by simulation evidence: finite samples from a computational experiment — a weaker form of justification. We adopt it because exact proof of the approximation’s validity is typically as hard as solving the original problem.
Two Kinds of Moves
The agent interleaves strict rewrites with simulation-justified approximations
Strict rewrite
Exact, unconditional, syntactic
Applies a categorical axiom or domain-specific rule to transform a circuit $C$ into an exactly equivalent circuit $C'$. Preserves semantics by construction.
Examples: associativity, interchange, naturality of trace, identity laws, scalar fusion, register–deregister cancellation.
Cost: zero approximation error.
Approximate rewrite
Conditional, simulation-justified, semantic
Replaces a subcircuit $S$ within $C$ with a candidate $S'$, producing $C' = C[S \mapsto S']$. Justified by simulation: the agent runs both $C$ and $C'$ over a set of inputs and verifies that $\|C(x) - C'(x)\| < \epsilon$ for all tested inputs.
Cost: incurs bounded approximation error.
Strict rewrites are free. Approximate rewrites are expensive.
The agent learns when to use each. Strict rewrites preserve exact equivalence at no cost. Approximate rewrites incur error but enable simplifications that strict rewrites cannot reach. The learned policy encodes which proof strategies tend to work for which classes of circuits.
The Agent Strategy
A typical search procedure for circuit simplification
Normalise
Apply strict rewrites to simplify the circuit where exact rules suffice.
Identify candidates
Find subcircuits that resist exact simplification — traced subnetworks, nonlinear terms, high-order expansions.
Propose replacements
Suggest a simpler subcircuit: a trace-free circuit, a linearisation, a lower-order expansion.
Simulate and measure
Run both versions, measure the error. If within tolerance, accept. If not, revise or try a different subcircuit.
Iterate
Continue interleaving strict and approximate moves until the circuit reaches the target complexity.
What counts as evidence
The simulation evidence for an approximate rewrite consists of:
Input distribution — the set of inputs (initial conditions, parameter values, time horizons) over which the approximation was tested.
Error bound — the maximum observed error $\epsilon = \max_x \|C(x) - C'(x)\|$ over the test inputs.
Confidence — if the inputs are sampled stochastically, a statistical confidence bound on the error.
An approximate rewrite is conditional: it holds for the tested regime. The agent tracks the conditions under which each approximation was validated.
The Mixed Proof
A new kind of proof object — part exact, part simulation-justified
A complete simplification by the agent produces a mixed proof: a sequence of strict rewrites (exact, unconditional) and approximate rewrites (simulation-justified, conditional). The result is a simplified circuit together with a record of which transformations are exact, which are approximate, and the overall error bound.
Analogous to Hoare logic with weakening
Each weakening step is justified, and the overall proof tracks the accumulated loss of precision. The proof is as strong as its weakest link — but crucially, the weakness is explicit and quantified.
Proof Sketching
Approximate reasoning as scaffolding for exact proofs
Approximate rewrites have a second, more subtle role: they can guide the search for strict rewrites, even when the final proof is entirely exact.
The key case is trace elimination. To eliminate a trace (feedback loop), one must exhibit a generator: an expression for the feedback wire that satisfies the fixed-point equation. This is analogous to finding a loop invariant in program verification, or a closed-form antiderivative in calculus: the result can be verified mechanically, but discovering it requires insight.
The agent maintains two parallel threads — one approximate and exploratory, one strict and verifiable — and uses the former to steer the latter.
Explore approximately
Simulate the traced circuit, observe the feedback wire, and fit an approximate expression — a truncated series, a rational function, an empirical formula.
Refine
Use the approximate candidate $\hat{g}$ as a starting point for exact search. Search the neighbourhood of $\hat{g}$ in expression space for an exact generator.
Verify strictly
Once an exact generator is found, the trace elimination proceeds by strict rewrite alone. The approximate reasoning was scaffolding; the final proof carries no approximation error.
Simulation and proof are not in tension.
Simulation provides the evidence that justifies approximate proof steps. The proof system provides the structure that keeps approximations composable and their limitations transparent. The result is a strictly valid proof that the agent would not have discovered without the approximate detour.
Example: A Nonlinear Oscillator
Discovering an approximate closed-form solution for $\ddot{x} + \alpha \dot{x} + \beta x + \gamma x^3 = 0$
Compile
Express the equation as a traced circuit with two feedback loops (position and velocity).
Strict rewrite
Normalise the circuit, apply known identities.
Simulate
Run over a range of initial conditions to understand the behavioural regime.
Propose approximation
Replace the cubic subcircuit $\gamma x^3$ with a linearised correction $\gamma' x$ chosen to minimise simulation error over the tested regime.
Eliminate trace
With the cubic term removed, the circuit is a linear second-order ODE — which does have a trace-elimination proof (the solution involves $\exp$, $\sin$, $\cos$).
Validate
Simulate the original and the trace-free approximation; record the error bound.
The result
An approximate closed-form solution: a trace-free circuit that matches the nonlinear oscillator's behaviour within tolerance $\epsilon$ for the tested regime.
The cubic term prevents exact closed-form solution. But the agent finds a path through the proof space that combines exact rewrites (where possible) with a single, well-justified approximate step (the linearisation) to reach a usable closed form.
Key insight
The approximate rewrite unlocks the exact rewrite. Without linearisation, the trace cannot be eliminated. With it, standard categorical machinery completes the proof.
The Navier–Stokes Frontier
From approximate solutions to regularity proofs
Approximate solutions
Piecewise closed forms for different regimes
The Navier–Stokes equations compile to a coupled traced circuit. No exact trace elimination exists. But the agent can identify regimes (low Reynolds number, boundary layers, far-field) where subcircuits simplify.
It proposes approximate rewrites justified by simulation in each regime, then composes regime-specific approximations into a piecewise closed-form solution. Each approximation carries its simulation evidence, making conditions of validity explicit.
Toward a regularity proof
Proof sketching at the frontier of mathematics
Global regularity is equivalent to a specific property of trace elimination: can the trace be eliminated by a generator that remains smooth for all time?
The proof-sketching strategy applies: simulate to propose approximate generators, identify structural regularities (uniform Fourier decay, bounded energy estimates), then search for strict rewrite chains that establish these bounds categorically.
The framework makes the problem mechanically addressable — simulation evidence constrains the search space, and partial results are captured as formal proof objects.
A note of honesty
This is unlikely to resolve the Millennium Problem directly. But it provides a concrete, computational framework in which to search for a resolution — and in which partial progress is captured as formal, verifiable proof objects rather than informal heuristic arguments.
As Reinforcement Learning
The agent's search over mixed proofs can be formalised as an RL problem
State
The current circuit and the history of applied rewrites.
Actions
Strict rewrites (from the categorical proof system) and approximate rewrites (propose a subcircuit replacement, simulate to validate).
Reward
Reduction in circuit complexity (fewer operations, lower trace depth), penalised by approximation error.
Terminal state
A trace-free circuit (or below a target complexity threshold) with error within tolerance.
Learned policy
Encodes which proof strategies tend to work for which classes of circuits — when to use exact vs. approximate moves.
Connection
The agent is searching for proofs in an extended proof system where some steps are syntactic (exact) and others are semantic (simulation-justified).
Connections
How simulation learning relates to existing ideas
Perturbation theory
Classical perturbation methods (regular, singular, multiple scales) are manual versions of simulation learning: the mathematician identifies a small parameter, proposes an approximate rewrite, and validates by checking the residual.
Our framework automates this and generalises it beyond expansion in a single small parameter.
Symbolic regression
Symbolic regression searches for mathematical expressions that fit data. Simulation learning is more structured: it searches within the space of typed circuits (compositional, with a proof system), using simulation to justify specific rewrite steps.
The result is not just an approximation but a proof of approximation, with explicit conditions of validity.
The role of types
The typed circuit representation constrains the search space: approximate rewrites must produce well-typed circuits (matching input/output degrees). This prevents the combinatorial explosion that plagues unconstrained symbolic search.
Implementation
Asgard provides the circuit algebra: compilation from equations, categorical rewrites, and differentiable simulation. Hugin provides the agent side: structured reasoning over an immutable interaction stack, with tool access to Asgard's rewrite and simulation engines.
Conclusion
Simulation and proof are not in tension — they are complementary modes of reasoning.
Simulation learning extends the categorical proof system with simulation-justified approximate reasoning. The result is a new kind of proof object: a mixed chain of exact rewrites and simulation-justified approximations, with explicit error bounds and conditions of validity.
Not by abandoning formal reasoning, but by enriching it with empirical evidence.