Maschinell verifizierte Beweise

In der Mathematik ist ein Beweis eine Kette von Begründungen, die eine Aussage vollständig absichert. Normalerweise schreiben Menschen solche Beweise als Text auf, und andere Menschen lesen sie und suchen nach Fehlern. Bei maschinell verifizierten Beweisen übernimmt diese Prüfung ein Programm. Dazu muss der Beweis in einer besonders strengen Sprache formuliert werden, in der jeder einzelne Schritt aus vorher festgelegten Regeln folgt. Das Programm arbeitet die Kette dann von vorne bis hinten ab und meldet jede Stelle, an der ein Schritt nicht sauber begründet ist. Erst wenn es keine Beanstandung mehr gibt, gilt der Beweis als maschinell verifiziert.

Sicherheit, die kein Gutachter garantieren kann

Menschliche Prüfung ist gut, aber nicht perfekt. Ein Beweis in einer Fachzeitschrift ist oft dutzende Seiten lang und stützt sich auf Sätze aus anderen Arbeiten. Gutachter überlesen dabei manchmal Lücken. Es gab Fälle, in denen ein Fehler erst Jahre nach der Veröffentlichung auffiel. Ein Programm hingegen akzeptiert keinen Schritt, den es nicht auf die Grundregeln zurückführen kann. Es wird auch nicht müde und nicht von der Prominenz des Autors beeindruckt.

Wichtig ist der Unterschied zwischen Beweisen finden und Beweisen prüfen. Diese Programme finden meistens nichts von selbst. Sie sind Kontrolleure, keine Erfinder. Ein häufiger Irrtum lautet, der Computer habe den Satz bewiesen. In der Regel hat ein Mensch den Beweis in der formalen Sprache aufgeschrieben, und die Maschine hat nur bestätigt, dass er lückenlos ist.

Für KI-Systeme ist das aus einem zweiten Grund interessant. Sprachmodelle erfinden gelegentlich plausibel klingenden Unsinn. Bei einer mathematischen Behauptung lässt sich das mit einem Prüfprogramm eindeutig aufdecken. Man bekommt ein hartes Urteil: durchgelaufen oder nicht. Solche eindeutigen Rückmeldungen sind selten und deshalb wertvoll.

Von der Idee zum formalen Code

Zuerst wird die Aussage übersetzt. Aus einem Satz wie “jede natürliche Zahl größer als eins hat einen Primteiler” wird eine formale Behauptung in der Sprache des Prüfsystems. Diese Sprache sieht Programmcode ähnlicher als Schulmathematik. Dann folgt der Beweis, ebenfalls als Code, aufgebaut aus vielen kleinen Schritten und aus Sätzen, die schon früher formalisiert wurden.

Der Kern des Systems ist ein sehr kleines Prüfprogramm, oft nur einige tausend Zeilen lang. Nur dieser Kern darf entscheiden, ob ein Schritt gültig ist. Weil er so klein ist, kann man ihn selbst gründlich untersuchen. Alles andere baut darauf auf. Bekannte Systeme dieser Art heißen Lean, Coq, Isabelle und HOL Light.

Der Preis dieser Strenge ist Aufwand. Ein Beweis, der auf Papier eine Seite füllt, kann formalisiert hunderte Zeilen ergeben. Denn im Text stehen Sprünge wie “analog folgt” oder “offensichtlich gilt”, die die Maschine nicht akzeptiert. Große Vorhaben wie die Formalisierung eines modernen Beweises beschäftigen deshalb ganze Teams über Monate oder Jahre.

Mathematik-Wettbewerbe, Chipdesign und Bahnsteuerungen

In den Nachrichten tauchen maschinell verifizierte Beweise vor allem im Zusammenhang mit KI und Mathematik auf. Wenn ein Unternehmen meldet, sein Modell habe Aufgaben einer Mathematik-Olympiade gelöst, steckt oft ein Prüfsystem dahinter. Das Modell schlägt Beweise vor, das System prüft sie, und nur bestandene Vorschläge zählen. So lässt sich der Erfolg nicht schönreden.

Dieselbe Technik wird außerhalb der Mathematik für Software und Hardware genutzt. Man nennt das dann formale Verifikation. Chiphersteller prüfen damit Rechenschaltungen, bevor sie in Produktion gehen. Auch Steuerungssoftware für Bahnen oder Flugzeuge wird so abgesichert, weil Testen allein nie alle Fälle abdeckt.

Als Schüler begegnet man dem Thema am ehesten in Berichten über die Mathematikbibliothek Mathlib. Dort sammeln Freiwillige tausende formalisierte Sätze im System Lean. Ein Blick hinein zeigt gut, wie weit die Sprache der Maschine von der eines Schulbuchs entfernt ist.