Berkeleys Vero-Benchmark: bestenfalls 27 von 43 Projekten vollständig gelöst

Das RDI Lab der UC Berkeley hat einen Benchmark namens Vero veröffentlicht. Er verlangt von KI-Agenten, auf der Ebene eines gesamten Repositories zwei Dinge gleichzeitig zu leisten: jede erforderliche API zu implementieren und jede vorgegebene Spezifikation zu beweisen, während Code, Beweis und Build durchgehend konsistent bleiben. Bisherige Benchmarks zur formalen Verifikation blieben im Wesentlichen auf der Ebene einzelner Theoreme oder Funktionen stehen – dies ist der erste auf Repository-Ebene.

Die Aufgabe besteht aus 43 mehrmoduligen Lean-4-Projekten, portiert aus bestehendem Code in Python, Dafny, Verus und Coq, mit insgesamt 743 APIs und 2.705 formalen Spezifikationen. Die Bewertung läuft in zwei Modi: Im reinen Beweismodus wird eine Referenzimplementierung vorgegeben, der Agent muss nur beweisen; im Code-und-Beweis-Modus muss der Agent die Implementierung selbst schreiben und anschließend beweisen, dass sie die Spezifikation erfüllt.

Die Punktetabelle

Anzahl vollständig gelöster Instanzen (von maximal 43) bei einem Budget von 90 Minuten:

Der Graben zwischen der ersten und der dritten Zeile verdient einen genauen Blick: Bei identischem GPT-5.5 und identischem Codex springt das Ergebnis im Code-und-Beweis-Modus allein durch die Umstellung der Reasoning-Stufe von medium auf xhigh von 2 auf 27. Bei dieser Art von Aufgabe ist der Grenznutzen des Denkbudgets noch längst nicht ausgeschöpft.

Schwierig ist nicht der einzelne Beweis

Die Spitzenzeile liefert noch eine weitere Zahl. GPT-5.5 (xhigh) besteht im Code-und-Beweis-Modus 87,3 Prozent der Einzelspezifikationen, im reinen Beweismodus 85,8 Prozent – doch gemessen am Maßstab „gesamte Instanz vollständig gelöst” bleiben nur 27/43 beziehungsweise 25/43 übrig. Die Einschätzung der Forscher ist eindeutig: Den Beweis jeder einzelnen Spezifikation zu führen ist inzwischen keine große Hürde mehr – schwierig ist es, das gesamte Beweis-Repository konsistent zu halten.

Die Kluft zwischen diesen beiden Zahlen hat handfeste technische Konsequenzen. Eine Erfolgsquote von 87 Prozent pro Spezifikation bedeutet, hochgerechnet auf ein Projekt mit mehreren Dutzend Spezifikationen, dass fast jedes Projekt an ein paar Stellen hängen bleibt. Formale Verifikation kennt aber kein Teilergebnis: Bleibt eine einzige Spezifikation unbewiesen, lässt sich das gesamte Repository nicht bauen, und die bereits korrekt bewiesenen Teile bringen keinerlei Teilpunkte. Das unterscheidet sich grundlegend von einem Projekt, das trotz 87 Prozent bestandener Unit-Tests trotzdem ausgeliefert werden kann.

Ein weiteres Detail betrifft die Zusammensetzung des Beweiscodes. In den vollständig gelösten Durchläufen machen Hilfslemmata im Median 73,6 Prozent des Beweiscodes aus. Anders gesagt: Drei Viertel dessen, was die Agenten schreiben, ist Gerüst, das provisorisch zur Stützung des Hauptbeweises errichtet wird. Dieser Anteil deutet darauf hin, dass aktuelle Modelle eher in die Breite gehen und mit einem Berg von Lemmata durchbrechen, statt eine schlanke Beweisstruktur zu finden.

Den Algorithmus selbst wählen: fünfmal geholfen, siebzehnmal geschadet

Der Code-und-Beweis-Modus gibt dem Agenten einen Freiheitsgrad: Da die Implementierung selbst geschrieben werden darf, kann er sich auch für einen leichter zu beweisenden Algorithmus entscheiden. Die Forscher haben den Nettoeffekt dieser Freiheit ausgewertet: In paarweisen Vergleichen führte der Algorithmuswechsel in 5 Fällen zum Erfolg, in 17 Fällen dagegen zum Scheitern.

Dieses Verhältnis von 5 zu 17 spricht Bände. Theoretisch sollte die Freiheit, die Implementierung selbst zu wählen, nur nützen – im schlimmsten Fall kopiert man einfach die Referenzimplementierung. In der Praxis wählt das Modell jedoch häufig eine vermeintlich clevere Variante, die sich als deutlich schwerer beweisbar erweist, und verheddert sich dann innerhalb der 90 Minuten. Code schreiben zu können und zu wissen, welcher Code sich leicht beweisen lässt, sind zwei verschiedene Fähigkeiten – aktuelle Agenten beherrschen bislang nur die erste.

Die Rangliste hält noch eine Randnotiz bereit: Von den 43 Instanzen wurden 10 in keiner Konfiguration und in keinem der beiden Modi jemals gelöst. Diese Gruppe markiert die aktuelle harte Obergrenze der Methode und ist zugleich der Punkt, auf den sich die nächste Forschungsrunde am dringendsten konzentrieren sollte.

Für alle, die KI-Programmierwerkzeuge bauen, liegt der Referenzwert von Vero nicht im Ranking, sondern darin, dass es „Konsistenz auf Repository-Ebene” – bislang nur intuitiv erfahrbar – erstmals in eine messbare Kennzahl übersetzt. Benchmarks vom Typ SWE-bench prüfen, ob ein einzelner Bug korrekt behoben werden kann, Vero dagegen prüft, ob man den vollständigen Beschränkungen eines Engineering-Projekts standhält – beides bewegt sich nicht auf demselben Schwierigkeitsniveau.

Quellen: öffentlicher Blog des RDI Lab der UC Berkeley, CocoLoop; Benchmark-Umfang, vollständig gelöste Instanzen in beiden Modi, Erfolgsquote pro Spezifikation, Anteil der Hilfslemmata und paarweise Vergleichsstatistik wurden anhand des öffentlichen Berichts geprüft.