Google DeepMind beweist die Sicherheit des Signal-Codes – mit KI-Agenten

Großartig, was für ein großartiger Anwendungsfall für KI. Ich habe das Gefühl, Google war von den großen Playern am saubersten, was nützliche Beiträge und die Kontrolle über ihre KI-Systeme angeht. Dieser neue Proof-Agent scheint allerdings nicht die Spezifikation herauszufordern, sondern nur die Implementierung, wenn ich das richtig verstanden habe.

Ich frage mich, wie sich dieser Agent von einem klassischen Coding-Agenten unterscheidet; am Ende scheint er genauso zu funktionieren, indem er über eine Codebasis iteriert, während er Lean- oder Rocq-Code schreibt und ausführt.

Ich erwarte, dass es sehr bald, vielleicht in den nächsten zwei oder drei Jahren, verrückt erscheinen wird, dass wir jemals _irgendeine_ unverifizierte Software auf unseren Systemen laufen ließen, so wie es heute verrückt erscheint, dass wir Telnet oder Klartext-HTTP verwendet haben.

Anfang dieses Jahres habe ich einige größere Refactorings an einem alten Projekt durchgeführt. Zu der Zeit nahmen Coding-Agenten richtig Fahrt auf, sodass man ihnen zunehmend für autonomere Arbeit vertrauen konnte, also war ich begeistert, es auszuprobieren.

Es führte das Refactoring durch, lief mehrere Stunden und bot am Ende auch noch eine umfangreiche Testsuite an. Alle Tests grün!

Ich war sehr beeindruckt, bis ich ein wenig genauer hinsah. Es hatte das Ganze rückwärts implementiert, auf eine Weise, die nicht nur sinnlos war (keines der erklärten Ziele erreichte), sondern die Dinge tatsächlich schlimmer machte als zuvor!

Bis zu diesem Moment war ich ziemlich optimistisch gewesen, was das Potenzial formaler Verifikation im KI-Zeitalter angeht. Aber als ich dieses Durcheinander sah, wurde mir klar, es hätte mir genauso gut einen mathematischen Beweis für den Code schreiben können, den es geschrieben hat, und der Beweis wäre durchgegangen, und der Code wäre trotzdem falsch!

Sehr cool. Vor ein paar Jahren habe ich mit dem Gedanken gespielt, ein spezialisiertes Modell für formale Verifikation zu entwickeln, mit etwas wie dem AlphaZero-Ansatz. Angesichts der Nachrichten der letzten Monate bin ich jetzt froh, dass ich es nicht getan habe; es scheint wirklich, dass Allzweck-LLMs alles auffressen.

Interessant, dass sie am Ende 26k Zeilen an Spezifikationen haben (einschließlich Arm-Semantik). Das ist eine ziemlich große Trusted Computing Base. Ich schätze, sie müssen die symbolischen/rechnerischen Modelle von Grund auf entwickeln. Es wird interessant sein zu sehen, ob wir wiederverwendbare Bibliotheken davon entwickeln können, à la mathlib, und wie die Anreize dort funktionieren. Die KI-Labore sind wahrscheinlich nicht besonders daran interessiert, und es ist auch wahrscheinlich undankbare Arbeit für die Forscher. Aber vielleicht, wenn Unternehmen, die Verifikation durchführen oder verifizierte Produkte verkaufen, aus dem Boden sprießen, gibt es einen Anreiz, die Arbeit zu teilen und eine standardisierte TCB zu haben. Das könnte, zum Guten oder Schlechten, auch den "Krieg der interaktiven Theorembeweiser" praktisch beenden.

Es ist auch interessant, wie sich das auf Code auswirken wird, der sich in Entwicklung befindet. ChatGPT behauptet, dass libsignal am Tag nach der Veröffentlichung erheblich geändert wurde :D Vielleicht könnte ein Zwischenmodell, ein nicht vertrauenswürdiges Modell in Rust, helfen (wobei sich der Großteil des Beweises auf das Rust-Modell zur Spezifikation bezieht und dann ein mechanischerer Beweis das Rust-Modell mit dem Binärprogramm verbindet); seL4 hat das vor langer Zeit gemacht. Aber ich habe keine Ahnung, ob das praktisch ist, ich habe noch nichts davon gehört […]

Ich habe damit experimentiert, wie einfach es für KI ist, Lean zu programmieren (https://metamagic.substack.com/p/beyond-the-proof-dump-lean-...), und ein paar Lektionen gelernt:

1. KI-Lean ist nicht perfekt, und KI kann leicht schummeln, da sie das Lean schreibt. Wer mit KI-Lean-Code herumspielt, braucht mindestens einen weiteren adversarialen Prompt, um das von der KI generierte Lean zu überprüfen.

2. Im Paper, als ich herumstöberte, sehe ich, dass sie einige Bugs wieder eingeführt haben, um zu verifizieren, dass es sie fängt, aber sie haben anscheinend keine Bugs gefunden. Vielleicht ist Signal einfach erstaunlich mit vielen Augen, die es überprüfen, aber die eigentliche Geschichte für den Rest von uns ist, dass, wenn man anfängt, mit KI nach Lean zu konvertieren, der Wert in den Annahmen liegt, die es findet. Selbst bei Dingen, von denen ich dachte, sie seien logisch wirklich dicht, fand Lean ein paar kleinere Dinge, die ich beheben musste. Ähnlich wie beim Fuzzing, wo ich noch nie keine Bugs gefunden habe, wenn ich Fuzzing in eine Codebasis eingeführt habe, erwarte ich dasselbe für die Konvertierung von Spezifikationen nach Lean.

3. Die Fähigkeit, Lean (kostengünstig) über KI zu generieren, ist ein sehr interessanter Türöffner für das Programmieren. Potenziell von Spezifikation zu Lean zu Code zu gehen und Lean als logischen Torwächter zu nutzen, könnte eine echte Fähigkeit sein, die täglich genutzt wird und nicht nur in der Forschung.

Noob-Frage: Abgesehen von diesen kryptografischen Systemen, wäre es nützlich, diese Beweise für allgemeine Softwarestücke zu erstellen? Konkret:

1. Hat jemand es auf Softwaresysteme angewendet, bei denen ein KI-Agent im Produktionsbetrieb im kritischen Pfad ist, d. h. nicht-deterministische Aktionen auftreten können (wenn auch mit Wiederherstellung)?

2. In welchen Szenarien macht es Sinn, von Anfang an einen Lean-Beweis zu haben? Ich stelle mir vor, wenn man ein Datenbanksystem mit einigen Garantien rund um ACID bauen wollte, wäre es vielleicht besser, das von Anfang an zu haben. Aber wahrscheinlich nicht so nützlich für den Bau eines API-gestützten Dienstes.

Großartig. Ich erinnere mich, letztes Jahr gedacht zu haben, dass Software bald viel fehlerhafter werden wird, da die Leute mehr an KI auslagern, aber Tools wie dieses geben mir Hoffnung, dass die Zukunft der Software vielleicht tatsächlich viel sicherer aussieht.