LLMs können Rust-Code generieren. Formale Beweise sind ein ganz anderes Problem.

Die Lücke zwischen korrektem Code und einem verifizierten Programm

LLMs können Rust schreiben, das kompiliert und sogar cargo test besteht. Was sie nicht zuverlässig können, ist einen formalen Beweis dafür zu führen, dass der Code für alle möglichen Eingaben korrekt ist.

Das Problem ist nicht die Rust-Syntax. Formale Verifikation erfordert, dass man angibt, was man beweisen möchte, die Invariante findet, die den Beweis ermöglicht, und beides in einer Sprache ausdrückt, die der Verifizierer akzeptiert. LLMs werden auf Quellcode trainiert, nicht auf das Beweisen. Sie sehen Theoreme, aber selten die zwanzig gescheiterten Versuche, die dem erfolgreichen Beweis vorausgingen.

Wenn Sie eine rekursive binäre Suche in GPT-4 einfügen und es bitten, „das zu beweisen“, erhalten Sie etwas, das wie ein Beweis aussieht. Es wird Loop-Invarianten und Vorbedingungen erwähnen. Es wird aber wahrscheinlich Syntax aus Dafny verwenden, Lemmata referenzieren, die nicht existieren, und Invarianten behaupten, die zu schwach sind, um die Nachbedingung zu etablieren. Es sieht richtig aus, bis man es überprüft.

Wie formale Verifikation von Rust tatsächlich aussieht

Rust hat mehrere Verifikationstools. Kani ist ein Model Checker, der alle möglichen Zustände einer Funktion bis zu einer Grenze erschöpfend erkundet. Prusti und Creusot sind deduktive Verifizierer, die Rust in Logik übersetzen und einen SMT-Solver bitten, Eigenschaften zu beweisen. Jedes erfordert Annotationen in einer bestimmten Syntax.

Hier ist eine einfache Funktion und wie ein echter deduktiver Beweis in Creusot aussieht:

// Requires creusot-contracts crate
use creusot_contracts::*;

#[requires(a.len() > 0)]
#[ensures(result == a[0])]
pub fn first<T>(a: &[T]) -> &T {
    &a[0]
}

Creusot überprüft, dass die Vorbedingung a.len() > 0 die Nachbedingung result == a[0] garantiert. Das ist trivial, weil die Logik einfach ist. Jetzt machen wir es schwieriger:

use creusot_contracts::*;

#[requires(n <= 1000)]
#[ensures(result == n * (n + 1) / 2)]
pub fn sum_to(n: u32) -> u32 {
    let mut i = 0;
    let mut s = 0;
    #[invariant(i <= n)]
    #[invariant(s == i * (i + 1) / 2)]
    while i < n {
        i += 1;
        s += i;
    }
    s
}

Die Invarianten sind der schwierige Teil. Ein Mensch schreibt sie, indem er darüber nachdenkt, was bei jeder Iteration wahr bleibt. Ein LLM könnte s == i * (i - 1) / 2 raten, weil dieses Muster in den Trainingsdaten vorkommt, oder es könnte die Invariante ganz weglassen und den Solver scheitern lassen.

Was passiert, wenn man ein LLM um einen Beweis bittet

Ich habe das mit mehreren Modellen getestet. Der Prompt war: „Schreibe eine verifizierte Rust-Funktion, die die Fakultät von n mit Creusot berechnet, mit vollständigen Vorbedingungen, Nachbedingungen und Loop-Invarianten.”

Die Antworten fielen in drei Kategorien.

Zuerst produzierten einige Modelle plausibel aussehende Annotationen, die aber die falsche Syntax verwendeten. Sie schrieben #[precondition(...)] statt #[requires(...)] oder mischten Prusti-Syntax mit Creusot-Syntax. Der Code würde nicht einmal parsen.

