Case study: solving P-99 with LPTP and an LLM

Stellen Sie sich eine Welt vor, in der Computer nicht nur starre, roboterhafte Anweisungen befolgen, sondern tatsächlich die chaotische, unpräzise Art verstehen können, wie Menschen Probleme beschreiben. Dies ist die Grenze der Künstlichen Intelligenz, speziell eines Zweigs namens Large Language Models (LLMs). Betrachten Sie ein LLM als einen superintelligenten, unglaublich belesenen Studenten, der fast alles im Internet gelesen hat. Wenn Sie ihn bitten, eine Geschichte zu schreiben, kann er das; wenn Sie ihn bitten, Code zu schreiben, kann er das auch. Aber es gibt einen Haken: Dieser Student neigt zu „Halluzinationen“, was bedeutet, dass er voller Selbstvertrauen Fakten erfinden oder Code schreiben kann, der perfekt aussieht, aber heimlich abstürzt, wenn man versucht, ihn auszuführen.

Um dies zu beheben, nutzen Wissenschaftler die Formale Verifikation, die wie eine superstrenge Mathelehrerin ist, die jeden einzelnen Schritt der Hausaufgaben eines Schülers überprüft, um sicherzustellen, dass es logisch unmöglich ist, falsch zu liegen. In der Welt der Informatik gibt es eine berühmte Sammlung von Herausforderungen namens 99 Prolog Problems (oder P-99). Diese sind wie „Fitnessübungen“ für die Logikprogrammierung – ein Programmierstil, bei dem man beschreibt, was passieren soll, anstatt Schritt für Schritt festzulegen, wie es zu erreichen ist. Die große Frage, die Forscher stellen, lautet: Können wir den KI-Studenten den Code basierend auf einer einfachen englischen Beschreibung schreiben lassen und dann die Mathelehrerin sofort prüfen lassen, ob er tatsächlich korrekt ist? Dieses Paper untersucht genau dieses Experiment und verbindet die kreative Freiheit der KI mit der unerschütterlichen Sicherheit der formalen Logik.

---

Das Experiment: Ein Codier-Duo mit einer strengen Lehrerin

In dieser Studie beschloss ein Forscherteam, eine neue Arbeitsweise zu testen, die „Vibe-Coding“ mit „Vericoding“ mischt. Stellen Sie sich „Vibe-Coding“ so vor, als würde man einem kreativen Freund sagen, er solle ein Baumhaus bauen, basierend auf einer groben Skizze, die man auf eine Serviette gezeichnet hat. Man sagt: „Ich möchte ein Baumhaus mit einer Rutsche und einer Geheimtür“, und die Person fängt einfach an zu bauen. Es ist schnell und macht Spaß, aber das Ergebnis könnte wackelig sein. „Vericoding“ ist das Gegenteil: Es ist, als würde man einen Architekten engagieren, der Blaupausen, Belastungstests und Sicherheitsinspektionen verlangt, bevor der erste Nagel eingeschlagen wird.

Die Forscher wollten sehen, ob sie diese beiden Ansätze kombinieren können. Sie verwendeten ein KI-Modell namens Claude (speziell die Version Opus 4.6), das als kreativer Baumeister fungierte. Sie gaben ihm die ersten 33 Probleme aus der berühmten P-99-Liste, die in einfachem, informellem Englisch verfasst sind. Ein Problem besagt zum Beispiel schlicht: „Finde das letzte Element einer Liste.“

Die Aufgabe der KI war es:

1. Den Prolog-Code zu schreiben, um das Problem zu lösen.
2. Eine Testdatei zu schreiben, um zu prüfen, ob der Code bei Beispielen funktioniert.
3. Einen formalen Beweis zu schreiben, der mathematisch garantiert, dass der Code sicher ist, korrekt ist und immer zum Abschluss kommt.

Um die Beweise zu überprüfen, verwendeten sie ein Tool namens LPTP (Logic Program Theorem Prover). Betrachten Sie LPTP als die strenge Mathelehrerin, die „sieht richtig aus“ nicht als Antwort akzeptiert. Sie verlangt eine schrittweise logische Ableitung für jede Behauptung.

Die Ergebnisse: Eine Mischung aus Magie und Mathematik

Das Experiment war ein Erfolg, aber es war kein Zauberstab. Dem Team gelang es, 33 von 88 Aufgaben (etwa 37,5 %) mit dieser Methode zu lösen. Hier ist, was hinter den Kulissen geschah:

