Computer-gestützte Verifikation existierender P/NP Beweise

Die berühmte P/NP-Frage gehört zu den anspruchsvollsten offenen Problemen der Informatik und ist eines der verbleibenden sechs ungelösten Millenniumsprobleme des Clay Institute. Trotz der Fortschritte, die in den Jahrzehnten, seit das Problem gestellt wurde, erzielt wurden, ist die Frage bisher nicht geklärt. Intuitiv ist sie leicht zu beschreiben: Betrachten Sie nur Problemstellungen, deren Antwort lediglich "ja" oder "nein" lautet. Darunter befinden sich auch solche, bei denen eine Ja/Nein-Antwort je nach Größe des Problems in " sinnvoller" Zeit berechenbar ist. Die Klasse all dieser Probleme nennen wir P. Angenommen, wir fragen nicht nach dem Lösungsweg, da eine Lösung schon gegeben ist. Dann besteht die Aufgabe in der Kontrolle, ob die vorliegende Lösung richtig oder falsch. Viele Probleme lassen eine solche Überprüfung in effizienter Weise zu. Diese Probleme bilden die Klasse NP. Die P/NP- Frage lautet: ist P = NP, P NP, oder (als dritte Möglichkeit), ist dies überhaupt beweisbar? Die scheinbare Einfachheit des Problems hat viele Forscher*innen dazu veranlasst, sich mit der Frage zu befassen, darunter Berufswissenschaftler*innen bis hin zu Hobbymathematiker*innen, die eine Vielzahl von Lösungsvorschlägen vorgelegt haben, von denen bisher keiner von der Fachwelt anerkannt wurde. Einige wenige Barrieren und "Sackgassen" auf dem Weg zu einer Antwort sind bekannt, aber die bloße Anzahl der veröffentlichten Beweisansätze wächst schneller, als die Fachwelt sie verifizieren kann. Langfristig könnte dies dazu führen, dass die richtige Antwort zwar gefunden wird, aber unter vielen Fehlversuchen unerkannt bleibt. Bis heute gibt es ca. 120 Beweisversuche, von denen eine knappe Mehrheit die Ungleichheit, eine Minderheit die Gleichheit, und ein kleiner Rest die Unbeweisbarkeit jedweder Antwort behauptet. In Anbetracht der Tatsache, dass das heutige wissenschaftliche Qualitätsmanagement stark von Peer- Reviews abhängt, die oft freiwillig und ohne Bezahlung durchgeführt werden, soll das Projekt dazu beitragen, dass Forscher*innen eine unabhängige und objektive Überprüfung ihrer Arbeit durch Computer erhalten können. Konkret werden im Projekt aus allen drei Kategorien (Gleichheit/Ungleichheit/Unbeweisbarkeit) Arbeiten auswählen, sie in eine maschinenlesbare Darstellung bringen, und einer automatisierten Verifikation durch Computer zuführen. Solche Beweisassistenten ermöglichen es, komplexe mathematisch/logische Argumente objektiv zu überprüfen, ohne hierfür freiwillige Gutachter*innen zu bemühen. Unabhängig von ihrer Bedeutung für die Wissenschaft ist die Beschäftigung mit der P/NP ein fruchtbares Forschungsfeld, das viele neue Konzepte und Ideen lieferte, die anderswo Anwendung fanden. Die maschinelle Verifizierbarkeit von P/NP-Beweisen (analog zur Natur der Klasse NP selbst) kann nicht nur ein Schritt in Richtung einer Antwort auf die Frage sein, sondern trägt jedenfalls auch zur Bedeutung von Beweisassistenten als mächtige Werkzeuge für die Forschung bei.

