Wenn KI den Code schreibt: Wer beweist, dass er funktioniert?
AI, Lean, and the Future of Formal Verification, with Lean Creator Leo de Moura
Leo de Moura, Schöpfer von Lean und Distinguished Scientist bei AWS, erklärt im Gespräch mit Ben Lorica, wie KI die formale Verifikation von einer Nischendisziplin zu einem praktischen Werkzeug macht. Frontier-Modelle übersetzen inzwischen Code beliebiger Programmiersprachen in Lean-Modelle und finden echte Bugs – der Claude-Code-Entwickler Boris ließ auf diese Weise Fehler aufspüren, ohne selbst Lean zu beherrschen. Doch ein maschinengeprüfter Beweis nützt nur, wenn das Modell den Code getreu abbildet. De Moura erwartet, dass sich die Softwareentwicklung deshalb von der Code- zur Spezifikationsarbeit verschiebt.
Es gibt inzwischen veröffentlichte Lean-Beweise mit 50 Millionen Zeilen. Mathlib hat zehn Jahre gebraucht, von Menschen geschrieben, um von null auf 2,5 Millionen zu kommen. Und jetzt schreiben Leute Beweise – die KI schreibt die Beweise – mit 50 Millionen Zeilen.
- wbeckler
Ich denke, die königliche Kombination ist Lean 4/TLA+/etc. plus KI plus ein deterministischer Generator. Für große Systeme müssen Aussagen aus formalen Methoden auf eine für Menschen verständliche Größe komprimiert werden. Das kann passieren, wenn die Aussagen die Korrektheit eines Modells und der daran angeschlossenen Codegeneratoren bestätigen. Der Generator kann Beweise für den generierten Code erzeugen, und ein Mensch muss nur sicherstellen, dass der Generator nachweisbar die korrekten Aussagen im großen Maßstab erzeugt.
So können formale Methoden KI für große Systeme einschränken.
Wir machen das bei der Open Markets Initiative, wo wir Millionen Zeilen von Lean 4, TLA+ und Rocq generiert haben, die sicherstellen, dass unser Open-Source-Code für ein elektronisches Handelsprotokoll korrekt ist. Wir hatten es nicht erwartet, aber der Lean-Prover hat tatsächlich einige fehlerhafte Schritte identifiziert.
- chamomeal
Was halten die Leute von Property-Based Testing? Ich habe ein paar Property-Based Tests eingerichtet, und es fühlt sich fast wie formale Verifikation an.
Ich weiß, es ist nicht dasselbe, aber PBTs können alle möglichen völlig verrückten Bugs aufdecken, nach denen ich nie suchen würde. Stateful-Kram, Cross-Service-Kram. Mein einziger Kritikpunkt an PBTs war immer das mühsame Setup, aber LLMs lösen das.
Ich habe in letzter Zeit nicht viel Diskussion über PBTs gesehen, aber im LLM-Zeitalter bekommt man eine Menge Gegenwert für seinen Aufwand.
- PandaRider
> ... Aber wir erwarten, dass sich die Leute in den nächsten Monaten und Jahren viel mehr auf die Spezifikationen konzentrieren werden, auf die Modelle, auf die Eigenschaften, die die Software haben soll.
Hat jemand Ressourcen zum Erlernen der Modellierung für formale Verifikation? (Muss nicht in Lean sein)
- fspeech
Derzeit sind die grundlegenden Theorien in mathlib unter der Annahme aufgebaut, dass formale Beweise teuer sind. Konzepte werden fragmentiert, um so viel Beweis wie möglich zu teilen. Mit LLMs ist diese Annahme nicht mehr korrekt. Konzepte und Beweise sollten so weit wie möglich an menschliches Denken angepasst werden, und Beweise können von LLMs zwischen Theorien portiert werden. Lean würde sicherstellen, dass die Übersetzung korrekt ist.
- westurner
Beispiele für den Vergleich der Ergebnisse von Lean und z. B. Rust, wie im Video beschrieben?
Ich habe symbolische Fehlerterme in Lean, die man vermutlich samplen und mit einer Monte-Carlo-Analyse vergleichen kann? Aber ich hatte bereits eine samplingbasierte Analyse, deshalb musste ich das alles (Doppelspaltexperiment und Gravitation mit GrC(2,4)) in Lean 4 machen.
Was wäre nötig, um Lean und eine oder mehrere Rust-TLA+-Implementierungen zu kombinieren? Wie plant und implementiert ein Agent das, und was sind die Vor- und Nachteile?
„Comparison of Isabelle/HOL, Lean, HOL4, and Agda: A Tale of Four Theorem Provers“ (2026), aber nicht Rocq?