From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification

Resumo Técnico: Do Linguagem Natural ao Código Verificado

Título Original: From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification

1. O Problema

O desenvolvimento de software de alta garantia (high-assurance) exige verificação formal, um processo matemático que garante que um programa satisfaça rigorosamente suas especificações. No entanto, este processo enfrenta dois grandes obstáculos:

• Carga de Especificação: Escrever especificações formais (como invariantes de loop e pré/pós-condições) é extremamente trabalhoso, muitas vezes exigindo mais esforço do que escrever o próprio código executável.
• Limitações dos LLMs: Embora os Grandes Modelos de Linguagem (LLMs) sejam excelentes em gerar código a partir de linguagem natural, eles frequentemente sofrem de "alucinações", gerando código que parece correto sintaticamente, mas é semanticamente incorreto ou logicamente falho. Além disso, há uma escassez de dados de treinamento para linguagens de verificação como o Dafny.

2. Metodologia

Os autores propõem uma abordagem de "Verificação no Ciclo" (Verification-in-the-Loop) para transformar requisitos informais em código provadamente correto.

• Dataset NL2VC-60: Criaram um novo benchmark contendo 60 problemas algorítmicos complexos (derivados do UVa Online Judge). Diferente de datasets existentes, estes problemas foram "generalizados" para remover detalhes irrelevantes de competições e focados em requisitos funcionais puros. Cada problema inclui uma descrição em linguagem natural, uma assinatura de método formal e casos de teste.
• Estratégias de Prompting em Camadas:
  1. Contextless Prompting (RQ1): Apenas a descrição em linguagem natural (estabelece uma linha de base).
  2. Signature Prompting (RQ2): Fornece a assinatura do método (parâmetros e tipos) para servir como âncora estrutural.
  3. Self-Healing Prompting (RQ3): Um processo iterativo onde as mensagens de erro do verificador Dafny são enviadas de volta ao LLM para que ele tente reparar o código e as especificações automaticamente.
• Validação Dupla:
  • Camada Formal: Uso do verificador Dafny e do solver SMT (Z3) para garantir a consistência lógica.
  • Camada Funcional: Integração com a plataforma uDebug para testar o código contra casos de borda reais, evitando a "verificação vacante" (quando o modelo cria uma especificação tão fraca que o verificador a aprova, mas o código não resolve o problema real).

3. Principais Contribuições

• NL2VC-60: O primeiro dataset de grande escala que mapeia requisitos complexos de linguagem natural para código Dafny verificado.
• Taxonomia de Erros: A primeira categorização sistemática de erros de compilação e verificação específicos para Dafny em LLMs (erros de sintaxe, erros semânticos/de tipo e falhas de verificação lógica).
• Framework de Avaliação: Um pipeline robusto que combina verificação formal com testes funcionais de comunidade (uDebug).

4. Resultados Principais

Os experimentos avaliaram sete modelos de pesos abertos (open-weight), com destaque para:

• O Gargalo Estrutural: Quase todos os modelos falharam quase totalmente (0% de sucesso) no Contextless Prompting, provando que os LLMs têm dificuldade em inferir a estrutura formal necessária apenas com texto descritivo.
• O Poder das Assinaturas: O uso de assinaturas de método (RQ2) causou uma virada dramática. O modelo GPT-OSS-120B saltou de 0% para 63,64% de sucesso. O Qwen 3.5-9B (um modelo menor) atingiu 72,73%, superando modelos muito maiores.
• Auto-correção (Self-Healing): O processo de cura automática foi altamente eficaz. O modelo Gemma 4-31B demonstrou uma resiliência excepcional, alcançando uma taxa de sucesso de 90,91% ao utilizar o feedback do verificador.
• Desempenho por Modelo: O Gemma 4-31B emergiu como o modelo mais robusto para o desenvolvimento autônomo em Dafny, independentemente do nível de contexto inicial.

5. Significância

O estudo demonstra que a verificação formal não é mais um domínio exclusivo de especialistas humanos. Ao combinar LLMs com verificadores formais (como o Dafny), é possível criar um fluxo de trabalho onde a IA atua como um "aprendiz" capaz de gerar código de alta confiança. Isso reduz drasticamente o custo de desenvolvimento de software crítico, tornando a engenharia de alta garantia economicamente viável para aplicações gerais, transformando o código de "plausível" em "provadamente correto".