Ein am 5. November auf arXiv veröffentlichtes Paper untersucht, was „verifiziert“ bei von großen Sprachmodellen generiertem Code bedeutet. Es unterscheidet drei Prüfungen: ob ein Verifizierer den Code akzeptiert, ob der Beweis an eine Spezifikation gebunden ist und ob diese Spezifikation die ursprüngliche Anforderung widerspiegelt.
In einem Test berichten die Autoren von einer Akzeptanzrate des Verifizierers von 99.1% bei HumanEval. Bei lediglich 1.9% der Beispiele war jedoch ein Zertifikat an ein durch die Spezifikation definiertes Prädikat oder eine Funktion gebunden. In einer separaten Rust-Pipeline, die diese Bindung sicherstellen sollte, scheiterten weiterhin 11.48% der strukturell verifizierten MBPP-Rust-Beispiele und 14.82% einer VeriContest-Teilmenge an versteckten Tests.
Warum es wichtig ist
Für Teams, die generierten Code mithilfe von Beweisprüfungen bewerten, zeigen die Ergebnisse: Die Akzeptanz durch einen Verifizierer allein belegt möglicherweise weder eine aussagekräftige Verbindung zu den Anforderungen noch die Korrektheit bei versteckten Tests.
