Anthropic hat sein Modell Claude eingesetzt, um mathematische Beweise für die Sicherheit von bereits bestehendem Code zu erstellen. Laut The Decoder entstanden dabei rund 180 Millionen Zeilen Beweiscode für 123 Open-Source-Bibliotheken. Das Modell stieß dabei auf Fehler, die jahrelanges Testen nicht aufgedeckt hatte.
Was formale Verifikation bedeutet
Klassische Tests prüfen, ob Software in ausgewählten Situationen das erwartete Ergebnis liefert. Sie decken allerdings nur Fälle ab, an die jemand gedacht hat. Bei der formalen Verifikation wird dagegen mathematisch bewiesen, dass ein Programm eine bestimmte Eigenschaft erfüllt, und zwar für alle möglichen Eingaben und nicht nur für Stichproben. Der Beweis selbst ist ebenfalls Code, den ein Prüfprogramm Schritt für Schritt kontrolliert.
Der Haken: Solche Beweise zu schreiben ist aufwendig und verlangt Spezialwissen. Deshalb wird die Methode bisher meist dort genutzt, wo Fehler besonders teuer wären. Genau hier setzt der Ansatz an. Wenn eine KI die Beweise erzeugt, könnte sich der Aufwand deutlich verringern.
Warum das für Entwickler interessant ist
Anthropic will formale Verifikation per KI nach Angaben der Quelle bald so praktikabel machen wie heutige Standardtests. Das wäre ein weiterer Schritt in der Automatisierung der Softwareentwicklung: Die KI schreibt nicht nur Code, sondern sichert auch dessen Korrektheit ab.
Nach der kurzen Meldung bleibt offen, wie viel menschliche Kontrolle nötig ist und für welche Arten von Fehlern die Beweise gelten. Ein Beweis ist immer nur so aussagekräftig wie die Eigenschaft, die er belegt. Wer Open-Source-Bibliotheken einsetzt, kann die Entwicklung im Auge behalten. Verlassen sollte man sich darauf aber erst, wenn nähere Details vorliegen.