Een paper die op 5 november op arXiv verscheen, onderzoekt wat ‘geverifieerd’ betekent bij code die door grote taalmodellen wordt gegenereerd. De auteurs onderscheiden drie controles: accepteert een verifier de code, is het bewijs gekoppeld aan een specificatie, en geeft die specificatie de oorspronkelijke vereiste weer?
Bij één test rapporteerden de auteurs een acceptatiepercentage van 99,1% door de verifier op HumanEval, maar had slechts 1,9% van de voorbeelden een certificaat dat gekoppeld was aan een predicaat of functie uit de specificatie. In een afzonderlijke Rust-pipeline die deze koppeling moest waarborgen, slaagde 11,48% van de structureel geverifieerde MBPP-Rust-voorbeelden en 14,82% van een deelverzameling van VeriContest alsnog niet voor verborgen tests.
Waarom het ertoe doet
Voor teams die proofchecking gebruiken om gegenereerde code te beoordelen, laten de resultaten zien dat acceptatie door een verifier op zichzelf niet aantoont dat de code betekenisvol aan de vereisten is gekoppeld of correct is bij verborgen tests.
