Automated Reasoning // mathematical proofs and logical deduction
LLMs/ML-models hallucinate make mistakes // how to fix/check that?
Amazon Web Services (AWS) has introduced Automated Reasoning checks in Amazon Bedrock Guardrails, a new safeguard that mathematically validates the accuracy of responses generated by large language models (LLMs) and prevents factual errors from hallucinations. This feature uses sound mathematical, logic-based algorithmic verification and reasoning processes to verify the information generated by a model, ensuring that outputs align with known facts and aren’t based on fabricated or inconsistent data.
Automated Reasoning checks are particularly useful for use cases where factual accuracy and explainability are important, such as validating LLM-generated responses about human resources (HR) policies, company product information, or operational workflows. This feature can be used alongside other techniques such as prompt engineering, Retrieval-Augmented Generation (RAG), and contextual grounding checks to provide a more rigorous and verifiable approach to ensuring that LLM-generated output is factually accurate.
To use Automated Reasoning checks, customers can create policies that encode their organization’s rules, procedures, and guidelines into a structured, mathematical format. These policies can then be used to verify that the content generated by LLM-powered applications is consistent with the guidelines. Customers can also test and refine their Automated Reasoning policies using the Test playground in the Automated Reasoning console.
The new Automated Reasoning checks safeguard is available today in preview in Amazon Bedrock Guardrails in the US West (Oregon) AWS Region. Customers can request access to the preview by contacting their AWS account team, and a sign-up form will be available in the Amazon Bedrock console in the coming weeks.
Automated reasoning is the field of computer science that attempts to provide assurance about what a system or program will do or will never do. This assurance is based on mathematical proof. People solve many logical problems in mathematics, science, and computation by using logical strategies like theorems and deductions. Automated reasoning uses computers that use the same tools to solve complex challenges. Automated reasoning tools attempt to answer questions about a program (or a logic formula) by using known techniques from mathematics. The tools help you check what’s true about a statement or expression.
Automated reasoning is a field of computer science that focuses on providing assurance about what a system or program will do or never do, based on mathematical proof. This is achieved by using logical strategies like theorems and deductions to solve complex challenges. Automated reasoning tools use known techniques from mathematics to answer questions about a program or logic formula, helping to check what’s true about a statement or expression. By producing proofs in formal logic supported by mathematical theorems, automated reasoning can verify that a system design or implementation obeys its specification and works as intended.
One of the key benefits of automated reasoning is its ability to prove properties of a system or program, such as security, compliance, availability, durability, and safety. This is done by using mathematical, logic-based algorithmic verification methods to produce proofs for all possible behaviors. Automated reasoning can be used to prove that systems used to configure networks, allow network access, or grant permissions work as intended. It can also be used to verify that data is private and secure. For example, automated reasoning can be used to prove that a system’s boot code is secure for every boot configuration.
Automated reasoning has several use cases, including mathematical modeling, hardware verification, software validation, and human reasoning modeling. In mathematical modeling, automated reasoning is used to solve problems and verify mathematical proofs by applying algebraic formulas in scientific applications. In hardware verification, automated reasoning helps hardware engineers build reliable products by discovering potential flaws overlooked by conventional testing methods. In software validation, automated reasoning is used to ensure applications are robust against undesired security issues and that software works as intended.
Automated reasoning differs from other AI technologies, such as natural language processing (NLP) and deep learning. While NLP focuses on training computers to understand written or verbal speeches, automated reasoning uses logical models and proofs to reason about the possible behaviors of a system or program. Deep learning, on the other hand, makes predictions based on applying statistical models to large datasets. Automated reasoning provides proof, rather than making predictions, and is based on mathematical truth and proof rather than large data samples.
At Amazon Web Services (AWS), automated reasoning is used to improve several service offerings. For example, Amazon CodeGuru Reviewer uses automated reasoning and machine learning to help developers identify software vulnerabilities. Amazon Inspector Classic has a Network Reachability feature that automatically analyses EC2 instances for potential security vulnerabilities and misconfigurations. AWS Identity and Access Management (IAM) Access Analyzer manages account permissions with automated reasoning, and Amazon Virtual Private Cloud (Amazon VPC) Reachability Analyzer applies automated reasoning to help understand and visualize AWS networks.
