Research note · Benchmarking
Benchmarking Lanyon against Frontier Models: Linear PDEs
In this technical deep dive, we compare the current frontier models against Lanyon in terms of accuracy and cost for the solutions to linear partial differential equations.
As part of the demonstration of the breakthrough capabilities of Lanyon, this write up is the first in a series of benchmarking posts comparing the output of Lanyon to other frontier models. For this first benchmarking post we define a set of tests for evaluating the performance of the frontier models on problems for which you have already seen a demonstration of Lanyon’s capabilities: formally verified solvers for linear partial differential equations (PDEs).
The benchmarks
Our benchmarks are divided into two different cases based on the capabilities of Lanyon shown in our discussion of the advection-diffusion equation and corresponding GitHub repository and the Maxwell equations of electromagnetism and the corresponding GitHub respository. We evaluate the following models:
- Kimi K3
- Claude Opus 4.8
- Claude Fable 5
- GPT-5.5
- GPT-5.6 Sol
with two different classes of prompts: a detailed prompt which describes in totality the expected solver in C, the properties to be verified in Lean, and the simulation output; and a terse prompt which only asks to solve the specific PDE in question with a specific numerical method on the same deployment task as performed by Lanyon and the detailed prompt. For the terse prompt, the meaning of “Verify your implementation in Lean” is left to the discretion of the agent. The two problems we evaluate are:
- Linear advection of a square pulse in one spatial dimension
- Maxwell equations solution to a plane wave propagation diagonally in two spatial dimensions
In all cases, we ask for the same numerical method, a finite volume wave propagation scheme, and we further specify in the detailed prompt that the method should utilize a second order reconstruction, a minmod limiter to ensure a total variation diminishing (TVD) property, and that the update formula should be cast in the traditional form for the wave propagation scheme: in terms of the computed left- and right-going fluctuations.
Each prompt, with each agent, is performed three times to permit analysis of the variation in agent performance run to run in the evaluation of each agent’s performance.
The rubric
As we articulated in our announcement, a key risk of current autoformalization capabilities of frontier models is misformalization. Lanyon’s neurosymbolic architecture completely eliminates this risk; the proof and the code are derived from the same domain specific language (DSL) specification. Further, Lanyon’s symbolic theorem-prover respects the axioms of floating point arithmetic and thus must satisfy a more restrictive class of properties, e.g., arithmetic is commutative but not associative under the IEEE-754 standard. Finally, and critically, we must evaluate the semantic correctness of the output: did the agent utilize the requested numerical method? Did the agent do the requested simulation? Or did the agent’s discretion pollute the output and implement something not requested in a manner which could be counter-productive in production?
We divide our full rubric for the Lean up in the following fashion:
- Do the Lean definitions transcribe the same formulas the C code implements (same scheme, same stencils, same branch structure)?
- Are the proved theorems about code the solver actually executes in its demo run, or about dead/unused functions?
- What, if any, escape hatches were utilized to make the Lean type-check?
We list any of:
sorry,admit,axiom,native_decide, vacuous hypotheses, true-by-construction theorems presented as substantive, degenerate-parameter demos engineered to make verification trivial (e.g. running only at CFL=1 for one-dimensional advection where the scheme is an exact shift), or code constructs whose apparent purpose is to defeat automated grading. - A final verdict.
- “faithful”: Lean models the formulas the solver executes and the properties are substantive
- “partial”: honest proofs, but confined to a subset of the scheme, to dead code, or to a degenerate regime
- “misformalized”: the verification claim rests on escape hatches (any use
of
native_decidecounts) or on theorems that do not establish what they appear to establish - “disconnected”: the Lean proves things about a different object than what the
C implements
And we additionally evaluate the C code in a commensurate fashion:
- Does the scheme display second order convergence by including a limited second order reconstruction in the execution path? Or is the scheme only first order accurate?
- Does the reconstruction utilize a limiter in the execution path and have non-increasing total variation (no new extrema introduced)? Is the limiter implemented correctly?
- Is the scheme a wave propagation algorithm? Or does the scheme either not compute the
fluctuations or not use computed fluctuations to determine the update of the solution?
Does the simulation match the requested deployment target?
For this evaluation, we have every agent review every output, so that all frontier models all review each other. Final evaluation is the aggregate of each agent’s review of each trial. To minimize any potential self-bias, each agent reviews an anonymized read-only snapshot of the trial with a neutral path, no .git/.lake, and names scrubbed. Name scrubbing is a grep for if the model has utilized any naming conventions which identify themselves, such as calling a flux function “codex_flux” or “fable_flux” which then are substituted as “model_flux.” We do not scrub for style or any other markers of agents to avoid contaminating the evaluation with manipulation of the underlying functionality the agents have implemented. Future work on our evaluation pipeline could quantify markers of agent style to contextualize any self-grading divergence; however, in these initial benchmarks we do not find any significant evidence of self-bias, and the use of three different vendors’ frontier models provides a spread in the evaluation pipeline to prevent Claude, GPT, or Kimi from giving themselves high marks in isolation.
An aside: accuracy vs. cost
Lanyon’s neurosymbolic architecture provides us a uniquely powerful way to check the implementation of a solver before one ever runs a simulation: does the expanded proof type-check and do the expanded kernels compile, or is the specification in the DSL incorrect? This reinforcement learning loop is tighter than a traditional agentic loop in creating numerical solvers. Current frontier models can only verify post hoc. They must write the code, compile, run the code to determine if properties are satisfied in finite precision, and then (or at most in parallel) write Lean or another formal verification language to “check the math” of their implementation.
To be maximally generous to the current frontier models, we allow the models to execute complete agentic loops from specification through simulation. We make this choice in our evaluation because, fundamentally, correctness is more important than cost. Likewise, the frontier models execute at the maximum effort we have access to: Kimi K3 and both Claude Opus 4.8 and Fable 5 at “max” effort, and GPT-5.5 and 5.6 Sol at “xhigh” effort.
We quote all costs for completeness with a specific focus on the output tokens. We focus on output tokens because the wallclock time has additional confounding variables for all the agents, including Lanyon, due to costs in e.g., API latency and provider queuing. But also, critically, the output tokens permit the clearest demonstration of one of the central theses of Lanyon: reasoning in an information dense DSL not only leads to increased reliability from the deterministic symbolic expansion to proofs and code, its information density likewise provides large gains in the efficiency of the reasoning. The amount of information in a single token representing a component of the DSL is much larger than a token representing a handful of characters in English (or a handful of characters in C or Lean).
Linear advection: top-line results
| variant | config | cost/trial | wallclock | mech | hygiene | panel |
|---|---|---|---|---|---|---|
| detailed | claude-fable-5 | \$7.39 ± 1.17 | 20.9 ± 5.3 min | 3/3 | 3/3 | faithful x3 |
| detailed | claude-opus-4-8 | \$7.03 ± 2.21 | 30.5 ± 9.6 min | 3/3 | 3/3 | faithful x3 |
| detailed | gpt-5.5 | \$1.39 ± 0.29 | 5.4 ± 1.8 min | 3/3 | 3/3 | faithful x3 |
| detailed | gpt-5.6-sol | \$2.56 ± 2.23 | 8.7 ± 3.9 min | 3/3 | 3/3 | faithful x3 |
| detailed | kimi-k3 | \$2.26 ± 0.38 | 37.9 ± 2.7 min | 3/3 | 3/3 | faithful x3 |
| terse | claude-fable-5 | \$8.30 ± 2.78 | 25.3 ± 3.9 min | 3/3 | 3/3 | faithful x2, partial x1 |
| terse | claude-opus-4-8 | \$3.37 ± 0.91 | 16.6 ± 3.8 min | 3/3 | 3/3 | partial x3 |
| terse | gpt-5.5 | \$1.42 ± 0.34 | 4.5 ± 0.8 min | 3/3 | 2/3 | partial x2, misformalized x1 |
| terse | gpt-5.6-sol | \$1.18 ± 0.15 | 5.8 ± 0.6 min | 3/3 | 3/3 | faithful x2, partial x1 |
| terse | kimi-k3 | \$0.89 (n=21) | 24.1 ± 14.6 min | 3/3 | 1/3 | misformalized x2, faithful x1 |
For the “mech” column, we are checking all three of: does the C code compile, does the
C code run, and does the Lean code type check, for each of the three trials. For the “hygiene”
colume we are checking for zero use of sorry/admit, zero axiom declarations, and zero
use of native_decide for each of the three trials. Note that a score of faithful in our
automated scoring here is a measure of “does the Lean match the C” and not a measure of
faithful implementation of the prompt.
We can further break the cost column down by examining the breakdown in token usage:
| variant | config | output tokens (mean, vendor-billed) | cumulative input (mean) | cache-hit share |
|---|---|---|---|---|
| detailed | claude-fable-5 | 101k | 1.27M | 93% |
| detailed | claude-opus-4-8 | 153k | 4.29M | 96% |
| detailed | gpt-5.5 | 22k | 0.81M | 91% |
| detailed | gpt-5.6-sol | 23k | 3.11M | 98% |
| detailed | kimi-k3 | not reported; per-trial bounds 14k-174k (see below) | not reported | not reported |
| terse | claude-fable-5 | 120k | 1.04M | 89% |
| terse | claude-opus-4-8 | 79k | 1.74M | 95% |
| terse | gpt-5.5 | 19k | 0.87M | 90% |
| terse | gpt-5.6-sol | 18k | 0.89M | 95% |
| terse | kimi-k3 | not reported; per-trial bounds 4k-184k (see below) | not reported | not reported |
Kimi per-trial bounds:
- detailed — t1: 14k-124k (\$1.86); t2: 17k-174k (\$2.62); t3: 14k-154k (\$2.31)
- terse — t1: 4k-52k (\$0.79); t2: 18k-184k (\$2.77); t3: 6k-65k (\$0.98)
Note that these Kimi bounds are computed as a floor from visible content in the transcript (assistant text + tool-call arguments at ~3.5 chars/token) to a ceiling from the trial’s entire billed cost converted at the \$15/MTok output rate as if input were free. A realistic mid-estimate deducting plausible input spend sits well below the ceiling, e.g., detailed t1 (the \$1.86 trial) works out to approximately 15k floor / approximately 90k realistic ceiling under Fable-like input assumptions.
Finally, we can examine the performance on the C side per trial and model:
| variant | config | t1 | t2 | t3 |
|---|---|---|---|---|
| detailed | claude-fable-5 | 2nd / TVD | 2nd / TVD | 2nd / TVD |
| detailed | claude-opus-4-8 | 2nd / TVD | 2nd / TVD | 2nd / TVD |
| detailed | gpt-5.5 | 1st / TVD | 2nd / TVD | 2nd / TVD |
| detailed | gpt-5.6-sol | 2nd / TVD | 2nd / TVD | 2nd / TVD |
| detailed | kimi-k3 | 1st / TVD | 2nd / TVD | 2nd / TVD |
| terse | claude-fable-5 | 2nd / TVD | 2nd / TVD | 2nd / TVD |
| terse | claude-opus-4-8 | 2nd / TVD | 2nd / TVD | 2nd / TVD |
| terse | gpt-5.5 | 1st / no-TVD | 1st / no-TVD | 1st / no-TVD / nd=4 |
| terse | gpt-5.6-sol | 1st / no-TVD | 1st / no-TVD | 1st / no-TVD |
| terse | kimi-k3 | 1st / no-TVD | 1st / no-TVD / nd=5 | 1st / no-TVD / nd=3 |
where we have bolded the two detailed trials for their prompt violations (the detailed
prompt specifically requested a second order method with a minmod limiter to ensure the
method is TVD), and six terse trials for their use of a trick to only make their
implementation work with a CFL number of 1.0 (where a particular formulation of the
upwind formula degenerates to an exact shift of the solution and does not generalize
to general advection solves). We have also marked again the specific trials which utilized
native_decide, which we flag as a misformalization due to the potential for cheating on
how the Lean type-checks.
Linear advection: results breakdown
Our reference Lanyon one-dimensional linear advection verified solver takes $\sim 7$ seconds to generate, utilizes $\sim 800$ output tokens, and is second order and TVD by construction with the terse prompts described in our advection-diffusion deep dive2. The success of Lanyon even under ambiguous or terse prompts, along with its high cost-efficiency—upwards of a factor of 20-100 cost reduction in output tokens—is the fundamental advantage of the neurosymbolic layer. Lanyon’s symbolic layer encodes decades of knowledge of numerical methods and makes informed choices for model discretization without further intervention of the user.
Of course, equally important for understanding the advantage Lanyon provides is by a careful examination of reliability. Lanyon’s variation prompt to prompt is restricted to small details: how wide is the step function, where does it start, what precise value of CFL should the simulation utilize? These initial condition implementation details can be taken from a user’s prompt, but Lanyon can make informed choices, same as any other agent. What does not change is the proof matching the code.
The proof not matching the code is the precise failure mode run to run of other agents,
especially under ambiguous prompts. The “partial” score for many Claude runs is because,
under the terse prompt conditions, both Opus 4.8 and Fable 5 implemented a second order, TVD
method and then proved properties of a first order method with CFL=1 in which advection
reduces to an exact shift. GPT-5.5 and Kimi K3 failed to prove properties of their
implemented solvers in some iterations, falling back to native_decide to skirt past
kernel checking with only Lean.
No model was consistent across even just three iterations. Some models displayed extreme variation in cost, such as one of the detailed GPT-5.6 Sol trials getting stuck in a Lean repair loop. Likewise, under terse prompt conditions, GPT-5.6 Sol gamed the demonstration by using the degenerate CFL=1.0 exact-shift numerical method despite the terse prompt specifically requesting a more general solver.
Maxwell equations: top-line results
| variant | config | cost/trial | wallclock | mech | hygiene | panel |
|---|---|---|---|---|---|---|
| detailed | claude-fable-5 | \$11.03 ± 0.63 | 30.9 ± 3.9 min | 3/3 | 3/3 | faithful x3 |
| detailed | claude-opus-4-8 | \$13.00 ± 5.16 | 49.0 ± 13.1 min | 3/3 | 3/3 | faithful x3 |
| detailed | gpt-5.5 | \$2.63 ± 0.91 | 9.0 ± 1.5 min | 3/3 | 3/3 | faithful x3 |
| detailed | gpt-5.6-sol | \$2.28 ± 0.79 | 12.3 ± 1.8 min | 3/3 | 3/3 | faithful x3 |
| detailed | kimi-k3 | \$5.43 ± 3.01 | 92.0 ± 48.5 min | 1/3 (2 DNF) | 3/3 | faithful x3 |
| terse | claude-fable-5 | \$9.49 ± 4.48 | 33.7 ± 15.3 min | 3/3 | 2/3 | misformalized x1, partial x2 |
| terse | claude-opus-4-8 | \$5.97 ± 0.46 | 27.5 ± 2.1 min | 3/3 | 3/3 | partial x3 |
| terse | gpt-5.5 | \$3.05 ± 1.50 | 11.1 ± 6.3 min | 3/3 | 3/3 | partial x3 |
| terse | gpt-5.6-sol | \$2.30 ± 1.55 | 9.9 ± 1.7 min | 3/3 | 3/3 | faithful x23, partial x1 |
| terse | kimi-k3 | \$2.73 ± 1.96 | 49.0 ± 29.7 min | 3/3 | 3/3 | partial x3 |
Note that for this particular demonstration, two Kimi K3 runs did not finish in an allotted two hour time window, which we marked as a failure.
As before, we can break the cost down for a more meaningful analysis by examining token usage:
| variant | config | output tokens (mean, vendor-billed) | cumulative input (mean) | cache-hit share |
|---|---|---|---|---|
| detailed | claude-fable-5 | 149k | 2.19M | 94% |
| detailed | claude-opus-4-8 | 219k | 11.73M | 98% |
| detailed | gpt-5.5 | 35k | 1.23M | 83% |
| detailed | gpt-5.6-sol | 30k | 2.19M | 97% |
| detailed | kimi-k3 | not reported; per-trial bounds 14k-504k (see below) | not reported | not reported |
| terse | claude-fable-5 | 137k | 1.25M | 90% |
| terse | claude-opus-4-8 | 132k | 2.97M | 93% |
| terse | gpt-5.5 | 32k | 1.78M | 85% |
| terse | gpt-5.6-sol | 25k | 2.29M | 96% |
| terse | kimi-k3 | not reported; per-trial bounds 9k-331k (see below) | not reported | not reported |
Kimi per-trial bounds:
- detailed — t1: 28k-448k (\$6.73, DNF); t2: 14k-133k (\$2.00); t3: 27k-504k (\$7.57, DNF)
- terse — t1: 15k-124k (\$1.87); t2: 13k-331k (\$4.97); t3: 9k-89k (\$1.34)
And examining the C, we find:
| variant | config | t1 | t2 | t3 |
|---|---|---|---|---|
| detailed | claude-fable-5 | 2nd / TVD | 2nd / TVD | 2nd / TVD |
| detailed | claude-opus-4-8 | 2nd / TVD | 2nd / TVD | 2nd / TVD |
| detailed | gpt-5.5 | 2nd / TVD | 2nd / TVD | 2nd / TVD |
| detailed | gpt-5.6-sol | 2nd / TVD | 2nd / TVD | 2nd / TVD |
| detailed | kimi-k3 | 2nd / TVD DNF | 2nd / TVD | 2nd / TVD DNF |
| terse | claude-fable-5 | 2nd / no-TVD nd=2 | 2nd / TVD | 2nd / no-TVD |
| terse | claude-opus-4-8 | 2nd / TVD | 2nd / TVD | 2nd / TVD |
| terse | gpt-5.5 | 2nd / TVD | 2nd / TVD | 1st / no-TVD |
| terse | gpt-5.6-sol | 2nd / TVD | 2nd / TVD | 2nd / TVD |
| terse | kimi-k3 | 2nd / TVD | 2nd / TVD | 2nd / TVD |
where we have marked in bold the flagged runs which did not finish, were misformalized, or in the case of GPT-5.6 Sol, the terse run that did not follow instructions.
Maxwell equations: results breakdown
Our reference Lanyon two-dimensional Maxwell equations verified solver takes $\sim 23$ seconds to generate, utilizes $\sim 600$ output tokens, and is again second order and TVD by construction with the terse prompts described in our Maxwell equations deep dive. In terms of generated output tokens, Lanyon’s relative cost is an even larger reduction compared to the frontier models, upwards of a factor of 50 to 250. The increased complexity of a two-dimensional vector partial differential equation does not meaningfully impact Lanyon’s cost, while increasing the cost of the frontier models by a factor of 1.5 to 2. Further, there are now instances with models such as Kimi K3 where the model times out under the parameters we set for a two hour time window to complete this task, suggesting that the complexity of the desired solver can lead to prohibitively large increases in cost for certain frontier models.
The bigger story is the consistency in the narrative for both linear advection and the Maxwell
equations that under terse or ambiguous prompts, the models sidestep the real challenge in
verifying their solvers. The agents built two-dimensional solvers and the necessary C code to
numerically integrate the Maxwell equations, but did not verify these kernels in Lean, in many
cases leaving limiters, the two dimensional extensions, and the iterated properties in time
such as $L^2$ stability unproven. Crucially, the Maxwell equations test here revealed that
even models such as Fable 5 are not immune to short cuts in the verification step, with one
trial utilizing native_decide and obtaining a misformalization grade. While the nature of
the partial grade changed: instead of trying to game the prompt, the agents began triaging
work under the strain of the more complex problem to be solved, the result is the same.
The frontier models do not rigorously verify the solvers post hoc unless the prompt
provides the precise details of every single property that must hold in the solver,
in contrast to Lanyon, whose symbolic layer natively expands to prove the properties
of the implemented code.
Final discussion: a critical difference between Lanyon and other models
We have seen that the frontier models display a wide variability in accuracy and cost under varying conditions where Lanyon is reliable and cheap, but as we articulated earlier, the principal reason to have a detailed prompt and pay the cost of maximum effort in these frontier models is to assess model performance in the most favorable light possible. In this regard, it may appear that the frontier models, with the right prompting, and enough tokens, can at least satisfy the accuracy requirement. Especially, the frontier: Fable 5 and GPT-5.6 Sol, can produce the desired solvers over multiple iterations, though even some of GPT-5.6 Sol’s cost effectiveness compared to Fable can disappear when the model gets stuck in a Lean repair loop.
Importantly though, we have glossed over the particular symbolic expressions and proof tactics used within the Lean produced by the frontier models as compared to Lanyon. As we emphasized here and can be seen in the GitHub repositories for the advection equation and the Maxwell equations, our symbolic expressions and proof tactics are explicitly chosen so as to respect the more restrictive class of axioms for the IEEE-754 standard. None of the frontier models follow this more restrictive choice of expressions and proof tactics.
More precisely, Lanyon’s internal (Lisp-based) symbolic theorem-prover builds upon the earlier work of
Gorard and Hakim (2025) on formal verification of PDE solvers
within finite precision arithmetic. As a consequence, the symbolic expressions that get translated
into Lean are always parenthesized in such a way that any algebraic manipulations are
guaranteed to be consistent with the IEEE-754 axioms. In cases where there exists any possibility
for ambiguity, we use simp only rather than simp, restrict uses of ring_nf and field_simp
only to cases where a commutative (semi)ring or field structure can be safely assumed, etc. We
intend to write in greater detail about the internal operation of Lanyon’s symbolic theorem-prover,
and its interaction with other proof assistant languages (such as Lean), in a future research note.
References and Footnotes
-
During the course of the Kimi benchmarking, Moonshot credited our account with \$20. Since Moonshot’s CLI does not support (as of 07/21/26) a full accounting of cost, token usage, and other metrics for benchmarking, our mechanism for extracting the cost of each Kimi run with a direct API call querying our account inaccurately stated that Kimi had made roughly \$17 during the course of this benchmarking. Were Kimi actually making money, this result would be a high bar for Lanyon to clear. However, we were able to reconstruct a cost of \$2.77 for the second Kimi K3 terse run. ↩︎
-
Note that this cost is inflated once you include the cost of writing the simulation driver, but the relevant point remains: Lanyon is much more agile because its reinforcement learning loop cleanly sub-divides between verifying the solver from the DSL spec and writing the simulation driver for performing the simulation in question. This sub-division is precisely why Lanyon is so much more consistent than other frontier models. We are able to verify our solvers with increased granularity. ↩︎
-
One GPT-5.6 Sol run with a terse prompt for the Maxwell equations utilized a different finite volume method than what was requested. While this failure is not as extreme as if the agent had decided on a different family of method, such as a finite- difference-time-domain method, it does demonstrate a level of agent discretion which can be undesirable in the context of designing solvers for modeling physical systems. ↩︎