AWS Neurosymbolic AI Delivers Verifiable Agent Automation for Regulated Sectors

AWS believes that making its Automated Reasoning Checks feature on Bedrock generally available will instill greater confidence in enterprises and regulated industries to adopt and deploy more AI applications and agents.

The company further anticipates that methods like automated reasoning—which uses mathematical validation to establish ground truth—will help enterprises transition into neurosymbolic AI. AWS views this as the next significant evolution, and a key differentiator, in the AI landscape.

Automated Reasoning Checks allows enterprise users to verify response accuracy and detect model hallucinations. AWS first introduced the feature on Bedrock at its re:Invent conference last December, asserting it can identify nearly all hallucinations. Initially accessible to a limited set of users via Amazon Bedrock Guardrails, the tool lets organizations define responsible AI policies.

Byron Cook, Distinguished Scientist and Vice President of AWS's Automated Reasoning Group, told VentureBeat in an interview that the preview demonstrated the system's effectiveness in enterprise environments. It also helped organizations appreciate the value of AI that blends symbolic, structured reasoning with the neural network capabilities of generative AI.

“Automated reasoning falls under the broader concept of neurosymbolic AI,” Cook explained. “The growing interest in neurosymbolic AI made users realize just how crucial this technology is while they were actively using the tool.”

Cook noted that some customers allowed AWS to analyze their data and answer-annotation documents. The tool's performance was found to be comparable to that of a human with the rulebook in hand. He added that while concepts of truth and correctness can be subjective, automated reasoning largely avoids this ambiguity.

“It was truly remarkable,” he said. “To see people with logic backgrounds debate what was true in an internal chat, then point to the tool after a few messages and realize, ‘Oh, it’s correct,’ was amazing.”

For the general release, AWS has enhanced Automated Reasoning Checks with new features, including:

• Support for large documents of up to 80k tokens or approximately 100 pages
• Simplified policy validation with the ability to save and reuse test scenarios
• Automated scenario generation from predefined specifications
• Natural language suggestions for policy refinement
• Customizable validation settings

According to Cook, Automated Reasoning Checks validates an AI system's truthfulness by proving a model did not hallucinate a solution. This capability could provide greater assurance to regulators and regulated enterprises concerned about generative AI's non-deterministic nature producing incorrect outputs.

Neurosymbolic AI and Establishing Truth

Cook emphasized that Automated Reasoning Checks helps demonstrate key principles of neurosymbolic AI.

Neurosymbolic AI combines the pattern recognition of neural networks—used by language models—with the structured logic of symbolic AI. While neural networks learn from data patterns, symbolic AI operates on explicit rules and logical reasoning. Foundation models primarily rely on neural networks, making them susceptible to hallucinations—a major enterprise concern. Conversely, symbolic AI lacks flexibility without manual programming.

Influential AI voices like Gary Marcus have argued that neurosymbolic AI is essential for achieving artificial general intelligence.

Cook and AWS are enthusiastic about bringing neurosymbolic AI concepts to the enterprise. In a podcast, VentureBeat's Matt Marshall discussed AWS's focus on methods like automated reasoning checks, which apply mathematical and logical rigor to generative AI to reduce hallucinations.

Currently, few companies offer productized neurosymbolic AI solutions, including Kognitos, Franz Inc., and UMNAI.

Applying Mathematical Rigor to Validation

Automated reasoning functions by applying mathematical proofs to model responses for a given query.

It utilizes a method called satisfiability modulo theories (SMT), where symbols have predefined meanings, to solve problems involving both logic (if, then, and, or) and mathematics. The technique applies this method to a model's response, checking it against a set of policies or ground truth data without requiring multiple test runs.

For instance, an enterprise might want to verify the correctness of a financial audit. If a model flags a report for containing unapproved payments, automated reasoning breaks this down into a logical statement:

(forall ((r Report))

(=> (containsUnapprovedVendorPayments r)

(shouldEscalate r)))

It then references the definitions, variables, and types configured by the user in Bedrock Guardrails and solves the equation to prove the model's response was both correct and truth-based.

Ensuring Provably Correct AI Agents

Cook stated that agentic use cases stand to benefit significantly from automated reasoning checks. Broader access via Bedrock will help demonstrate its utility. However, he cautioned that automated reasoning and other neurosymbolic AI techniques are still in their infancy.

“I believe it will impact agentic AI, though that field is highly speculative at the moment,” Cook said. “Several techniques exist—like identifying ambiguity in a statement, pinpointing key differences between possible interpretations, and then seeking user clarification—that I think will be crucial. This mirrors the emotional journey I observed in customers who began experimenting with generative AI a few years ago.”