Beweisstrukturen: Beweise als formale Objekte und als Datenstrukturen

• Antragsteller: Dr. Christoph Wernhard
• Fachliche Zuordnung: Künstliche Intelligenz und Maschinelle Lernverfahren
• Förderung: Förderung seit 2021
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 457292495

Das Gebiet des Projekts ist Automated Reasoning, ein zentrales Teilgebiet der KI, das sich der Untersuchung schließenden Denkens mit Hilfe des Computers widmet und dessen Methodik theoretische und experimentelle Aspekte kombiniert. Typische Systeme des Automated Reasoning konstruieren Beweisstrukturen: Repräsentationen von Beweisen, verknüpften Folgerungsschritten. Beweisstrukturen lassen sich einerseits als formale Objekte betrachten, die in Beziehung zu logischen Formeln stehen, andererseits als Datenobjekte, die die formalen Objekte materialisieren und in praktischen Anwendungen als Eingaben dienen können. Beispiele sind dabei Anfrage-Umformulierung zur Wissensintegration, Synthese von Logikprogrammen sowie die Organisation von formalisiertem mathematischen Wissen. Im Kontext aktueller KI-Anwendungen sind Beweisstrukturen Erklärungen in einer idealen Form, die einen formalen Zugang ermöglicht, so dass ihre Untersuchung grundlegende und beispielhafte Erkenntnisse erwarten lässt. Generelles Ziel des Projekts ist die Verbesserung von Systemen des Automated Reasoning in der Leistungsfähigkeit beim Finden von Beweisen sowie durch Erweiterung des Anwendungsspektrums. Vor dem Hintergrund der Ergebnisse der ersten Förderperiode sind die Ziele der beantragten Fortsetzung im Einzelnen wie folgt: (1) Verbesserungen beim Finden von Beweisen. Bisheriges Ergebnis ist ein Framework, das von der Generierung von Beweisstrukturen ausgeht. Aus der Kombination von Merkmalen unterschiedlicher Beweiser-Paradigmen und der Einbindung von Beweiskompression resultieren neue Methoden. Ein schwieriges Problem wurde erstmals vollautomatisch gelöst. Das Projekt zielt nun auf ein tiefes systematisches Verständnis des Frameworks, neue Variationen, und Anwendbarkeit für weitere Problemklassen. (2) Verbesserungen und neuartige Anwendungen von Beweissystemen im Kontext einer großen formalisierten mathematischen Wissensbibliothek. Ziele sind, bisherige Projektresultate skalierend, Verbesserungen durch Beweisanalyse und maschinelles Lernen, sowie die Generierung alternativer Sichten auf mathematisches Wissen durch Umstrukturierung, Reduktion und Kompression von Beweisen. (3) Verbesserungen von Anfrage-Umformulierung durch Interpolation für die Wissensrepräsentation. Dabei wird die Ergebnisanfrage aus einem Beweis berechnet. Die erste Methode, die dabei allgemeine automatische Beweissysteme einsetzt, ist ein Projektergebnis. Ziel ist nun, den Bezug zu speziellen Anwendungsformalismen zu präzisieren. Ein weiteres Projektergebnis erschließt verschachtelte Relationen. Ziel ist, dies über automatisches Beweisen in die Praxis zu überführen. (4) Verbesserung von Programmsynthese in der Answer-Set-Programmierung, einem Ansatz zur deklarativen Problemlösung. Programmsynthese, auf Interpolation beruhend, ist ein aktuelles Projektergebnis. Ziel ist, dies in die Praxis umzusetzen, unter Berücksichtigung laufender Weiterentwicklungen der Answer-Set-Programmierung.

• DFG-Verfahren: Sachbeihilfen