Skip to content

Untrusted Solver with Trusted Checker

Architecture pattern — instantiates Generate-and-Verify Separation

Splits a hard task into a large untrusted solver that proposes an answer plus a certificate and a small trusted checker that validates it, so authority rests only in the checker.

Untrusted Solver with Trusted Checker is the archetype's architecture in its bare form: deliberately arrange a system so a big, fast, possibly proprietary or heuristic solver does the hard work of finding an answer and, alongside it, produces a certificate; a small, simple, thoroughly trusted checker then validates that the certificate proves the answer correct. The solver may be a black box, a vendor, a GPU cluster, or a language model — it is never trusted. All acceptance authority lives in the checker, built to be small enough to trust and cheap enough to always run. Its defining commitment, versus mechanisms that specify a particular checking technique, is the organizing decision itself: pay the cost asymmetry on purpose, keep generation and validation as separate roles, and never let the checker grow into a second solver.

Example

A logistics company buys route optimization from an outside vendor whose solver is a proprietary black box. Rather than trust the vendor's schedules or rebuild the solver in-house, the company requires each returned schedule to arrive with a certificate: for a claim of feasibility, the assignment of every delivery to a vehicle-and-time-slot that a checker can confirm violates no capacity, time-window, or driver-hours constraint; for a claim of optimality, a bound (such as a linear-programming dual) the checker can confirm the solution meets. A small in-house checker — far simpler than any solver — validates the certificate against the company's own constraints before a schedule is dispatched. If the vendor's solver has a bug or cuts a corner, the certificate fails to check and the schedule is rejected. The company gets to use a solver it does not trust while trusting only code it wrote and understands — the certifying-algorithm discipline.[1]

How it works

  • Demand a certificate, not just an answer. The solver's contract is to output evidence that makes its answer checkable, not merely the answer.
  • Keep the checker small and independent. The checker is written separately, ideally by a different party, and validates the certificate without redoing the search.
  • Trust the checker, distrust everything upstream. Soundness rests entirely on the checker; the solver's size, opacity, or provenance is irrelevant to correctness.
  • Guard the asymmetry. The design holds only while checking stays far cheaper than solving; a checker creeping toward the solver's complexity forfeits the whole benefit.

Tuning parameters

  • Certificate design — what evidence the solver must emit. A well-chosen certificate makes checking trivial; a poorly chosen one forces the checker to redo the solver's work.
  • Checker–solver independence — how separated the two are (different teams, languages, even organizations). More independence guards against shared bugs but costs coordination.
  • Property checked — feasibility only, or optimality, or full functional correctness. Checking more rules out more bad answers but demands richer, harder-to-produce certificates.
  • Coverage of the un-certifiable — what to do when the solver cannot certify part of its answer. Falling back to trust or to review there is where the guarantee quietly leaks.

When it helps, and when it misleads

Its strength is that you can harness the most powerful available solver — heuristic, proprietary, outsourced, AI — while keeping a correctness guarantee that depends only on a small artifact you control, and it localizes bugs to whichever side fails to produce or pass a certificate. It is the general pattern the other siblings are special cases of.

Its failure modes are the archetype's own, sharpened. The guarantee is only as good as what the certificate actually proves: a checker that validates a narrow technical property (feasibility) can silently bless an answer that is worthless on the property you cared about (real-world quality), substituting a checkable proxy for genuine validity. The checker can also drift toward the solver's complexity until it is no longer trustworthy or cheap, dissolving the asymmetry. And answers whose correctness resists certification tempt a fallback to trusting the solver just there. The classic misuse is declaring the system "verified" when the checker checks the easy thing rather than the thing that matters. The discipline is to keep the checker small, independent, and audited, and to make sure the property it checks is the property you actually need.

How it implements the components

  • generator_verifier_role_separation — the pattern is this separation: an untrusted solver role and a trusted checker role, held apart by design.
  • generation_verification_cost_model — it is chosen precisely on the asymmetry that checking is far cheaper than solving, and it lives or dies by keeping that gap open.
  • checkable_acceptance_predicate — acceptance is decided by an explicit predicate the checker evaluates over the certificate, not by trust in the solver.
  • soundness_boundary — all soundness authority is concentrated in the checker; the boundary of "what can be wrong without being caught" is exactly the checker's coverage.

It fixes the architecture, not the checking technique: re-deriving from a logical kernel (trusted_verifier_kernel) is Proof-Assistant Kernel Check; consuming a supplied witness or certificate (witness_or_certificate_contract) is Feasibility Certificate Check; a succinct, private cryptographic proof (privacy_and_disclosure_boundary) is Succinct Cryptographic Proof Verifier; and buying assurance by repetition (verification_redundancy_rule, probabilistic_error_budget) is Randomized Repetition and Error Amplification.

Notes

This is the parent pattern: a kernel check, a certificate check, a succinct proof, and a sandbox are all this arrangement with a specific checker slotted in. The recurring smell to watch for is checker-complexity creep — the moment the checker needs the solver's machinery to validate an answer, the asymmetry that justified the whole design is gone, and you are trusting two systems where you meant to trust one.

References

[1] A certifying algorithm returns, with each output, a certificate or witness that a separate, simpler checker can use to confirm the output's correctness — so a bug in the (possibly complex) algorithm cannot produce a silently wrong result that passes the checker. Mehlhorn and colleagues developed the discipline in the LEDA library. ↩