En artikel som publicerades på arXiv den 5 november undersöker vad det innebär att kod som genererats av stora språkmodeller är ”verifierad”. Författarna skiljer mellan tre kontroller: om en verifierare godkänner koden, om beviset är knutet till en specifikation och om specifikationen motsvarar det ursprungliga kravet.
I ett test rapporterar författarna att verifieraren godkände 99,1 % av koden i HumanEval, men att bara 1,9 % av exemplen hade ett certifikat kopplat till ett predikat eller en funktion som definierats i specifikationen. I en separat Rust-pipeline, utformad för att säkerställa den kopplingen, underkändes ändå 11,48 % av de strukturellt verifierade exemplen i MBPP-Rust och 14,82 % i ett urval från VeriContest när de kördes mot dolda tester.
Varför det spelar roll
För team som använder beviskontroll för att bedöma genererad kod visar resultaten att en verifierares godkännande i sig inte nödvändigtvis innebär att koden är meningsfullt kopplad till kraven eller klarar dolda tester.
