Das Logische digital untermauern

Dass 2 + 2 = 4 wahr ist, weiß eigentlich jeder. „Aber es reicht nicht aus, es zu wissen oder für gegeben hinzunehmen“, erklärt Professor Jasmin Blanchette, der seit März den Lehrstuhl für Theoretische Informatik und Theorembeweisen an der LMU innehat. „Man muss es logisch beweisen können.“ Blanchettes Fach erforscht die Grundlagen der Informatik, also Struktur, Verarbeitung, Übertragung und Wiedergabe von Informationen mittels Abstraktion und Modellbildung – und befasst sich konkret mit dem maschinell gestützten Beweisen von Theoremen. „Ein Theorem ist eine wahre logische Aussage oder Gleichung, die sich beweisen lässt.“ Dabei können sie sich seit einigen Jahren von Computerprogrammen unterstützen lassen, die man „Theorembeweiser“ nennt. „Ziel meiner Forschung ist es“, so Blanchette, „die Beweisautomatisierung zu stärken und effizienter zu machen.“

Aus Kanada stammend, hatte Blanchette Informatik an der dortigen Universität Sherbrooke sowie in Oslo studiert und sich schon in seiner Promotion an der Technischen Universität München (TUM) mit Theorembeweisern befasst. Im Anschluss forschte er zunächst an der TUM, dann am Inria in Nancy und am Max-Planck-Institut für Informatik in Saarbrücken und arbeitete zudem bei einem norwegischen Software-Unternehmen. Als Assistenzprofessor ging er 2017 an die Freie Universität Amsterdam, bevor er 2023 an die LMU berufen wurde.

„Ein bisschen wie Tippfehlersuche“

Markenzeichen seiner Forschung ist die Kombination automatischer und interaktiver Beweisprogramme. „Bei Ersteren prüft die Technik eine Logik vollautomatisch. Bei Zweiteren dagegen macht der Nutzer in einer Art Texteditor den ersten Schritt in der Beweiskette.“ Ein klassischer mathematischer Schachzug an dieser Stelle sei die „Induktion über x“. Das Programm biete daraufhin mehrere Unterfälle, für die es „quasi auf Knopfdruck“ des Benutzers hin nach Beweisen suche. „Funktioniert das nicht, muss der Nutzer wieder eingreifen – eine weitere Induktion vorgeben, den Satz vereinfachen oder dies und das umrechnen.“ Die automatischen Beweiser, die Blanchette in seiner Forschung selbst nutzt und entwickelt, sind textbasiert. „Sie ähneln Programmiersprachen wie Mathematica. Wenn ein Beweisschritt nicht korrekt ist, wird das angezeigt – ein bisschen so wie Tippfehler in Word, mit roten Unterstreichungen.“

Jasmin Blanchette ist Mitentwickler von interaktiven Theorembeweisern wie „Isabelle“, an dem er seit seiner Promotion an der TUM arbeitet, aber auch eines vollautomatischen Beweisers. Die relative Verlässlichkeit der Beweisprogramme lasse sich auf ihren sogenannten „kleinen Kern“ zurückführen, durch den alle Unterbeweise generiert würden. „Mit nur ein paar Tausend Codezeilen sind diese für Informatiker sehr überschaubar und lassen sich manuell leicht lesen und prüfen“, so der Forscher. „Damit werden alle komplizierten Beweise auf kleinschrittige, überschaubare Kernbeweise reduziert.“ Sei der Kern zu groß, könne man seine Ausgaben mit einem anderen, externen Ansatz prüfen. „Man nutzt also ein zweites Beweis-Programm, das die Ausgabe des ersten checkt.“

Die meisten Nutzer solcher Beweisassistenten fänden sich in der Informatik. „Ihnen helfen sie, Zeit zu sparen, weil ihre zu erbringenden Beweise umfangreich und manuell schwer zu beweisen sind.“ Mathematikern dagegen könnten die Programme helfen, manuell erbrachte Beweise für komplizierte Theoreme zu erhärten, Beweisketten abzukürzen oder allgemein bessere Ansätze zu finden.

Gottesexistenz und Sicherheitssoftware

„Auch Philosophen nutzen die automatischen Beweiser teilweise, etwa zur Frage der Gottesexistenz, und vereinzelt Computerlinguisten.“ Ein wichtiges Anwendungsbeispiel in der Industrie sei die Verifikation sicherheitsrelevanter Software, weshalb Blanchette an der LMU mit Lehrstühlen der Informatik kooperiert, die sich mit diesem Gebiet befassen.
Für die Zukunft wünscht Blanchette sich, dass automatische Beweiser routinemäßig für kritische Computerinfrastrukturen, den Entwurf von Programmiersprachen und allgemein für die Forschung in Informatik und Mathematik eingesetzt werden – und dass dies zu „vertrauenswürdigeren Systemen und Forschungsergebnissen“ führt. Ein Trend sei bereits jetzt der Einsatz von Künstlicher Intelligenz bei der Beweissuche.

Aber trotz aller mathematischen Raffinesse, Tausenden von Code-Zeilen und dem Einsatz von KI: „Hunderprozentig sicher sein, dass etwas wahr ist, kann man im Endeffekt nie – selbst bei 2 + 2 = 4“, so Blanchette. „Denn das ist – rein logisch – letztendlich unmöglich.“