Für eine Vielzahl von Aufgabenstellungen bietet die Informatik effiziente Algorithmen zur Lösung an. Dies umfasst Berechnungsprobleme, Optimierungsprobleme aber auch reine Entscheidungsprobleme, deren Antwort lediglich "ja" oder "nein" lautet. Die Klasse "P" umfasst hierbei speziell letztgenannte Entscheidungsprobleme, sofern diese in "sinnvoller" Zeit lösbar sind, d.h. mit realistischem Ressourcenaufwand bzgl. Zeit und Speicher. Eine hierzu verwandte Klasse von Entscheidungsproblemen bildet die Klasse NP, bei welcher algorithmische Lösungen zwar bekannt, aber mit aktuellen Ressourcen nicht immer erreichbar sind. Dennoch erlauben viele der in NP enthaltenen Entscheidungsprobleme eine sehr effiziente Überprüfung einer gegebenen Lösung. Beispiele hierfür sind etwa das Problem der Handlungsreisenden (Finden einer kürzesten Route durch eine Reihe von Städten, ohne eine Stadt zweimal zu besuchen), oder auch das Platzieren von Personen um eine runde Tafel, sodass die individuellen Wünsche bzgl. linker und rechter Sitznachbarschaft berücksichtigt werden (bekannt als Hamilton-Kreis-Problem). Trotz der scheinbaren Einfachheit entziehen sich diese und viele weitere Probleme allen Versuchen einer effizienten Lösung. Das P/NP Problem ist die Frage, ob Probleme für die man eine gegebene Lösung schnell überprüfen kann, auch das Auffinden einer solchen Lösung ebenso effizient zulassen. Diese seit Jahrzehnten unbeantwortete Frage wurde zu einem der 6 Milleniums-Probleme erklärt, und gilt als eines der fundamentalsten Probleme der Informatik. Speziell der intuitiven Einfachheit wegen haben sich eine Vielzahl von Autor*innen, sowohl innerhalb als auch außerhalb der Wissenschaft an einer Lösung versucht, und mit Stand Herbst 2023 wurden mehr als 120 Beweisversuche veröffentlicht. Keiner von diesen konnte die wissenschaftliche Gemeinschaft bisher überzeugen, und die Vielzahl an Fehlversuchen führte dazu, dass wertvolle Ressourcen zur Überprüfung neu eingereichter Arbeiten bisweilen nur spärlich investiert wurden. Obgleich die Überprüfung neuer theoretischer Ergebnisse unabdingbar wichtig ist, genießt dieser Teil wissenschaftlicher Tätigkeit ein vergleichsweise geringeres Prestige und Ansehen als das Finden neuer Ergebnisse. Die Durchführung beider Tätigkeiten durch die gleiche Person oder Autor*innen-Gruppe wäre zwar wünschenswert, ist jedoch nicht zwingend ebenso objektiv. Das Projekt CAVE PNP hat somit das Ziel, die Machbarkeit einer Überprüfung mathematischer Beweise im Kontext der P/NP Frage durch computer-gestützte Beweisassistenten zu untersuchen. Hierbei handelt es sich zumeist um speziell gestaltete Programmiersprachen, welche die Konzepte, Strukturen und Schlussfolgerungsketten mathematischer Beweisführungen nachbilden, teilautomatisch finden oder überprüfen können. Dies ermöglicht einer oder mehrerer Autor*innen eines mathematischen Beweises eine unabhängige Überprüfung der Arbeit, zumal die computer-gestützte Verifikation keine formalen Ungenauigkeiten erlaubt. Die Mehrheit der wissenschaftlichen Gemeinschaft "glaubt" daran, dass P und NP verschiedene Problemklassen sind; eine etwas geringere Menge von Autor*innen glaubt an die Gleichheit der beiden Klassen, und ein paar wenige Arbeiten behaupten die generelle Un-Beantwortbarkeit der Frage. Was davon zutrifft wird die Zeit eines Tages zeigen; Die Fähigkeit zu einer objektiven Selbst-Überprüfung wissenschaftlicher Ergebnisse durch Beweisassistenten stellt hierbei eine spannende Möglichkeit dar, welche das CAVE PNP Projekt am Beispiel der P/NP Frage erforschte.