Un article publié sur arXiv le 5 novembre examine ce que signifie « vérifié » pour du code généré par de grands modèles de langage. Il distingue trois contrôles : l’acceptation du code par un vérificateur, le lien entre la preuve et une spécification, et la fidélité de cette spécification à l’exigence initiale.
Dans un test, les auteurs font état d’un taux d’acceptation de 99.1% par le vérificateur sur HumanEval, mais seulement 1.9% des échantillons disposaient d’un certificat lié à un prédicat ou à une fonction définis dans la spécification. Dans une chaîne de traitement Rust distincte, conçue pour garantir ce lien, 11.48% des échantillons MBPP-Rust vérifiés structurellement et 14.82% des échantillons d’un sous-ensemble de VeriContest échouaient malgré tout aux tests cachés.
Pourquoi c'est important
Pour les équipes qui s’appuient sur la vérification de preuves afin d’évaluer le code généré, ces résultats montrent que l’acceptation par un vérificateur ne suffit pas nécessairement à établir un lien pertinent avec les exigences, ni à garantir la correction du code face à des tests cachés.
