Amazon is implementing AI aggressively across its business in a bid to improve operational efficiency, delight customers, and ultimately make money. But adopting probabilistic systems that don’t always behave as expected and are prone to hallucinations also comes with risks. To help minimize AI-related risks, Amazon and its AWS subsidiary are turning to a time-tested but little-known technique dubbed automated reasoning.
Automated reasoning is a field of computer science designed to provide greater certainty about the behavior of complex systems. At its core, automated reasoning gives adopters strong assurances, based on logic and mathematics, that a system will do what it was designed to do.
Neha Rungta, who is the director of applied science at AWS, has a PhD in computer science from Brigham Young University and used automated reasoning techniques during her work at NASA Ames Research Center in Northern California.
“It’s the use of mathematical logic to prove correctness of systems and design systems in architecture code,” Rungta said. “Traditionally, these techniques were used in things like aerospace, where it’s critical to get systems correct.”
Since 2016, Rungta has been using her expertise to help AWS improve the security of its services. Her AWS resume includes two products, including IAM Access Analyzer, which is used to analyze Amazon IAM (Identity and Access Management) and its 2 billion requests per second, and Amazon S3 Block Access.
Automated reasoning techniques used to ensure critical flight control systems work as designed are now being applied to AI. (Source: Media_works/Shutterstock)
“[Amazon S3 Block Access] is powered by automated reasoning where, if a customer turns it on, they have an assurance that their bucket does not grant unrestricted access to the public, not today or any time in the future,” Rungta told BigDATAwire in an interview at re:Invent 2024 this week. “Even as AWS changes–because things change, we launch new features, new products all the time–that bucket will not grant unrestricted access.”
At re:Invent on Tuesday, AWS announced that it’s using automated reasoning with Amazon Bedrock, its service for training and running foundation models, including large language models (LLMs) and image models. The company said the service, dubbed Automated Reasoning Checks, is the “the first and only generative AI safeguard that helps prevent factual errors due to hallucinations using logically accurate and verifiable reasoning.”
While neural networks, such as the LLMs at the heart of GenAI, are powerful and provide greater predictive power than traditional machine learning techniques, they’re also often opaque, which limits their usefulness in some fields. By using an automated reasoning model atop the GenAI model, customers can gain more confidence that the model won’t misbehave for mysterious reasons.
It’s largely a rules-based approach, Rungta said.
“These are very different models than the LLM kind of models that you think about,” she said. “The way to think about those models is they’re a set of rules, a set of declarative statements about what’s true of the system. What are the assumptions? Given a certain set of inputs, what is the outputs that you want to make sure they hold?
Automated reasoning brings a rules-based approach to ensuring the proper behavior of probabilistic AI systems. (Source: Adam Flaherty/Shutterstock)
“There are different techniques to create and analyze these models,” she continued. “Some are based on proving formal theorems. Another one is based on satisfiability problems, so it’s essentially Boolean logic at the end of it. And some are based on code analysis techniques. So they’re very, very different than what you would think of large language models or foundational models.”
If automated reasoning can provide something resembling deterministic behavior to probabilistic systems, then why aren’t they more widely used? After all, the fear of an LLM doing or saying something toxic or erroneous is one of the biggest concerns in the current GenAI boom, and is preventing many companies from rolling out their GenAI applications into production.
The reason, Rungta said, is that automated reasoning comes with a cost. It’s not so much the computational costs of running the automated reasoning model, but the cost in developing and testing it. Adopters require not only expertise in this small branch of the AI field, but also in the domain for which automated reasoning is being applied. That’s why so far it has been restricted to being used in only the most sensitive areas where getting wrong answers can be catastrophic.
Amazon Executive Chairman Jeff Bezos is involved in the company’s internal AI projects.
“There’s tons of work that goes into how do you know that your rules are right for a complex system?” Rungta said. “That’s not easy. You have to do validation. How do you know how your rules interact with an environment? You don’t have the rules of the entire world.”
As some of these LLMs get smaller and better tuned to specific domains, the easier and less costly it will be to apply automated reasoning techniques to them, Rungta said. To that end, AWS also announced its new Amazon Bedrock Model Distillation offering alongside the Automated Reasoning Checks offering. These two techniques go hand in hand.
Amazon is looking to become a leader as the GenAI era takes off. The company has more than 1,000 AI projects internally, according to Amazon founder Jeff Bezos, who spoke at the New York Times’s DealBook conference this week. According to the Business Insider he is spending more time with the company to shepard some of these AI projects toward completion.
As we begin the agentic AI era, we’ll see that different AI agents have different jobs. It’s likely that we’ll see some AI agents that function as supervisors of worker agents, and these supervisory agents may be developed with automated reasoning capabilities.
AWS is a pioneer in the use of automated reasoning with AI. It doesn’t appear that any other companies are using this technique to improve the reliability of AI models and the applications they power. But Rungta is bullish that the technique has a lot to offer and ultimately will help to unlock the vast potential that AI holds.
“I do think generative AI is going to be transformative of how we live our lives,” she said. “The models are getting better every week, if not every day. It’s a fascinating time.”
This article first appeared on sister site BigDATAwire.
