QBF-Beweise und Zertifikate

Mathematische Theoreme wie der Satz von Pythagoras oder der große Fermatsche Satz sind vielen Menschen geläufig. Mathematiker werden nicht nur dafür bewundert, diese Theoreme entdeckt zu haben, sondern auch für die Beweise, die diese Resultate untermauern. Ein Beweis garantiert die dauerhafte Gültigkeit eines Theorems, völlig unabhängig von künftigen Fortschritten in der Mathematik. Beweise haben in der Mathematik schon immer eine wichtige Rolle gespielt, genauso wie Zahlen, Funktionen, oder Gleichungen. Aber erst seit dem 20. Jahrhundert werden Beweise als eigenständige mathematische Objekte untersucht, wie etwa in den Arbeiten des österreichischen Logikers Kurt Gödel. Heute werden Beweise nicht nur in einem eigenen Zweig der mathematischen Logi k, der sogenannten Beweistheorie, und der philosophischen Logik untersucht, sondern auch in der Informatik. Dort garantieren Beweise die Sicherheit von Online-Zahlungsverfahren, Hardwaresystemen, sowie kryptografischen Protokollen. Im Zusammenhang mit Computern kann man sich Beweise als Zertifikate von wahren (1) und falschen (0) logischen Aussagen vorstellen, die die Korrekheit von Rechenergebnissen bestätigen, die ebenfalls als Folgen von Nullen und Einsen dargestellt werden. Wir möchten Beweise möglichst kurz halten, damit sie effizient übertragen werden können. Damit kommen wir zur zentralen Frage unserer Forschung: wie kurz kann ein Beweis sein? Die Größe eines Beweises entspricht der Anzahl von Bits in seiner Binärdarstellung. Die Beweisgröße hängt natürlich von der bewiesenen Aussage ab: je länger und komplizierter die Aussage, desto länger ist im Normalfall der Beweis. Aber um wieviel länger? Wenn die Beweisgröße exponentiell mit der Länge der Aussage wächst, werden Beweise für Anwendungen schnell zu groß. Das Gebiet der Beweiskomplexität beschäftigt sich mit solchen Fragen. Gegenstand dieses Forschungsprojekts ist eine Logik, die sich besonders gut dafür eignet, schwierige rechnerische Probleme als logische Probleme auszudrücken: die quantifizierte Aussagenlogik (engl. Quantified Boolean Formulas, kurz QBF). Das Ziel ist, kürzere QBF - Beweise für eine Reihe von Anwendungen zu ermöglichen. Wir orientieren uns dabei an neuesten Fortschritten beim automatisierten Lösen von QBFs, die wir um robuste Verfah ren zur Verifizierung von Lösungen erweitern wollen. Unser Vorhaben bewegt sich zwischen angewandter Forschung rund um das Lösen von QBFs, und theoretischer Forschung im Bereich der Beweistheorie. Wir erwarten, dass das Projekt neue Ergebnisse in diesen beiden Forschungszweigen nach sich ziehen wird.

Dieses Projekt hat theoretische Fortschritte erzielt, die es ermöglichen, computergenerierte Beweise kleiner und leichter zu überprüfen, wodurch die Grundlagen für sichere und vertrauenswürdige digitale Technologien gestärkt werden. Viele moderne digitale Systeme sind hochkomplex, führen jedoch kritische Aufgaben wie Benutzerauthentifizierung, Finanztransaktionen und Sicherheitskontrollen aus. Das bedeutet, dass diese Systeme äußerst zuverlässig sein müssen. Daher verwenden viele bereits versteckte mathematische Beweise, um die Korrektheit der Vorgänge sicherzustellen, und es wird streng getestete und theoretisch robuste unabhängige Software eingesetzt, um diese Beweise automatisch zu überprüfen. Im Laufe der Zeit wurden viele verschiedene Beweisverfahren entwickelt, entweder in der Hoffnung, einen bestehenden Ansatz zu verbessern oder neue Arten von Problemen anzugehen. Beweise können nur funktionieren, solange sie zuverlässig überprüft werden können, und eine große Anzahl von Regeln erschwert die automatische Überprüfung von Beweisen und macht sie anfälliger für Fehler, die katastrophale Folgen haben können. Unser Ansatz begann damit, eine Reihe ähnlicher Probleme zu gruppieren. Unser Hauptbeitrag besteht dann in der Vereinfachung einer großen Anzahl von Beweisregeln für diese Probleme auf nur fünf einfache Regeln. Dies wurde schließlich in der Arbeit "Better Extension Variables in DQBF via Independence" vorgestellt, da das Beweissystem, das wir Ind Ext QU-Res genannt haben, den Höhepunkt unserer Arbeit darstellt. Die Suche nach einem solchen Beweissystem wurde bereits vor Beginn des Projekts als langfristiges Ziel festgelegt, und seine Realisierung stellt einen bedeutenden theoretischen Beitrag dar. Die meisten anderen Arbeiten, die im Rahmen des Projekts in den letzten drei Jahren unterstützt wurden, legen entweder wichtige Grundlagen für dieses Beweissystem, tragen in irgendeiner Weise zum Nachweis der endgültigen Eigenschaften dieses Beweissystems bei oder zeigen, dass andere vorgeschlagene Regelkombinationen entscheidende Schwächen aufweisen. Die häufigste Schwäche besteht darin, dass es in einem Beweissystem eine Handvoll Fälle gibt, in denen Beweise unvermeidlich zu einer enormen Größe anwachsen, die praktisch unmöglich zu speichern und noch schwieriger zu überprüfen ist. Der andere Beitrag besteht darin, dass mit der Arbeit begonnen wurde, die numerische Daten statt reiner Binärdaten (wahr/falsch) umfasst. Dies hat zu neuen Fortschritten sowohl bei den Lösungstechniken als auch bei der Zertifizierung von Lösungstechniken und der Berechnungstheorie geführt. Dies erweitert das Potenzial unserer Arbeit. Zwar gibt es noch einiges zu tun, um die Lücke zwischen Theorie und Praxis zu schließen und den Anwendungsbereich beider auf neue Arten von Problemen auszuweiten, doch insgesamt hat das Projekt die Grundlagen der computergestützten automatisierten Verifizierung gestärkt, indem es neue Beweissysteme geschaffen hat, die einfacher, aber leistungsfähiger sind.