Was ist Automated Reasoning?
Automated Reasoning ist das Gebiet der Informatik, das versucht, Gewissheit darüber zu geben, was ein System oder Programm tun wird oder niemals tun wird. Diese Zusicherung basiert auf mathematischen Beweisen. Menschen lösen viele logische Probleme in Mathematik, Wissenschaft und Berechnung, indem sie logische Strategien wie Theoreme und Schlussfolgerungen anwenden. Automated Reasoning verwendet Computer, die dieselben Tools verwenden, um komplexe Herausforderungen zu lösen. Tools für Automated Reasoning versuchen, Fragen zu einem Programm (oder einer Logikformel) zu beantworten, indem sie bekannte Techniken aus der Mathematik verwenden. Mit den Tools können Sie überprüfen, was an einer Aussage oder einem Ausdruck wahr ist.
Welche Probleme kann Automated Reasoning lösen?
Wissenschaftler und Softwareentwickler verwenden Automated Reasoning, um zwei Dinge zu beweisen. Erstens beweisen sie, dass ein Systemdesign oder eine Systemimplementierung seinen Spezifikationen entspricht. Zweitens beweisen sie, dass es so funktioniert, wie es beabsichtigt war.
Automated Reasoning erreicht dies, indem es Beweise in formaler Logik liefert, die durch mathematische Theoreme oder bekannte Wahrheiten gestützt werden. Automated Reasoning verwendet mathematische, auf Logik basierende algorithmische Verifizierungsmethoden, um Sicherheits- oder Korrektheitsnachweise für alle möglichen Verhaltensweisen zu erbringen.
Automated Reasoning kann auch verwendet werden, um nachzuweisen, dass Systeme, die zur Konfiguration von Netzwerken, zur Erteilung von Netzwerkzugriffen bzw. zum Gewähren von Berechtigungen oder zur privaten und sicheren Aufbewahrung von Daten verwendet werden, wie vorgesehen funktionieren.
Wenn Sie Automated Reasoning verwenden, legen Sie dem System zunächst eine Problemstellung vor. Dann berechnet und validiert das Automated-Reasoning-System die Annahmen mit der Problemstellung. Die Software tut dies, bis alle Optionen ausgeschöpft sind.
Beispielproblem für Automated Reasoning
Um Automated Reasoning besser zu verstehen, sollten Sie die Problemstellung Leben Katzen an Land? und die folgenden Behauptungen betrachten:
- Katzen sind Säugetiere
- Säugetiere leben an Land
Das Automated-Reasoning-System bewertet, ob die Aussage in der Problemstellung wahr ist. Insbesondere verwendet es logisches Schlussfolgern. In diesem Fall sind Katzen Säugetiere und Säugetiere leben an Land. Es würde also bestätigen, dass Katzen an Land leben.
Einschränkungen des Automated Reasoning
Automated Reasoning macht keine Vorhersagen oder Verallgemeinerungen. Zum Beispiel können wir Automated Reasoning verwenden, um ein Argument wie dieses vorzubringen:
- Katzen haben Haare
- Fluffy ist eine Katze
- Fluffy hat also Haare
Wir können Automated Reasoning nicht verwenden, um Argumente wie diese vorzubringen:
- Katzen sind Säugetiere
- Katzen leben an Land
- Also leben alle Säugetiere an Land
Solche Anwendungen sind bei Theorembeweisern üblich, die bei der Ausführung von Aufgaben des deduktiven Denkens menschliche Anleitung benötigen.
Was sind einige Anwendungsfälle für Automated Reasoning?
Die Fähigkeit von Automated Reasoning, Schritt für Schritt logische Schlüsse zu ziehen, ist in mehreren Bereichen hilfreich. Mithilfe von Automated Reasoning können Sie die Sicherheit, Konformität, Verfügbarkeit, Haltbarkeit und Sicherheitseigenschaften großer Architekturen nachweisen.
Hier sind einige andere Anwendungsfälle für Automated Reasoning.
Mathematische Modellierung
Wissenschaftler, Ingenieure und Mathematiker lösen Probleme und verifizieren mathematische Beweise, indem sie algebraische Formeln in wissenschaftlichen Anwendungen anwenden. In solchen Praktiken verwenden sie mathematische Modelle, die sich auf mehrere Variablen stützen, um wahrscheinliche Lösungen für ein Problem abzuleiten.
Hardwareverifizierung
Automated Reasoning hilft Hardwareingenieuren dabei, zuverlässige Produkte zu entwickeln. Es ermöglicht ihnen, potenzielle Fehler zu entdecken, die bei herkömmlichen Testmethoden übersehen wurden.
Elektronikdesigner verwenden beispielsweise strenge mathematische Automated-Reasoning-Analysen, um schlüssig nachzuweisen, dass ein bestimmtes Hardwaredesign seinen Spezifikationen entspricht, z. B. beim Systemverhalten oder der Ausführung.
Die Verifizierung zeigt, dass alle möglichen Verhaltensweisen des Systems die zeitlichen Eigenschaften erfüllen, die die Spezifikation ausmachen. Es könnte auch zeigen, dass jedes mögliche Verhalten der Systemimplementierung mit einem gewissen Verhalten seiner übergeordneten Spezifikation übereinstimmt.
Softwarevalidierung
Softwareentwickler verwenden Automated Reasoning, um sicherzustellen, dass Anwendungen robust gegen unerwünschte Sicherheitsprobleme sind und dass die Software wie vorgesehen, bzw. entworfen, funktioniert. Wie bei der Hardwareverifizierung ermöglicht Automated Reasoning es Entwicklern, Softwaresicherheitsmaßnahmen anhand verschiedener Richtlinien zu validieren.
Beispielsweise beweisen die Techniker von Amazon Web Services (AWS) mit Autmated Reasoning, dass der Startcode für jede Startkonfiguration sicher ist. Ein weiteres Beispiel ist, dass sie nachweisen, dass die auf Amazon Simple Storage Service (Amazon S3) gespeicherten und verarbeiteten Daten geschützt sind. In diesem Beispiel verlassen sie sich bei Replikation, Konsistenz, Auto Scaling, Load Balancing und anderen Koordinationsaufgaben auf Automated Reasoning.
Modellierung des menschlichen Denkens
Informatiker verwenden Technologien für Automated Reasoning, um den Zugriff zu konfigurieren. Zu diesem Zweck schreiben sie Richtlinien, die beschreiben, wann Benutzeranfragen für den Zugriff auf eine Ressource zugelassen und verweigert werden sollen. Dadurch wird verifiziert, dass nur die vorgesehenen Benutzer Zugriff auf die Ressource haben, was für die Sicherheit und den Datenschutz der Ressource wichtig ist.
Informatiker verwenden beispielsweise Satisfiability Modulo Theories (SMT)-Formeln und SMT-Solver, um Sicherheitseigenschaften nachzuweisen.
Was sind einige Tools und Techniken für Automated Reasoning?
Als Nächstes stellen wir mehrere Methoden der automatisierten Schlussfolgerung vor, die es Computersystemen ermöglichen, menschliche Ableitungen durchzuführen.
Klassische Logik
Die klassische Logik ist eine mathematische Philosophie, die grundlegende Denkmodelle für automatisierte logische Denkprogramme bereitstellt. Diese Logik basiert auf dem Prinzip, dass jeder Satz einen Wahrheitswert hat, der entweder wahr oder falsch ist, aber nicht beides.
Sie konzentriert sich hauptsächlich auf Logik erster Ordnung, die es Mathematikern ermöglicht, unbekannte Variablen wie x mit Quantifikatoren darzustellen, wie sie in einem Satz existieren. Wissenschaftler wenden zum Beispiel klassische Logik in der Logikprogrammierung an, um x in diesem Satz zu finden: Es gibt x, sodass x an Land lebt und x ein Säugetier ist.
Aussagenlogik
Die Aussagenlogik ist ein Logiksystem, in dem es Aussagen gibt, die entweder wahr oder falsch sein können, und Beziehungen zwischen ihnen, die als Argumente bezeichnet werden, konstruiert werden.
Die klassische Aussage eines Arguments in der Aussagenlogik lautet Wenn P, dann Q. Wenn es zum Beispiel Samstag ist, dann ist es Wochenende.
Automated Reasoning verwendet eine Technik, die als SAT-Solving bezeichnet wird. Es verwendet Tools, sogenannte SAT-Solver, um nach befriedigenden Zuweisungen zu Argumenten in der Aussagenlogik zu suchen. Das bedeutet Variablen, die das Argument wahr machen.
Was ist der Unterschied zwischen Automated Reasoning und künstlicher Intelligenz?
Automated Reasoning ist eine spezielle Disziplin der künstlichen Intelligenz (KI), die logische Deduktion auf Computersysteme anwendet.
KI ist eine Wissenschaft, die Computern beibringt, beim Lösen von Problemen wie Menschen zu denken. Jüngste Entwicklungen in der KI haben zur Weiterentwicklung verschiedener Teildisziplinen geführt, darunter Deep Learning, Datenanalyse und Machine Learning.
Automated Reasoning unterscheidet sich von anderen KI-Technologien wie der natürlichen Sprachverarbeitung (NLP), bei der Computer darin trainiert werden, schriftliche oder mündliche Äußerungen zu verstehen. Stattdessen verwendet Automated Reasoning logische Modelle und Beweise, um Schlussfolgerungen über das mögliche Verhalten eines Systems oder Programms zu treffen, einschließlich über Zustände, die es erreichen kann oder niemals erreichen wird.
Was ist der Unterschied zwischen Automated Reasoning und Deep Learning?
Automated Reasoning beweist Eigenschaften eines Programms oder Systems. Es verwendet das Programm oder System selbst sowie ein Modell oder eine Spezifikation des Systems in der formalen Logik.
Deep Learning trifft Vorhersagen anhand der Anwendung statistischer Modelle auf große Datensätze.
Deep Learning ist eine fortschrittliche Technologie für Machine Learning, die simuliert, wie das menschliche Gehirn funktioniert. Es verwendet verschiedene neuronale Netzwerkmodelle, die aus mehreren Schichten von Neuronen bestehen, die relevante Informationen extrahieren, vergleichen und analysieren. Datenwissenschaftler nutzen Deep Learning für komplexe Anwendungen, beispielsweise für die Verarbeitung von Kamera- und Sensordaten in selbstfahrenden Autos.
Ist Automated Reasoning gleich Machine Learning?
Automated Reasoning und Machine Learning sind nicht dasselbe. Kurz gesagt, Machine Learning trifft Vorhersagen und zieht Schlüsse. Automated Reasoning liefert Beweise.
Machine Learning ist ein Teilbereich der KI, der Computer darin trainiert, Entscheidungen anhand großer Datenproben zu treffen. Datenwissenschaftler nutzen beispielsweise Machine Learning, um Banksoftware darin zu trainieren, betrügerische Aktivitäten zu erkennen. Sie verwenden große Stichproben von Finanzdaten, um sicherzustellen, dass die Software abnormale Muster auf der Grundlage zuvor erlernter Ergebnisse leicht erkennt.
Anstatt das Modell mit Daten zu trainieren, ermöglicht Automated Reasoning dem Modell, auf der Grundlage mathematischer Wahrheiten und Beweisen ein Ergebnis abzuleiten.
Wie nutzt AWS Automated Reasoning, um Serviceangebote zu verbessern?
AWS verwendet Automated Reasoning, um verschiedene Serviceangebote zu verbessern. Wir führen unterhalb ein paar Beispiele auf:
- Amazon CodeGuru Reviewer verwendet Automated Reasoning und Machine Learning, um Entwicklern bei der Identifizierung von Softwareschwachstellen zu helfen.
- Amazon Inspector Classic verfügt über eine Funktion zur Netzwerkerreichbarkeit, die Ihre EC2-Instances automatisch auf potenzielle Sicherheitslücken und Fehlkonfigurationen analysiert.
- AWS Identity and Access Management (IAM) Access Analyzer verwaltet Kontoberechtigungen mithilfe von Automated Reasoning.
- Amazon Virtual Private Cloud (Amazon VPC) Reachability Analyzer wendet Automated Reasoning an, um Ihnen zu helfen, Ihr AWS-Netzwerk zu verstehen und zu visualisieren.
Weitere Informationen zu Automated Reasoning in allen AWS-Services finden Sie unter Nachweisbare Sicherheit. Wir verwenden mathematisches Denken, um starke Sicherheitsgarantien für Ihre Sicherheits-Workloads zu bieten.
Beginnen Sie mit Sicherheit in AWS, indem Sie noch heute ein Konto erstellen.
Nächste Schritte in AWS
Sie erhalten sofort Zugriff auf das kostenlose Kontingent von AWS.
Starten Sie mit der Entwicklung in der AWS-Managementkonsole.