Ajudas Automáticas em Dafny Usando IA

Dafny é uma linguagem usada pra verificar código. Ela ajuda a provar que o código se comporta como devia. Grande parte desse trabalho de Verificação é feita automaticamente usando um resolvedor SMT, mas às vezes o resolvedor precisa de uma ajudinha extra. É aí que entram as declarações auxiliares. Elas são afirmações que guiam o resolvedor a provar certas propriedades do código. Porém, criar essas declarações pode ser complicado e demorado pros desenvolvedores.

Neste artigo, vamos falar sobre uma nova ferramenta que usa modelos de linguagem grandes (LLMs) pra gerar automaticamente essas declarações auxiliares. O objetivo é facilitar e tornar o processo de verificação mais eficiente pros desenvolvedores.

#O Problema

Quando usam o Dafny, os programadores muitas vezes esbarram em um muro quando o resolvedor não consegue verificar certas partes do código. Isso pode acontecer porque o raciocínio necessário é muito complexo pro resolvedor lidar. Nesses casos, os desenvolvedores precisam fornecer informações adicionais na forma de declarações auxiliares. Essas declarações ajudam a decompor provas complicadas em passos mais gerenciáveis.

No entanto, encontrar a declaração auxiliar certa pode ser frustrante. Os desenvolvedores podem passar muito tempo adivinhando qual declaração pode ajudar a superar o obstáculo de verificação. A situação piora quando mudanças no código ou na ferramenta de verificação fazem provas que antes funcionavam falharem. Às vezes, os desenvolvedores têm que adicionar rapidamente declarações em partes do código com as quais não estão familiarizados pra evitar atrasos no lançamento do software.

#A Solução

Pra resolver esse problema, propomos uma ferramenta que usa LLMs pra gerar declarações auxiliares automaticamente. LLMs são modelos avançados de inteligência artificial que entendem e geram texto parecido com o humano. Eles já mostraram grande sucesso em tarefas como gerar e corrigir código, e agora queremos aplicar suas capacidades na geração de declarações auxiliares no Dafny.

Nossa ferramenta aproveita estratégias específicas pra melhorar o desempenho dos LLMs na geração dessas declarações. Primeiro, analisamos as mensagens de erro fornecidas pelo verificador do Dafny. Fazendo isso, conseguimos descobrir onde a declaração faltante deve ser colocada. Em segundo lugar, fornecemos aos LLMs exemplos de declarações semelhantes do mesmo conjunto de código. Isso dá contexto pros LLMs, ajudando-os a entender que tipo de declaração gerar.

#Como a Ferramenta Funciona

A ferramenta começa pegando um conjunto de código em Dafny e o nome de um lema alvo (uma afirmação em Dafny que precisa ser verificada). O objetivo aqui é inserir uma declaração em determinado lugar pra que o lema seja verificado com sucesso.

A ferramenta segue esses passos:

1. Analisando Mensagens de Erro: O verificador do Dafny produz mensagens de erro quando algo dá errado. Nossa ferramenta pega essas mensagens e as usa pra localizar onde a declaração faltante deve ser colocada no código.

2. Encontrando Declarações de Exemplo: A ferramenta então vasculha o código pra coletar um conjunto de declarações relevantes que poderiam servir como exemplos. Em vez de usar toda e qualquer declaração, que poderia confundir o LLM, escolhemos um número pequeno com base em quão semelhantes elas são ao lema atual. Isso é feito usando uma nova métrica de similaridade que desenvolvemos.

3. Gerando Declarações Auxiliares: Com o espaço reservado pra declaração posicionado corretamente no código, e as declarações de exemplo relevantes em mãos, o LLM pode gerar a declaração auxiliar necessária. Ele vai substituir o espaço reservado pela declaração gerada e depois recheckar com o verificador do Dafny.

4. Iterando: Se o lema ainda falhar na verificação após a primeira tentativa, a ferramenta pode pedir ao LLM pra gerar mais declarações até um número definido de tentativas.

#Principais Insights

Da nossa pesquisa, fizemos duas observações chave que guiam como a ferramenta funciona:

1. Localização Importa: LLMs frequentemente têm dificuldades pra encontrar o lugar certo pra declaração faltante baseando-se apenas no código. Porém, analisando a mensagem de erro do Dafny, nossa ferramenta consegue localizar com precisão onde a declaração deve ser colocada.

2. Similaridade é Útil: Declarações que são semelhantes entre si costumam ser úteis na hora de guiar o processo de geração. Ao selecionar declarações de exemplo que são estruturalmente similares ao lema alvo, permitimos que o LLM se baseie em conhecimentos existentes, aumentando as chances de gerar declarações corretas.

#Avaliação

Pra testar a eficácia da nossa ferramenta, usamos conjuntos reais de código do Dafny. Extraímos dados de vários projetos, que forneceram um rico conjunto de exemplos pra trabalhar. Nossa avaliação examina se o uso de espaços reservados pra declarações e a seleção de exemplos com base na similaridade melhora a taxa de sucesso dos LLMs na geração de declarações auxiliares válidas.

Durante nossa avaliação, rodamos diferentes configurações da ferramenta sob várias condições. Comparamos os resultados com base em quantos lemas foram verificados com sucesso após a geração das declarações.

#Resultados

Os resultados foram encorajadores. Ao usar nossas técnicas propostas, vimos um aumento significativo no número de declarações auxiliares que os LLMs conseguiram gerar com sucesso. A ferramenta conseguiu gerar declarações auxiliares válidas em cerca de 52% dos casos testados, provando que com as estratégias certas, os LLMs podem ajudar efetivamente os programadores no processo de verificação.

#Benefícios de Usar a Ferramenta

1. Eficiência: Com a ajuda dessa ferramenta, os desenvolvedores podem economizar muito tempo. Em vez de passar horas adivinhando qual declaração pode funcionar, eles podem contar com a ferramenta pra gerar declarações pra eles.

2. Menos Frustração: A geração automática de declarações auxiliares também reduz a frustração que os desenvolvedores muitas vezes sentem ao lidar com falhas de verificação complexas.

3. Melhoria na Qualidade do Código: Ao incentivar o uso de declarações adequadas, a ferramenta pode ajudar a levar a provas mais limpas e eficientes. Isso é benéfico não só pra projetos individuais, mas também pra comunidade de desenvolvedores mais ampla.

4. Recurso de Aprendizado: Pra desenvolvedores menos experientes, olhar pra declarações de exemplo pode servir como um recurso educacional. Eles podem aprender a formular declarações melhor observando exemplos bem-sucedidos.

#Conclusão

Dafny é uma ferramenta poderosa pra verificação de código, mas vem com seus desafios. A necessidade de declarações auxiliares pode complicar o processo de verificação, levando a frustrações e perda de tempo pros desenvolvedores. Nossa ferramenta, que usa LLMs pra gerar automaticamente essas declarações, apresenta uma solução eficaz.

Analisando mensagens de erro e aproveitando declarações existentes, a ferramenta melhora a precisão e a eficiência do processo de verificação. Nossa avaliação demonstra o sucesso da ferramenta em gerar declarações auxiliares válidas, tornando-a uma adição valiosa ao ecossistema do Dafny.

O futuro da verificação de programas parece promissor com a integração de tecnologias de IA. À medida que os LLMs continuam a evoluir, esperamos que nossa ferramenta se torne ainda mais eficaz, abrindo caminho pra mais avanços na verificação de código e garantia de qualidade. Este trabalho abre as portas pra explorar mais aplicações de LLMs em várias linguagens de programação e frameworks, aumentando a produtividade dos desenvolvedores e a confiabilidade do software.