Zweitens produzierten einige Modelle syntaktisch korrekte Annotationen mit Invarianten, die zu schwach waren. Die Fakultätsfunktion braucht eine Invariante wie res == fact(i). Modelle schrieben oft res >= i, was wahr, aber nutzlos zum Beweisen der Nachbedingung ist. Creusot würde melden, dass es das Ziel nicht etablieren kann, und das LLM hatte keinen Mechanismus, das zu beheben.

Drittens hatten einige Antworten die Invariante richtig, aber halluzinierten ein Hilfslemma. Sie referenzierten eine math::fact-Funktion, die in Creusots Standardbibliothek nicht existiert. Der Beweis funktioniert nur, wenn man diese logische Definition selbst baut.

Keines der Modelle produzierte einen Beweis, der beim ersten Versuch bestanden hat.

Wo LLMs im Verifikations-Workflow tatsächlich helfen

Das bedeutet nicht, dass LLMs für die formale Verifikation nutzlos sind. Es bedeutet, dass man sie für die richtigen Aufgaben einsetzen muss.

Sie sind gut darin, Boilerplate zu generieren. Bei einer gegebenen Funktionssignatur kann ein LLM normalerweise die #[requires]- und #[ensures]-Klauseln produzieren, die die offensichtlichen Contracts erfassen. Für eine Funktion fn divide(a: i32, b: i32) -> i32 wird es korrekt #[requires(b != 0)] und #[ensures(result * b == a)] vorschlagen. Das sind keine tiefen Einsichten, aber sie sparen Tastenanschläge.

Sie sind passabel darin, Verifizierer-Fehler zu erklären. Wenn Creusot meldet „cannot prove loop invariant“, das Fehlermeldung in ein LLM einzufügen, liefert oft eine nützliche Erklärung, was die Invariante tun soll. Es wird nicht die genaue Invariante vorschlagen, die Sie brauchen, aber es wird den Suchraum eingrenzen.

Sie sind nützlich für die Übersetzung zwischen Verifikationssprachen. Wenn Sie einen Dafny-Beweis haben und ihn nach Prusti portieren möchten, kann ein LLM einen Großteil der syntaktischen Abbildung übernehmen. Die zugrunde liegende Logik ist dieselbe. Das ist genau die Art von Pattern-Matching-Aufgabe, in der LLMs brillieren.

Die fundamentale Einschränkung: Beweisen ist Suche, nicht Vervollständigung

Ein Beweis zu schreiben ist nicht wie einen Webserver zu schreiben. Wenn Sie einen Webserver schreiben, gibt es viele richtige Antworten. Wenn Sie einen Beweis schreiben, gibt es genau eine Antwort, oder eine kleine Familie von Antworten, und alles andere ist falsch.

LLMs sind Next-Token-Predictors. Sie generieren die wahrscheinlichste Fortsetzung gegeben den Kontext. Ein Beweisschritt ist nicht die wahrscheinlichste Fortsetzung. Es ist der Schritt, der die Beweisverpflichtung schließt, der die zwanzigstwahrscheinlichste Option oder die zweitausendste sein kann.

Betrachten Sie den Beweis, dass eine Sortierfunktion eine Permutation ihrer Eingabe zurückgibt. Der Schlüssel ist normalerweise die Definition eines Multisets oder das Zählen von Vorkommen. Ein LLM könnte vorschlagen, Längen zu vergleichen, was notwendig, aber nicht hinreichend ist. Es braucht einen Menschen, um zu erkennen, dass Längengleichheit nicht Implikation bedeutet, und die Zählinvariante einzuführen.

Model Checking mit Kani vermeidet einiges davon, weil es keine Invarianten benötigt. LLMs können kani::proof-Harnesses zuverlässiger generieren, weil sie wie Unit Tests aussehen. Aber Kani funktioniert nur für bounded verification. Wenn Sie einen unbounded proof brauchen, brauchen Sie immer noch den Menschen.

Ein praktischer Workflow, der beides nutzt

Wenn Sie Rust heute verifizieren wollen, hier ist ein Workflow, der tatsächlich funktioniert.

