What is automated reasoning? How is it used in AI?
Automated reasoning is the area of computer science concerned with applying reasoning in the form of logic to computing systems. If given a set of assumptions and a goal, an automated reasoning system should be able to make logical inferences toward that goal automatically.
Computers that use automated reasoning can automate and apply logical reasoning to activities such as proving theorems, checking proofs or designing circuits. Automated reasoning can also use logic in the form of reasoning through analogy, induction, abduction and nonmonotonic reasoning. However, the term automated reasoning is mostly used when referring to deductive reasoning in mathematics and logic.
The term problem domain describes the class of problems presented to an automated reasoning program. Problem domains include problem assumptions, which are statements that provide relevant information to the automated reasoning system, and problem conclusions, which are the questions being asked of the system. The reasoning program will receive the problem domain as input and provide a result as output, such as the accuracy of a proof. An automated reasoning program will terminate when an answer is found, or resources are depleted.
The most common use of automated reasoning programs to prove theorems is by providing algorithmic descriptions of the calculus being used. Users are also required to define the class of problems the automated reasoning program will need to solve, the language the program will use to represent given information and what the program will use to implement deductive inferences.
The term automated deduction can also refer to automated reasoning. However, it is used more narrowly to refer to using deduction logic in mathematics.
How does automated reasoning work?
In a typical automated reasoning process flow, the problem to be solved is rendered as formal logic -- a set of premises and a goal or problem to be solved. This logic is processed using inference rules that are applied to generate a conclusion. The process returns a result: Either the goal follows logically, and a proof is offered; the goal is not provable, and a counterexample is produced; or there is no result at all, as the logic is incomplete, or the goal is irresolvable.
Automated reasoning examples
Automated reasoning is mostly used with deductive reasoning to find, check and verify mathematical proofs using a computing system. Using an automated reasoning system to check proofs ensures that the user has not made a mistake in their calculations. Automated reasoning can also be used for applications in mathematics, engineering, computer science or nonmathematical purposes. However, many of these other subjects still must be represented using a language the program understands.
To demonstrate how automated reasoning works, let's consider an AI agent that is used in customer service. These chatbots can generate relevant, factual responses based on existing knowledge, such as company policies. For example, an AI chatbot could use automated reasoning to verify that a customer service response aligns with organizational standards and factual evidence. These chatbots can offer customers automated 24/7 access and self-service options as well as verify customer accounts and route customers to the correct representatives.
In addition to customer service, other practical use cases for automated reasoning include the following:
- Verifying hardware and software reliability. Automated reasoning uses various techniques and approaches to verify that software works as intended and follows the necessary specifications and safety guidelines.
- Image analysis in healthcare. Automated reasoning can detect abnormalities in imaging such as X-rays, MRIs or CT scans that are not visible to the human eye.
- Defect detection in manufacturing. During product development robots can inspect systems using sensors and vision systems, ensuring products meet quality standards.
- Fraud detection in banking. Automated reasoning systems powered by AI can monitor transactions and detect suspicious activities in real time.
Automated reasoning can be used to create systems that think logically when solving problems and make decisions like humans, but faster and more accurately.
Automated reasoning and AI
Automated reasoning is a subfield of AI. However, the methods and implementation of both are unique enough that they can be thought of as separate entities. For example, AI typically uses a type of logic called modal logic, which uses classical logic while also expressing modality such as possibilities or impossibilities. The phrase AI also has connotations denoting a computer that works like a person, opposing how automated reasoning operates.
What are automated reasoning checks?
Automated reasoning checks are steps in automated reasoning processes that verify the accuracy and consistency process in pursuit of quality assurance. These can include the following:
- Validity. Checks the truth of a formula across models such as theorem proof.
- Consistency. Checks rule sets, ensuring that no fact contradicts another; for example, legal compliance.
- Equivalence. Checks whether two functions are logically identical, such as refactoring.
- Implication. Checks whether one logical statement properly follows from the previous statement, such as AI.
- Satisfiability. Checks a logical proposition to ensure that it can be true, such as bug detection.
- Model check. Determines whether a system model matches its own specification, such as hardware design.
The new Amazon Bedrock Guardrails machine learning tool from AWS validates AI-generated output to ensure accuracy and mitigate hallucinations. Alternative products include open source Llama Guard and Nvidia NeMo Guardrails.
AI hallucinations can cause major business disruptions. Learn how organizations can prevent hallucinations to improve the reliability and accuracy of their generative AI models.
