Anthropic: Claude generiert汇编-Level-formale Beweise für 123 Open-Source-Bibliotheken

Anthropic arbeitet mit dem auf formale Verifikation spezialisierten Unternehmen Theorem zusammen, um bestehende Fuzzing-Tests in Open-Source-Projekte in mathematische Spezifikationen zu überführen. Claude erstellt daraufhin die Beweise, die anschließend vom Beweiskontrollsystem Rocq verifiziert werden. Laut Anthropic hat das Team innerhalb weniger Wochen Beweise für 123 Open-Source-Bibliotheken und 239 Testeintrittspunkte erstellt, wobei der gesamte Beweiscode etwa 180 Millionen Zeilen umfasst. Die zentrale Schlussfolgerung lautet: Bei Eingaben kleiner als 64 MB stürzen die gepatchten und für ein spezifisches RISC-V-Programm kompilierten Testeintrittspunkte unter festgelegten Linux-Response- und Speicherlayouts weder aufgrund von Speicherfehlern noch aufgrund fehlgeschlagener Assertionen. Beim Erstellen der Beweise hat Claude zudem bisher unentdeckte Fehler identifiziert und behoben, darunter Out-of-Bounds-Lese- und Schreibzugriffe, die nur durch seltene Eingaben ausgelöst werden. Im Gegensatz zum Fuzzing, das Stichproben wiederholt abtastet, decken formale Beweise alle Eingaben innerhalb des definierten Bereichs ab; die Gültigkeit der Schlussfolgerungen hängt jedoch von der Genauigkeit der Spezifikationen, des Maschinenmodells und des Prüfers ab. Die derzeit vorliegenden Beweise beziehen sich auf spezifische Laufzeitbedingungen wie Einzelthread-Ausführung und statisches Linking und decken nicht den gesamten Code jeder Bibliothek ab. Anthropic hat einen Teil der Beweise öffentlich gemacht, damit diese von externen Parteien überprüft und wiederverwendet werden können. Diese Studie demonstriert das Potenzial von KI, den Aufwand für formale Verifikation zu reduzieren, rechtfertigt jedoch nicht die Behauptung, dass die 123 Bibliotheken „fehlerfrei“ seien.