AWS is banking on the fact that by bringing its Automated Reasoning Checks feature on Bedrock to general availability, it will give more enterprises and regulated industries the confidence to use and deploy more AI applications and agents. 

It is also hoping that introducing methods like automated reasoning, which utilizes math-based validation to determine ground truth, will ease enterprises into the world of neurosymbolic AI, a step the company believes will be the next major advancement — and its biggest differentiation — in the world of AI.  

Automated Reasoning Checks enable enterprise users to verify the accuracy of responses and detect model hallucination. AWS unveiled Automated Reasoning Checks on Bedrock during its annual re: Invent conference in December, claiming it can catch nearly 100% of all hallucinations. A limited number of users could access the feature through Amazon Bedrock Guardrails, where organizations can set responsible AI policies.

Byron Cook, distinguished scientist and vice president at AWS’s Automated Reasoning Group, told VentureBeat in an interview that the preview rollout proved systems like this work in an enterprise setting, and it helps organizations understand the value of AI that can mix symbolic or structured thinking with the neural network nature of generative AI. 

“There’s this notion of neurosymbolic AI, that’s the sort of moniker under which you might call automated reasoning,” Cook said. “The rise of interest in neurosymbolic AI caused people, while they were using the tool, to realize how important this work was.”

Cook said that some customers allowed AWS to review their data and the documents used to annotate the answers as right or wrong, and found that the work generated by the tool performed similarly to humans with a copy of the rule book in front of them. He added that the concept of truth or correct can often be subject to interpretation. Automated reasoning doesn’t have quite the same issue. 

“It was really amazing! It was amazing to have people with logic backgrounds be in an internal communication channel arguing about what is true or not, and in five or six messages point to the tool and realize Oh, it is right,” he said. 

AWS added new features to Automated Reasoning Checks for general release. These include:

• Support to add large documents of up to 80k tokens or up to 100 pages 
• Simpler policy validation by saving validation tests for repeated runs
• Automated scenario generation from pre-saved definitions
• Natural language suggestions for policy feedback
• Customizable validation settings

Cook said Automated Reasoning Checks validates truth or correctness in an AI system by proving that a model did not hallucinate a solution or response. This means it could offer regulators and regulated enterprises worried that the non-deterministic nature of generative AI could return incorrect responses more confidence. 

Neurosymbolic AI and proving truth

Cook brought up the idea that Automated Reasoning Checks help prove many of the concepts of neurosymbolic AI. 

Neurosymbolic AI refers to the combination of neural networks used by language models, with the structured thinking and logic from symbolic AI. Where neural networks recognize patterns from data, symbolic AI uses explicit rules and logic problems. Foundation models often rely on neural networks or deep learning, but because the models base their responses on patterns, they are prone to hallucinations, a concern that continues to concern enterprises. But symbolic AI is not very flexible without manual instructions.

Prominent voices in AI, like Gary Marcus, have said that neurosymbolic AI is critical for artificial general intelligence. 

Cook and AWS have been excited to bring ideas of neurosymbolic AI to the enterprise. VentureBeat’s Matt Marshall spoke about AWS’s focus on methods like automated reasoning checks and combining math and logic to generative AI to cut down on hallucinations in a podcast. 

Currently, few companies offer productized neurosymbolic AI. These include Kognitos, Franz Inc. and UMNAI.

Bringing math to validation

Automated reasoning works by applying mathematical proofs to models in response to a query. 

It employs a method called the satisfiability modulo theories, where symbols have predefined meanings, and it solves problems that involve both logic (if, then, and, or) and mathematics. Automated reasoning takes that method and applies it to responses by a model and checks it against a set of policy or ground truth data without the need to test the answer multiple times. 

For example, in an enterprise setting, they want to prove that a financial audit is correct. The model responds that a report contains unapproved payments. Automated reasoning checks break this down to a logic string:

(forall ((r Report))

  (=> (containsUnapprovedVendorPayments r)

      (shouldEscalate r)))

It then goes into the definitions, variables and types set by the user on Bedrock Guardrails and solves the equation to prove that the model responded correctly and based on truth.

Making agents provably correct

Cook said that agentic use cases could benefit from automated reasoning checks, and granting more access to the feature through Bedrock can demonstrate its usefulness. But he cautioned that automated reasoning, and other neurosymbolic AI techniques, are still in its very early stages. 

“I think it will have an impact on agentic AI, though, of course, the agentic work is so speculative right now,” Cook said. “There are several techniques like this of discovering ambiguity in the statement then finding the sort of key deltas between the possible translations, and then coming back to you and getting refinement on that, which I think, will be key in terms of the emotional journey that I saw customers go through they began playing with generative AI a couple of years ago.”