• Der kreative Teil (Vibe-Coding): Die KI war überraschend gut in der anfänglichen Programmierung. Sie schrieb 58 Logik-Prozeduren (den eigentlichen Code) und 508 Testfälle in nur wenigen Minuten pro Problem. Sie verstand die englischen Anweisungen und generierte Code, der korrekt lief.
• Der strenge Teil (Vericoding): Hier begann die eigentliche Arbeit. Die KI musste beweisen, dass ihr Code korrekt war. Sie generierte 257 Lemmata (kleine mathematische Fakten) und schrieb eine atemberaubende Menge von 11.800 Zeilen Beweis.
• Der menschliche Faktor: Die Forscher ließen die KI nicht einfach wild herumwurschteln. Sie überprüften manuell jede einzelne Datei. Sie führten die Tests aus, lasen die logischen Aussagen und ließen die Beweise erneut mit LPTP durchlaufen. Wenn die KI stecken blieb oder einen Beweis schrieb, der keinen Sinn ergab, griffen die Menschen ein, um ihr einen Hinweis zu geben. Zum Beispiel mussten die Menschen bei einem Problem über das Finden des letzten Elements in einer Liste die KI fragen: „Hey, wie hängt das mit der append-Funktion zusammen?“, um ihr zu helfen, den richtigen Beweis zu formulieren.

Die wichtigsten Erkenntnisse

Das Paper zeigt einige zentrale Dinge über diese neue Arbeitsweise auf:

1. KI wird gut im „Vibe-Coding“: Die KI konnte eine vage englische Beschreibung nehmen und sie sehr schnell in funktionierenden Prolog-Code umwandeln. Sie vermied sogar „unreine“ Tricks, die in realer Prolog-Programmierung oft vorkommen, und hielt sich an einen strikten, logischen Stil, den die Mathelehrerin (LPTP) verstehen konnte.
2. KI braucht einen Anstoß für „Vericoding“: Während die KI den Code leicht generieren konnte, war der Beweis, warum er korrekt war, schwieriger. Für komplexe funktionale Eigenschaften (wie etwa den Beweis, dass der Code genau das tut, was er soll) musste die KI manchmal die menschlichen Forscher bitten, die Logik zuerst in einfachem Englisch zu erklären. Sobald die Menschen einen Hinweis gaben, konnte die KI dies formalisieren und beweisen.
3. Es ist noch kein „gelöstes“ Problem: Das Team hat nicht alle 99 Probleme gelöst. Einige dauerten für die KI nur 15 Minuten (wie das einfache „letzte Element“-Problem), während andere mehrere Stunden dauerten (wie das „Primfaktorzerlegung“-Problem). Die Forscher stellen fest, dass die KI bei den schwierigsten Problemen immer noch Schwierigkeiten hat, von sich aus die richtigen Beweisstrategien zu entwickeln, ohne menschliche Anleitung.

Ein Blick in die Zukunft: Die „MCP“-Verbindung

Das Paper beschreibt auch ein neues Tool, das sie gerade entwickeln: das Model Context Protocol (MCP). Derzeit kommunizieren die KI und die Mathelehrerin (LPTP) über Dateien und Textdokumente, was ein wenig so ist, als würde man sich Briefe hin und her schicken. Das neue MCP-Tool ist wie eine direkte Telefonleitung zwischen ihnen. Dies ermöglicht es der KI, in Echtzeit um Hilfe bei der Mathelehrerin zu bitten, ihre eigene Arbeit sofort zu überprüfen und Fehler zu korrigieren, ohne darauf zu warten, dass ein Mensch eingreift. Sie testeten dies mit anderen KI-Modellen (wie Gemini) und fanden heraus, dass zwar einige Modelle die Ideen für Beweise generieren konnten, aber nur Claude in der Lage war, die gültigen Beweise zu generieren, die die strengen Prüfungen bestanden.

Das Fazit

Dieses Paper zeigt, dass wir in eine Ära eintreten, in der KI als kreativer Partner beim Schreiben komplexer, logischer Codes fungieren kann, aber immer noch einen menschlichen „Piloten“ benötigt, um sie durch die schwierigsten Teile zu steuern. Die KI kann den Code schreiben und sogar die mathematischen Beweise entwerfen, aber sie verliert sich manchmal in den Details. Durch die Kombination der Geschwindigkeit und Kreativität der KI mit einem formalen Beweisprüfer wie LPTP haben die Forscher ein System geschaffen, das die Fehler der KI abfängt, bevor sie zu echten Bugs werden. Es ist noch keine vollautomatisierte „Alles-Reparierer“-Maschine, aber es ist ein mächtiges neues Werkzeug, das das Schreiben zuverlässiger Software schneller und sicherer als je zuvor macht.