Anthropics Claude schreibt Code und beweist automatisch seine Sicherheit
decoder ·
Anthropic hat mit Theorem zusammengearbeitet, um zu demonstrieren, dass sein KI-Modell Claude automatisch mathematische Beweise generieren kann, die die Korrektheit von bestehendem Softwarecode verifizieren. In einem kürzlichen Projekt erstellte Claude innerhalb weniger Wochen etwa 180 Millionen Zeilen Beweiscode für 123 Open-Source-Bibliotheken aus Googles OSS-Fuzz-Projekt. Dieser autonome Prozess umfasste die Übersetzung von Absturztests in mathematische Probleme sowie die Analyse von kompiliertem Maschinencode, wobei ein unabhängiges Tool namens Rocq die Ergebnisse überprüfte. Während dieser Verifikationsphase identifizierte Claude Hunderte von Fehlern, die herkömmliche Testmethoden über Jahre hinweg verpasst hatten, darunter kritische Sicherheitslücken in weit verbreiteten PDF-Readern. Diese formalen Beweise unterliegen jedoch strengen Einschränkungen und gelten nur für spezifische Prozessorarchitekturen, single-threaded Programme und Eingaben unter 64 MB. Obwohl die Rechenkosten hoch bleiben, weist Anthropic darauf hin, dass neuere Modelle effizienter werden und weniger Tokens benötigen, um ähnliche Beweise zu lösen. Das Unternehmen zielt darauf ab, die KI-gestützte formale Verifikation so alltäglich wie das Standard-Softwaretesting zu machen, was möglicherweise transformiert, wie Entwickler KI-generierten Code vertrauen und überprüfen.
decoder