Espúrio ou Genuíno? Avaliando Modelos de Linguagem de Grande Escala na Validação de Contraexemplos para Inferência Invariante de Loop

Se um contraexemplo é genuíno ou espúrio influencia fundamentalmente a eficácia e a completude da inferência invariável de loop, que é um componente central da verificação automática de programas. No entanto, determinar de forma confiável a validade de um contraexemplo continua sendo uma tarefa desafiadora. Neste artigo, apresentamos uma avaliação sistemática de modelos de linguagem de grande escala (LLMs) sobre esse problema. Construímos um benchmark de estados de programa que servem como contraexemplos, categorizados em três tipos representativos: (i) pré-estados de contraexemplos indutivos derivados de invariantes propostos pelos LLMs e (ii–iii) estados de limite derivados de invariantes indutivos corretos, onde os estados em si violam (ii) ou satisfazem (iii) a pré-condição do programa. Rótulos de verdade fundamental são estabelecidos usando um verificador de programa de última geração. Avaliamos múltiplos LLMs sob diversas estratégias de solicitação. Nossos resultados mostram que os LLMs apresentam bom desempenho nos dois primeiros tipos de contraexemplos no benchmark, mas um desempenho ruim no terceiro. Além disso, os LLMs são substancialmente mais precisos na classificação de contraexemplos espúrios do que genuínos. Essas descobertas oferecem orientações valiosas para futuras pesquisas sobre a inferência invariável de loops assistida por LLMs.