Instanziierungs- und lernbasierte Methoden im automatischen Gleichheitsbeweisen

Als NP-vollständiges Problem galt das Boolesche Erfüllbarkeitsproblem (SAT) lange als zu schwer, um für die Praxis relevant zu sein. Durch intensivste Forschung entstanden in den letzten 15 Jahren jedoch effiziente und mächtige Werkzeuge zur Lösung des Erfüllbarkeitsproblems (sogenannte SAT-Solver). Solche Werkzeuge finden inzwischen verbreitet Anwendung in der Praxis, etwa zur Verifikation von Hardwarekomponenten oder zur Lösung von Planungsproblemen. SAT-Solver werden mittlerweile auch in Verfahren des automatischen Beweisens angewandt. Dabei werden weit schwierigere Probleme durch ein Boolesches Erfüllbarkeitsproblem approximiert. Die folgenden zwei Verfahren dieser Art sind für dieses Projekt von Bedeutung: (1) Instanziierungsbasierte Beweistechniken wie das InstGen-Verfahren wurden für das Erfüllbarkeitsproblem in der Prädikatenlogik entwickelt, welches im Allgemeinen unentscheidbar ist. (2) Maximale Vervollständigung stellt ein SAT-basiertes Verfahren für Gleichungslogik da. Diese beiden Verfahren erwiesen sich im Vergleich mit anderen Techniken für die entsprechenden Probleme als schnell und effektiv. Dieses Projekt möchte die Grenzen und Möglichkeiten des SAT-basierten Theorembeweisens weiter ausreizen. Im ersten Schritt werden wir maximale Vervollständigung erweitern, um sie mit dem InstGen- Verfahren kombinieren zu können. Damit kann ein effizienter Theorembeweiser mit optimaler Unterstützung für Gleichheit implementiert werden. Bisherige Kombinationen von instantierungsbasierten Beweistechniken mit Techniken aus dem Gleichheitsbeweisen stellten sich als schwierig heraus. Wir erwarten jedoch, dass die Verbindung zweiter SAT-basierter Verfahren es erlaubt, Synergien bei den jeweiligen Approximationen zu nützen, und dadurch ein effizienteres Verfahren ermöglicht. Im nächsten Schritt werden wir Techniken des maschinellen Lernens verwenden, um die implementierten Beweiser zu optimieren. Diese Techniken erhöhen die Effizienz indem sie es erlauben, Beweisstrategien optimal an das Eingabeproblem anzupassen. Dazu gibt es bislang noch wenige Forschungsergebnisse, wir erwarten aber, dass sich die betrachteten Verfahren für derartige Optimierungen besonders gut eignen. Theorembeweiser stellen hochgradig komplexe Software dar, und sind daher notorisch fehleranfällig. Hinzu kommt, dass es praktisch unmöglich ist, die ausgegebenen Beweise manuell zu prüfen. Dies trifft auf SAT- basierte Beweiser umso mehr zu, doch es gibt bislang keine Möglichkeit, solche Beweise automatisch zu verifizieren. Daher werden wir im dritten Schritt des Projekts einen verfizierten Beweisprüfer für die implementierten Theorembeweiser entwickeln. Zusammengefasst möchte dieses Projekt die Grenzen des SAT-basierten Beweisens in dreierlei Hinsicht erweitern: Anwendbarkeit im Gleichheitsbeweisen, Flexibilitat und Effizienz sowie Verifizierbarkeit.

Automatisches Schließen (automated reasoning) beschäftigt sich mit der Entwicklung und Implementierung von Algorithmen, die logische Deduktion in einem Computersystem automatisieren. Solche Systeme sind wichtig, um Hardware- und Softwarekomponenten automatisch auf Korrektheit zu überprüfen, aber auch um Planungsprobleme zu lösen. Das Erfüllbarkeitsproblem der Aussagenlogik (SAT) stellt einen Spezialfall des automatischen Schließens dar. Als NP-vollständiges Problem galt SAT lange als nicht effizient lösbar. Dank des Fortschritts in der Forschung der letzten 20 Jahre sind SAT-Solver jedoch mittlerweile in der Lage, riesige Probleme effizient zu verarbeiten, und werden dementsprechend routinemäßig in vielerlei Anwendungen eingesetzt. Anstatt reiner SAT-Solver werden inzwischen vielfach SMT-Solver verwendet, die SAT-Solver um Prozeduren für Theorien wie Arithmetik ergänzen, und damit Effizienz mit höherer Aussagekraft verbinden. Viele Anwendungsprobleme des automatischen Schließens sind jedoch nicht mit einem SAT- oder SMT-Solver lösbar, sondern benötigen mächtigere Inferenzmechanismen. Dieses Projekt konzentrierte sich auf logisches Schließen mit Gleichheit - ein Fall von hoher praktischer Relevanz. Um eine effektive Behandlung der Logik mit Gleichheit zu ermöglichen, kombinierte dieses Projekt zwei SAT/SMT-basierte Algorithmen. Behandelt wurden dabei sowohl der Sonderfall, in dem die Eingabeformel einer Menge von (Un-)Gleichungen ist, wie auch der allgemeine Fall der Prädikatenlogik mit Gleichheit. (1) "Maximal completion" is eine schnelle und wirksame Methode zur Behandlung des besonderen Falls, in dem das Eingabeproblem nur aus Gleichungen besteht. (2) "InstGen" ist ein SAT-basiertes Verfahren des instanzbasierten Theorembeweisens, das zwar die ganze Prädikatenlogik unterstützt, Gleichheit bislang aber ineffizient behandelte. In diesem Projekt wurden diese beiden Ansätze zu einer kombinierten Methode vereinigt, die Synergien zwischen den beiden SAT-Anbindungen nutzen kann. Eine entsprechende Implementierung in der Anwendung maedmax wurde experimentell evaluiert. Zwecks Optimierung der Performance wurden Techniken des maschinellen Lernens verwendet, um bessere Strategien für die im Beweisprozess nötigen Entscheidungen zu entwickeln. Das schließt die Bestimmung kritischer Laufzeitparameter ebenso mit ein wie die Auswahl des nächsten zu bearbeitenden Literals. Zu diesem Zweck entwickelten und evaluierten wir auch neuartige Features eines Eingabeproblems, die in diesem Kontext relevant sind. Automatische Theorembeweiser stellen komplexe, und damit inhärent fehleranfällige Softwaresysteme dar. Auch wenn ein Beweis für ein Theorem ausgegeben wird, ist dieser oft zu lang, als dass er von einem Menschen kontrolliert werden könnte. Um daher die Vertrauenswürdigkeit von Tools wie maedmax zu erhöhen, wurde im Rahmen dieses Projekts ein Beweisprüfer entwickelt, mit dem die Ausgabezertifikate von maedmax kontrolliert werden können. Dazu wurde die Korrektheit aller in maedmax implementierten Algorithmen formell im dedizierten Beweisassistenten Isabelle bewiesen. Zusammenfassend wurden in diesem Projekt die Möglichkeiten des SAT/SMT-basierten Theorembeweisens mit Gleichheit ausgereizt und erweitert. Die Methode wurde mittels maschinellem Lernen optimiert, und ihre Korrektheit formell in einem automatischen Beweisassistenten bewiesen.