Um artigo publicado no arXiv em 5 de novembro examina o que significa dizer que um código gerado por grandes modelos de linguagem foi “verificado”. O estudo distingue três etapas: se um verificador aceita o código, se a prova está vinculada a uma especificação e se essa especificação reflete o requisito original.
Em um teste, os autores relatam que o verificador aceitou 99,1% dos códigos no HumanEval, mas apenas 1,9% das amostras tinham um certificado vinculado a um predicado ou função definido pela especificação. Em um pipeline separado em Rust, desenvolvido para assegurar esse vínculo, 11,48% das amostras do MBPP-Rust verificadas estruturalmente e 14,82% das de um recorte do VeriContest ainda falharam nos testes ocultos.
Por que importa
Para equipes que usam verificação de provas para avaliar código gerado, os resultados mostram que a aceitação pelo verificador, por si só, pode não comprovar nem uma ligação significativa com os requisitos nem a correção nos testes ocultos.