Beginnen Sie damit, den Code normal zu schreiben. Führen Sie cargo test aus. Dann fügen Sie Contracts hinzu. Verwenden Sie ein LLM, um die #[requires]- und #[ensures]-Klauseln aus der Funktionssignatur zu generieren. Überprüfen Sie sie sorgfältig. Das Modell wird die einfachen richtig bekommen und die schwierigen subtil falsch.

Führen Sie den Verifizierer aus. Er wird bei mindestens einer Schleife scheitern. Nehmen Sie die Fehlermeldung und bitten Sie das LLM, zu erklären, welche Invariante fehlt. Verwenden Sie seine Erklärung als Ausgangspunkt, nicht als Antwort. Schreiben Sie die Invariante selbst.

Iterieren. Der Verifizierer wird Ihnen sagen, ob Ihre Invariante stark genug ist. Das LLM wird es nicht. Behandeln Sie das Modell als einen Pair Programmer, der die Syntax kennt, aber noch nie einen Beweis zu Ende gebracht hat.

Die ehrliche Antwort auf die Frage

Können LLMs formale Beweise für Rust schreiben? Nein. Noch nicht. Nicht ohne einen Menschen, der die Logik versteht.

Sie können das Gerüst schreiben, Fehler erklären und zwischen Tools übersetzen. Aber die Invariante, das Lemma oder die Induktionshypothese zu finden, die den Beweis ermöglicht, ist immer noch eine menschliche Fähigkeit.

Wenn Sie nach einem Tool suchen, das es Ihnen erlaubt, Separation Logic oder Hoare-Tripel zu überspringen, ist ein LLM nicht das Richtige. Wenn Sie nach einem Tool suchen, das die Lernkurve flacher macht, indem es die Syntax und Boilerplate übernimmt, während Sie sich auf die Logik konzentrieren, ist ein LLM einen Versuch wert.

Beginnen Sie mit Kani, wenn Sie bounded checks ohne Invarianten wollen. Wechseln Sie zu Creusot oder Prusti, wenn Sie unbounded proofs brauchen. Verwenden Sie das LLM, um die Syntax richtig zu bekommen, aber erwarten Sie, den Beweis selbst zu schreiben.

---

Häufig gestellte Fragen

Was ist formale Verifikation in Rust?

Formale Verifikation verwendet mathematische Logik, um zu beweisen, dass ein Programm eine Spezifikation für alle möglichen Eingaben erfüllt. In Rust fügen Tools wie Kani, Prusti und Creusot Annotationen zu Funktionen hinzu, die Vorbedingungen, Nachbedingungen und Invarianten beschreiben. Ein Verifizierer prüft dann, ob diese Eigenschaften gelten.

Kann ChatGPT Beweise für Kani schreiben?

ChatGPT kann Kani-Proof-Harnesses schreiben, die wie Unit Tests mit #[kani::proof]-Attributen aussehen. Diese Harnesses sind einfacher zu generieren als deduktive Beweise, weil sie keine Loop-Invarianten benötigen. Komplexe Harnesses mit Assumptions und Assertions brauchen jedoch immer noch menschliche Überprüfung.

Was ist der Unterschied zwischen Kani und Creusot?

Kani ist ein bounded model checker. Er erkundet alle möglichen Ausführungspfade bis zu einer Grenze und prüft auf Panics oder Assertion-Failures. Creusot ist ein deduktiver Verifizierer. Er übersetzt Rust in logische Formeln und verwendet einen SMT-Solver, um Eigenschaften für alle Eingaben zu beweisen, einschließlich unbounded loops, benötigt aber vom Benutzer bereitgestellte Invarianten.

Warum haben LLMs Probleme mit Loop-Invarianten?

Loop-Invarianten erfordern Reasoning darüber, was über Iterationen hinweg wahr bleibt, was eine Form von inductive reasoning ist. LLMs werden trainiert, wahrscheinliche Textfortsetzungen vorherzusagen, nicht nach der exakten logischen Aussage zu suchen, die eine Beweisverpflichtung schließt. Die korrekte Invariante ist oft nicht das wahrscheinlichste nächste Token.