Skip to content

PATTERN Cited by 2 sources

Post-inference verification

Pattern

  1. An AI component (LLM, agent, generator) produces an output y for input x.
  2. A mechanical reasoner (SAT/SMT solver, theorem prover, or spec-checker) evaluates y against a specification S.
  3. Based on the reasoner's verdict:
  4. proof → pass y downstream.
  5. counterexample → reject y; optionally regenerate with feedback, or fail closed.

The reasoner is the filter between model and production. Hallucinations that violate the spec are caught before they reach downstream systems or users.

    input x
       │
       ▼
  ┌─────────┐
  │   LLM   │ ── output y ──▶ ┌────────────┐
  └─────────┘                  │  reasoner  │ ── proof  ──▶ accept y
       ▲                       │  vs spec S │ ── CE     ──▶ reject / regenerate
       │                       └────────────┘
       │                              │
       └────── feedback loop ─────────┘

The Bedrock Guardrails instantiation

systems/bedrock-guardrails-automated-reasoning-checks is the canonical AWS product (launched in preview 2024-12-04, US West Oregon):

  • Customer authors (or imports) a specification S of the allowed output shape / content / constraints. The actual concepts/autoformalization pipeline: upload a source document (HR policy, airline policy, operational manual) + intent statement + sample Q/As → Bedrock decomposes the document, translates each unit from natural language to formal logic, validates translations, combines into a logical model, surfaces the result as typed variables + natural-language rules in a UI for review (Source: sources/2024-12-04-aws-automated-reasoning-to-remove-llm-hallucinations).
  • Bedrock runs the inference; the guardrail layer runs concepts/automated-reasoning against y vs S.
  • Verdict is one of three classes — Valid / Invalid / Mixed results — each paired with structured suggestions (Invalid: variable assignments that would make the answer valid; Valid: unstated assumptions required for the conclusion to hold; Mixed: list of findings). This is qualitatively richer than a scalar filter — the reasoner returns why it holds or how it fails.
  • Reported up to 99% provable accuracy for outputs that pass (Source: sources/2026-02-17-allthingsdistributed-byron-cook-automated-reasoning-trust-ai).

Critically: the accuracy number is not an average over a benchmark dataset. It is a provable lower bound for any output that passes, contingent on the spec being correct. This is qualitatively different from "our model gets 92% on MMLU."

Concrete regenerate-with-feedback loop

The 2024-12-04 preview post publishes the canonical realization of the regenerate-on-CE branch of this pattern (Source: sources/2024-12-04-aws-automated-reasoning-to-remove-llm-hallucinations):

for f in findings:
    if f.result == "INVALID":
        if f.rules is not None:
            for r in f.rules:
                feedback += f"<feedback>{r.description}</feedback>\n"

new_prompt = (
    "The answer you generated is inaccurate. Consider the feedback below within "
    f"<feedback> tags and rewrite your answer.\n\n{feedback}"
)

Key design choice: the feedback stays in natural language. The rule's natural-language description (not its formal-logic form) is what gets wrapped in <feedback> tags and returned to the LLM. The logical form is never exposed to the model — the spec surface is symmetric at authoring and feedback time.

Why this shape

  • LLM cheap + reasoner expensive per call. Running a prover on every candidate output is affordable precisely because the LLM has already collapsed the search space to a concrete artifact; the prover only needs to check, not generate.
  • Spec is smaller than the model. Authoring S is a one-time cost (with ongoing maintenance). The LLM is a ~10¹¹-parameter black box. The spec is kilobytes of temporal logic / constraints. The economics favor putting the proof burden on the spec side.
  • Hallucination is indistinguishable from correctness from the LLM's side. Only an external reference can tell them apart. The reasoner is that external reference, but one that does not require human oversight in the loop.

What the spec can say

Simple cases: - Numeric bounds ("the response quotes a price between $X and $Y"). - Schema compliance ("the JSON has fields id, amount, currency"). - Constraint satisfaction ("this code uses only functions from the allowed list").

Harder cases (the temporal / knowledge domain — see concepts/temporal-logic-specification): - "The response does not claim private information about a person not in the input." - "The generated code is semantically equivalent to the reference implementation." (the cryptographic-optimization case Cook names) - "The output correctly characterizes the zoning-code interpretation as of date D."

The harder the spec, the more of concepts/automated-reasoning is required underneath.

When this works (and when it fails closed)

Works when: - The domain has a specifiable correctness criterion. Crypto: yes. Code compilation: yes. Zoning code: yes. Creative writing: no (no spec). - The cost of a false-negative rejection is tolerable. The system will sometimes reject valid outputs because the reasoner cannot prove them correct. This is fail-closed by design. - The spec author can express the intended property. Autoformalization is the bottleneck; see concepts/specification-driven-development.

Fails when: - The property is inherently fuzzy ("is this response helpful?"). - The spec has latent contradictions. (Cook flags that humans often cannot agree on rules — the spec surfaces the conflict, which is good, but you cannot verify against a contradictory spec.) - The reasoner times out or hits undecidability. See concepts/automated-reasoning on the NP-complete / undecidable floor.

Comparison: post-inference vs in-loop verification

This pattern is post-inference — the reasoner runs after generation. The alternative is in-loop / tool-cooperation verification where the reasoner is invoked during the agent's reasoning, as a callable tool. Cook names both:

They compose: in-loop reasoning catches more cases early (the agent knows to be more careful when a claim is contested), but post-inference is the final backstop regardless of what the agent did internally.

  • patterns/envelope-and-verify — the capability counterpart: restrict what the agent can do, then verify its trajectory is within the envelope. Post-inference verification constrains outputs; envelope-and-verify constrains actions. Most production systems want both.
  • patterns/executable-specification — the development-time counterpart: the spec is part of the repo, property-tested against production. Post-inference verification moves the spec to runtime gating.

Seen in

Last updated · 200 distilled / 1,178 read