Spend the GPU on language

An agent that answers every question with a model call is paying a language model to do arithmetic. Some of the work in a question is exact: filter these rows, find what is reachable from this node, check that a constraint holds. A CPU engine does that work correctly and almost for free. The model is only needed where the answer really is language.

compute-offload is the piece of Theorem that makes that split. The model writes the question down as a small graph of operations, and a planner sends each operation to the cheapest executor that is good enough for it.

Every operation gets a pocket

The planner has six kinds of executor, and it ranks them by cost. A fresh cached result comes first, then an exact CPU engine, then a verification engine, a learned executor, a cheap model and an expensive model. Each operation carries a quality floor, and the planner picks the first executor in that order that meets it.

In the demo plan, a filter and a reachability query both go to CPU engines. Only the synthesis step, which turns the results into prose, calls a model. Run the same reachability query again and it never reaches an engine at all: the cache already holds the answer.

Not another gateway

LLM gateways already route requests, but they route from one model to another. They pick a cheaper model, serve a semantically similar cached answer, or fall back when a provider is down. None of them sends a question to something that is not a model.

That is the square compute-offload fills: model to exact engine, with a quality floor on every operation. A gateway saves money by taking a little risk on quality. Offloading exact work saves money and makes the answer more correct, because a Datalog engine does not get multi-hop reachability almost right.

A receipt for every choice

Every routing decision writes a receipt: the operation, the executor that ran it, and a content hash of what it produced. In the demo, the filter and the reachability query each leave a receipt, and the ledger holds three entries once synthesis is done. The receipt shapes are a versioned open spec, so another tool can replay a plan and check that each step gives the same answer.

The receipts are also where the costs come from. The planner does not guess what an executor costs; it reads what earlier runs actually spent, and its estimates improve as the ledger grows.

Same start, different finish

The benchmark runs each query twice: once on the model alone, and once through the planner with the CPU executors switched on. It measures three kinds of question with a small local model, qwen2.5:0.5b, averaged over five seeds.

Symbolic questions are pure reachability. The model spends 5.5 GPU seconds and gets 0% of them right. The CPU executor spends no GPU time at all, a third of a second of CPU, and gets all of them right.

Control questions have nothing to offload, so both runs land within a second of each other: 22.4 against 21.4 GPU seconds. That bucket is there to show that the harness adds no cost of its own.

Mixed questions need both kinds of work. Both runs still call the model to write the answer, but with offload the exact results are bound into the prompt instead of being worked out in it, so the synthesis prompt shrinks from 1,828 tokens to 612. GPU time falls from 33.5 seconds to 3.4, and symbolic accuracy rises from 0% to 100%.

These are local numbers from a very small model, so the shape matters more than the absolute cost. The cost win grows with how much exact work there is to hand off. The correctness win holds wherever there is any.

Both figures are drawn with the Anatomy kit for isometric explanatory figures. The numbers come from the compute-offload README in Theorem at commit b2f927f.