Un articolo pubblicato su arXiv il 5 novembre esamina cosa significhi «verificato» nel caso del codice generato da modelli linguistici di grandi dimensioni. Distingue tre controlli: se un verificatore accetta il codice, se la prova è collegata a una specifica e se tale specifica rispecchia il requisito originario.
In un test, gli autori riportano un tasso di accettazione del 99,1% da parte del verificatore su HumanEval, ma solo l’1,9% dei campioni aveva un certificato collegato a un predicato o a una funzione definiti dalla specifica. In una pipeline Rust separata, progettata per garantire questo collegamento, l’11,48% dei campioni MBPP-Rust verificati strutturalmente e il 14,82% dei campioni di una porzione di VeriContest non hanno comunque superato i test nascosti.
Perché conta
Per i team che usano la verifica formale per valutare il codice generato, i risultati mostrano che la sola accettazione da parte del verificatore potrebbe non dimostrare né un legame significativo con i requisiti né la correttezza rispetto a test nascosti.
