Kompetitive Interaktive Zertifizierung für automatisiertes Schließen

• Antragsteller: Professor Dr. Javier Esparza; Professor Dr. Rupak Majumdar
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung seit 2026
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 568501586

Automatisierte Beweiser wie SAT-Solver, SMT-Solver und Model-Checker werden in vielen Bereichen der Informatik weit verbreitet eingesetzt, sind jedoch nicht vor Fehlern gefeit. Um diesem Problem zu begegnen, erzeugen moderne Werkzeuge Korrektheitszertifikate, die unabhängig überprüft werden können. Zertifikate für coNP-vollständige Probleme wie UNSAT oder PSPACE-vollständige Probleme wie Hardware-Model-Checking müssen jedoch zwangsläufig superpolynomiale Worst-Case-Größen aufweisen, es sei denn, NP=coNP oder NP=PSPACE. Insbesondere erzeugen alle bestehenden Solver und Model-Checker Zertifikate mit exponentiellen Worst-Case-Größen. Dies wird zu einem praktischen Problem, da Zertifikate inzwischen Größen von mehreren Terabyte oder mehr erreichen. Interaktive Beweissysteme stellen eine prinzipielle Möglichkeit dar, diese Zertifikatsgrößen zu überwinden: In diesem Modell tauschen ein Prover und ein polynomiell beschränkter Verifier Nachrichten gemäß eines Protokolls aus, nach dem der Verifier entscheidet, ob der Prover eine Berechnung korrekt durchgeführt hat. Klassische Ergebnisse der Komplexitätstheorie zeigen, dass, während konventionelle Zertifizierung nur für NP möglich ist, Zertifizierung durch interaktive Beweissysteme (kurz: interaktive Zertifizierung) für alle PSPACE-Probleme möglich ist (Shamirs Theorem), was grundlegende automatisierte Beweisprobleme wie UNSAT, QBF oder Hardware-Modellprüfung einschließt. Trotz zahlreicher Bemühungen haben diese theoretischen Ergebnisse noch nicht zu praktischen automatisierten Beweisinstrumenten geführt. Der Hauptgrund dafür ist, dass bestehende Prover so konzipiert wurden, dass sie für beliebige Berechnungen und Algorithmen arbeiten, was sie in der Praxis ineffizient macht. Als Antwort darauf haben wir einen neuen Ansatz vorgeschlagen, bei dem wir sorgfältig einen spezifischen Lösungsalgorithmus für ein wichtiges Problem (z. B. UNSAT) auswählen und ein maßgeschneidertes, kompetitives interaktives Protokoll dafür entwerfen. Hier bedeutet "kompetitiv", dass der Prover des Protokolls im Vergleich zum Algorithmus nur einen geringen zeitlichen Overhead verursacht. Auf dieser Grundlage haben wir das erste interaktive Protokoll für QBF implementiert, das kompetitiv ist im Vergleich zu einem Standardalgorithmus für QBF auf der Basis von binary decision diagrams. Das Ziel dieses Projekts ist es, unseren neuen Ansatz auf die derzeit von SAT-Solvern, SMT-Solvern und Model-Checkern verwendeten Algorithmen auszudehnen, einschließlich des Davis-Putnam-Logemann-Loveland (DPLL)-Algorithmus, clause-driven clause learning (CDCL), DPLL(T), oder iteratives model-checking. Darüber hinaus werden wir untersuchen, wie wir unsere interaktiven Beweissysteme zu Zero-Knowledge-Systemen weiterentwickeln können – um sicherzustellen, dass der Verifier vom Prover überzeugt wird, ohne zusätzliche Informationen aus dem Prozess zu extrahieren.

• DFG-Verfahren: Sachbeihilfen