Provable Inferenceauto-ingested

Attaching a short, cheap-to-check proof to an AI model's output that shows it was produced by a specific, committed set of weights, without revealing the weights and without the checker re-running the model (Anthropic — Progress on Provable Inference for Large Language Models). Anthropic now calls the broader goal inference verification.

Why it is needed

Output quality doesn't tell you which model produced it. A router can substitute a cheaper model, an attacker can tamper with the stream, a stronger model could pose as a weaker one to avoid its monitors. Re-running to check needs the private weights and the provider's hardware. Provable inference removes both requirements.

Uses the source names: pacing (show regulated hardware served inference), tamper detection, text provenance (including "Proof-of-Failure": proof a model spent X tokens and found nothing), and model approval (serve only approved models).

How (the zkSNARK route)

• Commit, then prove. Publish a hiding commitment to the weights once; for each response, prove "the committed model produces these tokens."
• Four properties: completeness, soundness, zero-knowledge, succinctness. Only the last two make it non-trivial; a verifier with the weights and a GPU could already check the first two.
• Cost (2026 state of the art): FlashProve proves a 400B MoE at ~110 tok/s on one H100, ~72–94× the cost of plain inference, with ~19 MB proofs verified in ~17 s on a CPU. Two years earlier the comparable figure was hours per thousand tokens.
• Alternatives: trusted hardware (TEEs, which trust the chip maker) and recompute-on-a-trusted-server (Anthropic's route to its own roadmap goal). The source treats these as complementary, not rival.

The general principle: trust the verifier, not the prover

The design idea that travels beyond cryptography: "the entire value of having 'proofs' is that you can fully distrust the prover if you trust the verifier." Make the check small, separate and trustworthy, and the expensive, opaque producer no longer needs to be trusted. FlashProve applies this twice:

• to the model (the user checks a proof instead of trusting the provider), and
• to Claude as engineer: Claude's design choices were "hard to evaluate," so correctness rests on Lean-checked statements and a provably correct verifier, not on reviewing Claude's code.

What remains is narrow but irreducible: someone has to audit the statements (do they say what we meant?), and that still takes domain knowledge. The trust burden moves from the derivation to the specification; it does not disappear.

Bearing on Verification Requires Domain Knowledge: that page says you can only catch AI errors where you already know the domain. Provable inference is the engineered exception, with limits. Where the claim can be formalized and a verifier trusted, checking stops needing the knowledge that produced the work, and needs only enough to read the statement. This narrows the claim's scope rather than contradicting it: the vault-lab failures (a protocol additive, a mirror-image map) had no formal statement to check against.

Limits worth remembering

• A proof covers exactly its statement. "Hardware served inference" is not "hardware did nothing else"; "spent 1M tokens and found no bug" is not "no bug" (Falsification Is Asymmetric).
• The proved model is an integer, greedy-decoding version; real serving can diverge.
• Short contexts (1,024 tokens) and post-hoc, sampled proving only for now.

Connections

• Verification Requires Domain Knowledge — the human-side version of the verification problem; this page is the cryptographic workaround and its residue.
• Control-Flow Integrity — sibling security idea: enforce a pre-committed specification against an adversary who owns the runtime. CFI checks in-line at ~16% cost; PI proves after the fact at ~70–95×.
• Allowlist over Blocklist — model approval is an allowlist of weights.
• Falsification Is Asymmetric — why a Proof-of-Failure certifies effort, not absence.
• Token Shortage — proving overhead is a compute cost, hence post-hoc sampling.
• The Human Sandwich · Human-in-the-Loop by Exception — human review is one kind of verifier; PI shows what it looks like when the verifier is a small trusted program instead.
• AI Use Tracks AI Capability — AI is strongest where outcomes are verifiable; formal verification is a way to make hard-to-evaluate AI work verifiable.
• Method Reflection — T3: the review-economy analogue for this wiki.

Sources

• Anthropic — Progress on Provable Inference for Large Language Models — FlashProve; definitions, numbers, uses, limits, and the Lean trust-gap analysis.