Claude beweist Sicherheitseigenschaften in über 100 Open-Source-Bibliotheken

Aus dem Anhang [0]: „Die von Agenten geschriebenen Beweise sind genauso ‚gut‘ wie jeder andere Beweis desselben Theorems, insofern sie das Äquivalenztheorem beweisen. Es bleibt jedoch abzuwarten, ob Agenten diesen ausführlichen Beweisstil direkt auf komplexere Programme skalieren können. Erfahrungen aus anderen agentenbasierten Verifikationsprojekten wie MachCSL deuten darauf hin, dass die Antwort nein sein könnte: Die Agenten stoßen mit dem ausführlichen Beweisstil an eine Komplexitätsgrenze, und eine Skalierung erfordert, dass die Beweise um bessere modulare Abstraktionen und Denkprinzipien herum strukturiert werden. Wenn das der Fall ist, wie können wir Agenten helfen, die richtigen Abstraktionen zu entdecken und einzuführen, um diese Komplexität zu reduzieren? Erfordert dies Input von Experten für Beweistechnik, oder können wir gemeinsame Prinzipien extrahieren, die Agenten dabei leiten können, gute Abstraktionen zu entdecken, die skalierbare Beweise ermöglichen?“

Einige Mathematiker haben ein ähnliches Muster bei den jüngsten LLM-Beweisen beobachtet, was sie zu der Vermutung veranlasste, dass LLMs in ihrer mathematischen Fähigkeit direkt jenseits der konvexen Hülle der menschlichen Mathematik an eine Wand stoßen werden. Die Art von Beweisen, die in der formalen Verifikation erbracht werden, ist ein ziemlich interessanter Lackmustest für die Argumentationsfähigkeit von LLMs, da die betrachteten Systeme nicht unbedingt auf der Verteilung liegen (im Vergleich zur Mathematik, wo die „Systeme“ und Strukturen, mit denen gearbeitet wird, und Beweise über sie in Tausenden von einzelnen Büchern erscheinen), sodass die Vorteile, die vortrainierte LLMs durch breites Domänenwissen gegenüber Menschen haben, nicht wirklich viel bringen. Meiner Meinung nach ist diese Beobachtung […]

Für die Skeptiker: Ich hatte mit formaler Verifikation für mein Rust-Rewrite von Postgres ziemlich guten Erfolg. Ich habe einen Compiler geschrieben, der sowohl Rust- als auch C-Code nach Lean übersetzen kann. Sobald diese beiden Funktionen in Lean sind, lasse ich ein LLM einen Lean-Beweis schreiben, dass sie sich identisch verhalten.

Bisher habe ich bewiesen, dass sich etwa 12 % des Codes bei single-threaded Ausführung gleich verhalten. Das entspricht ungefähr 70.000 Zeilen C-Code. Dies hat sehr geringfügige Verhaltensunterschiede aufgedeckt, wie etwa, dass Gleitkommaoperationen auf verschiedenen Plattformen unterschiedliche Ergebnisse liefern können.

Ich arbeite daran, herauszufinden, wie ich das skalieren kann, aber ich sehe keine grundsätzliche Einschränkung, die eine weitere Skalierung verhindern würde.

Ich bin 35, ich bin am Arsch, wenn sie sich durchsetzen. Ich werde nicht ins Handwerk gehen, ich habe mit 27 das Baugewerbe aufgegeben, weil ich Programmieren so sehr liebe. Ich wollte mich im Baugewerbe praktisch jeden Tag umbringen. Ich habe meine Zwanziger weggesoffen, weil es so scheiße war. Ich bin jetzt seit Jahren nüchtern, einzig und allein wegen des Programmierens und weil ich tatsächlich liebe, was ich tue. Aber dieses Unternehmen stiehlt mir das, auf viele verschiedene Arten.

Ich habe einen Großteil meines Lebens und meine gesamten Ersparnisse in diesen Übergang investiert. Jetzt werde ich jeden Tag angeschrien, ich solle Elektriker werden, weil Anthropic behauptet, sie würden das Halteproblem auf irgendeine umständliche Weise lösen, sie müssen nicht einmal tun, was sie behaupten. Sie müssen nur 20 % der Branche davon überzeugen, dass sie es tun werden, und Leute wie ich werden nie die Chance bekommen, lange genug zu arbeiten, um in Rente zu gehen.

Ich glaube wirklich nicht, dass sie Erfolg haben werden, aber wenn doch, werde ich obdachlos sein und aus der öffentlichen Bibliothek heraus programmieren, weil ich nicht noch einmal von vorne anfange.

Habe das in den letzten Wochen bei der Arbeit gemacht. Extrem mächtig, wenn ein Agent einen PR mit einigen Experimenten öffnen kann, die zeigen, dass er eine Funktion mit SIMD oder CUDA schneller macht, und man ihn einfach selbstbewusst mergen kann, weil der PR einen Rocq-Beweis enthält, dass er verhaltensgleich zur ursprünglichen Implementierung ist.

Formale Verifikation wogegen?

Gegen die schwer fassbare formale Spezifikation mit 100 % Abdeckung, die jede beabsichtigte und unbeabsichtigte Eingabe, die Interessen jedes Stakeholders und jedes mögliche Nutzerverhalten abdeckt? Im Vibecoding-Zeitalter? Nein, die Seite hat die Anständigkeit anzuerkennen, dass es das nicht gibt.

Am Ende einigen sie sich darauf, Abstürze mit einem herkömmlichen Fuzzer zu finden, Abstürze zu beheben und dann ... einen formalen Beweis zu schreiben, dass der Absturz behoben ist? Das scheint ... ziemlich sinnlos zu sein? Übersehe ich hier etwas?

Ein Haus zu bauen hat drei Ebenen:

1. Vision: was wir wollen (unsere Absicht)

2. Bauplan: die Spezifikation, die wir geschrieben haben (unser Design)

3. Inspektion: Überprüfung, was wir gebaut haben, gegen den Bauplan (die Beweise)

Diese Forschung macht die Inspektion nahezu perfekt. Aber eine Inspektion prüft nur den Bauplan, nicht unsere Vision, also kann ein Haus, das nach dem falschen Bauplan gebaut wurde, eine perfekte Inspektion bestehen. Die andere Hälfte besteht darin, sicherzustellen, dass der Bauplan unserer Absicht entspricht und das so bleibt, während Agenten bauen. Ich arbeite daran, also denke ich, dass dies komplementär ist:

https://github.com/pullboard-dev/pullboard

Das schien eine hohe Wahrscheinlichkeit zu haben, aber da unsere Einführung von LLMs in der Software bisher meist darin bestand, Best Practices über Bord zu werfen, bin ich skeptisch, dass es uns zu erweiterter Verifikation führen wird.

Es ist wie Bezos, der darüber spricht, wie wir eine 3-Tage-Woche haben werden, während er seine Angestellten in Flaschen pissen lässt.