Beweisassistent

Ein Beweisassistent ist ein Computerprogramm, mit dem man mathematische Beweise aufschreibt und prüfen lässt. Der Mensch gibt jeden Schritt an, das Programm kontrolliert, ob er wirklich aus dem Vorherigen folgt. Fehlt eine Begründung, meldet die Software das sofort und akzeptiert den Beweis nicht. Damit das möglich ist, muss alles in einer sehr strengen Sprache geschrieben werden, in der jedes Wort exakt festgelegt ist. Umgangssprachliche Formulierungen wie „offensichtlich gilt“ sind dort nicht erlaubt. Bekannte Programme dieser Art heißen Lean, Coq (heute Rocq) und Isabelle.

Warum Mathematiker einer Maschine das Nachrechnen überlassen

Moderne mathematische Beweise sind oft hunderte Seiten lang. Kein Mensch kann sie vollständig im Kopf behalten. Gutachter von Fachzeitschriften brauchen manchmal Jahre für die Prüfung, und trotzdem rutschen Fehler durch. Ein berühmtes Beispiel ist die Klassifikation der endlichen einfachen Gruppen: Der Beweis umfasst zehntausende Seiten von hunderten Autoren, und Lücken fielen erst Jahrzehnte später auf.

Ein Beweisassistent verschiebt das Vertrauen. Man muss nicht mehr darauf hoffen, dass alle Gutachter aufmerksam waren. Man muss nur noch dem sehr kleinen Kern des Programms vertrauen, der die logischen Regeln umsetzt. Dieser Kern ist bewusst so knapp gehalten, dass Fachleute ihn vollständig überprüfen können.

Der zweite Grund ist Software-Sicherheit. Programme in Flugzeugen, Chips oder Verschlüsselung dürfen keine Fehler enthalten. Testen findet immer nur die Fehler, an die jemand gedacht hat. Ein formaler Beweis zeigt dagegen, dass ein Programm unter allen möglichen Eingaben korrekt arbeitet. Der Betriebssystemkern seL4 und Teile der Chips von Intel und AMD wurden auf diese Weise abgesichert.

Von der Behauptung zum geprüften Beweisskript

Zuerst übersetzt man die Aussage in die formale Sprache des Systems. Aus „jede gerade Zahl größer als zwei ist keine Primzahl“ wird eine Zeile aus Symbolen, deren Bedeutung eindeutig festliegt. Diese Übersetzung ist oft der mühsamste Teil der Arbeit. Man muss auch alle benutzten Begriffe definieren, bis hinunter zu den Grundaxiomen.

Danach schreibt man den Beweis als Folge von Anweisungen, sogenannten Taktiken. Eine Taktik sagt etwa: „Führe eine Fallunterscheidung durch“ oder „Wende diesen bekannten Satz an“. Das System zeigt dabei laufend an, was noch zu zeigen bleibt. Man arbeitet also wie an einer Aufgabenliste, die man Schritt für Schritt abarbeitet, bis nichts mehr offen ist.

Wichtig ist die Abgrenzung zu vollautomatischen Beweisern. Ein Beweisassistent denkt sich die Beweisidee nicht selbst aus, er prüft nur. Er nimmt einem lediglich einfache Routineschritte ab. Man kann ihn sich wie einen extrem pedantischen Korrektor vorstellen: Er hat keine eigenen Einfälle, aber er übersieht auch keine einzige Lücke.

Lean, KI-Systeme und Mathematik-Wettbewerbe

In den Nachrichten tauchen Beweisassistenten meist zusammen mit künstlicher Intelligenz auf. Sprachmodelle erfinden gelegentlich falsche Begründungen, die überzeugend klingen. Ein Beweisassistent kann das aufdecken, weil er jeden Schritt nachrechnet. Deshalb koppeln Forschungslabore ihre Modelle an Systeme wie Lean: Die KI schlägt Beweisschritte vor, das Programm sortiert die falschen aus.

So funktionierten auch die Ergebnisse bei der Internationalen Mathematik-Olympiade. Systeme wie AlphaProof von Google DeepMind erzeugten Beweise in Lean, die dann maschinell geprüft wurden. Der Vorteil dieser Kopplung: Das Training bekommt ein verlässliches Signal darüber, ob eine Lösung stimmt. Bei normalem Text lässt sich das nicht so eindeutig entscheiden.

Außerhalb der Forschung begegnet dir das Thema vor allem bei sicherheitskritischer Technik. Wenn ein Hersteller mit „formal verifizierter“ Software oder Hardware wirbt, steckt fast immer ein Beweisassistent dahinter. In der Mathematik gibt es zudem große Gemeinschaftsprojekte wie Mathlib, eine offene Bibliothek mit über einer Million formal geprüfter Beweiszeilen.