Automated Reasoning Checks Rewriting Chatbot: Reference Implementation Explained

AWS has published an open-source sample chatbot demonstrating how feedback from Automated Reasoning checks can be used to iterate on generated content, ask clarifying questions, and prove the correctness of answers. The implementation, described on the AWS Machine Learning Blog, also produces an audit log with mathematically verifiable explanations for answer validity, and a user interface that reveals the iterative rewriting process happening behind the scenes.

Automated Reasoning checks use logical deduction to demonstrate that a statement is true. Unlike large language models, they do not guess or predict accuracy — they rely on mathematical proofs to verify compliance with defined policies. This article walks through the implementation architecture of the rewriting chatbot and what it takes to adapt it.

Why Logic Checking Improves Accuracy and Transparency

LLMs can produce responses that sound convincing but contain factual errors — a serious problem in domains where wrong answers carry real cost. The reference implementation shows one mitigation pattern: validate every chatbot answer against an Automated Reasoning policy, feed the findings back to the LLM, and rewrite automatically until the answer is provably consistent with the policy.

The Chatbot Reference Implementation

The backend is a Flask application exposing APIs for submitting questions and checking answer status. To surface the system’s inner workings, the API also reports the state of each iteration, the feedback from the Automated Reasoning checks, and the rewrite signals sent to the LLM.

The frontend — built in React and served as static files by Flask — lets users configure which Amazon Bedrock LLM generates answers, select an Automated Reasoning policy for validation, and set the maximum number of rewrite iterations. Selecting a chat thread opens a debug panel showing each iteration of the content and its validation output. Once a response is proven valid, the interface displays a verifiable explanation of that validity:

How Automated Reasoning Checks Evaluate an Answer

When validating a question-and-answer pair, the check separates the input into factual premises and claims made against those premises. A premise can be a factual statement in the user’s question (“I am an S3 user in Virginia”) or an assumption in the answer; a claim is the statement being verified. Asked about S3 storage pricing across two regions, for example, the check produces one finding per independent logical statement — one validating the US East price, another the Asia Pacific price.

Each finding carries a validation result (VALID, INVALID, SATISFIABLE, TRANSLATION_AMBIGUOUS, IMPOSSIBLE) plus the feedback needed to rewrite the answer so that it becomes VALID. The feedback varies by result type: ambiguous findings include two competing interpretations of the input text, while satisfiable findings include two scenarios showing how a claim can be true in some cases and false in others.

Initial Feedback and Verification

When a user submits a question, the application first calls the configured Bedrock LLM to generate an answer, then calls the ApplyGuardrail API to validate it. Using the Automated Reasoning output in the ApplyGuardrail response, the application enters a loop: each iteration examines the findings, takes an action — typically asking the LLM to rewrite based on the feedback — and then calls ApplyGuardrail to re-verify the updated content.

The Rewrite Loop: Heart of the System

After initial validation, the system orders findings by priority — TRANSLATION_AMBIGUOUS, IMPOSSIBLE, INVALID, SATISFIABLE, VALID — and addresses the most important first. Because VALID is last in the priority list, the system only accepts a VALID result after the other finding types have been resolved. The handling logic works as follows:

• For TRANSLATION_AMBIGUOUS findings, the check returns two interpretations of the input text; for SATISFIABLE findings, it returns scenarios that prove and disprove the claims. In both cases the application asks the LLM to decide: rewrite the answer to remove the ambiguity, or ask the user follow-up questions. For example, SATISFIABLE feedback might indicate that a price of $0.023 holds only in US East (N. Virginia) — prompting the LLM to ask which region the user means. When the LLM chooses to ask, the loop pauses for the user’s reply, then regenerates the answer and restarts.
• For IMPOSSIBLE findings, the check returns the policy rules that contradict the accepted premises, and the application asks the LLM to rewrite the answer to remove the logical inconsistency.
• For INVALID findings, the check returns the policy rules that invalidate the claims, and the LLM is asked to rewrite the answer to conform to those rules.
• For VALID findings, the application exits the loop and returns the answer to the user.

After each rewrite, the system resubmits the question and answer through the ApplyGuardrail API, and the next iteration starts from that fresh feedback. Every iteration is stored with full context, so the system can always explain how it arrived at an answer.

Getting Started

Trying the reference implementation takes two steps. First, create an Automated Reasoning policy: open Amazon Bedrock in the AWS Management Console in a supported US or European region, navigate to the Automated Reasoning section, choose the option to create a sample policy, name it, and create it. Second, run the chatbot: clone the amazon-bedrock-samples repository, follow the README to install dependencies, build the frontend, start the application, and open it in a browser.

Backend Implementation Details

For teams adapting the implementation for production, five backend components do the heavy lifting:

• ThreadManager — manages the conversation lifecycle: creation, retrieval, and state tracking of threads, with locks enforcing thread-safe operations during the rewrite process.
• ThreadProcessor — runs the rewrite loop as a state machine, managing transitions between stages such as GENERATE_INITIAL, VALIDATE, CHECK_QUESTIONS, HANDLE_RESULT and REWRITING_LOOP to lead each conversation correctly through the process.
• Verification service — integrates with Amazon Bedrock Guardrails, submitting each LLM response for validation through the ApplyGuardrail API, handling retries with exponential backoff, and parsing results into structured findings.
• LLMResponse parser — interprets the LLM’s intent during rewrites. When asked to fix an invalid response, the model must decide whether to attempt a rewrite (REWRITE), ask clarifying questions (ASK_QUESTIONS), or declare the task impossible due to contradictory premises (IMPOSSIBLE). The parser detects markers such as “DECISION:”, “ANSWER:”, and “QUESTION:” in the natural-language output, handles Markdown, and enforces a configurable time limit.
• Audit logger — writes structured JSON logs recording two major event types: VALID_RESPONSE when a response passes verification, and MAX_ITERATIONS_REACHED when the system exhausts its retry budget. Each entry captures timestamp, thread ID, prompt, response, model ID, and validation findings, along with any clarifying-question exchanges.

Limitations and What to Watch

The approach verifies compliance with a policy, not truth in general: an Automated Reasoning check is only as good as the rules encoded in its policy, and authoring those rules for a complex domain is real work that the sample policy only hints at. The rewrite loop also adds latency and cost — each iteration is another model call plus a validation call — so production deployments need sensible iteration caps and user-facing messaging for the slow path. Finally, this is a reference implementation: the state machine, parser, and audit logger provide a solid skeleton, but authentication, rate limiting, and scaling are left to the adopter. Related reading on this site: governed enterprise agent orchestration with Agent Bricks.

The Bottom Line

Together, these components form a strong foundation for trustworthy AI applications that combine the flexibility of large language models with the rigor of mathematical verification — and an unusually transparent one, since every accepted answer ships with a provable explanation of why it is valid.

About the Original Authors

This article is adapted from a post written by members of the AWS Automated Reasoning team, including product manager Stefano Bulliani.