🤖 AI

Automated Proof Generation for Rust Code via Self-Evolution

O artigo apresenta o SAFE, um framework que supera a escassez de dados de provas formais para Rust ao estabelecer um ciclo de autoevolução que sintetiza e depura automaticamente provas, permitindo que modelos de linguagem open source atinjam uma precisão de 52,52% em benchmarks especializados, superando significativamente o desempenho do GPT-4o.

Autores originais: Tianyu Chen, Shuai Lu, Shan Lu, Yeyun Gong, Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Hao Yu, Nan Duan, Peng Cheng, Fan Yang, Shuvendu K Lahiri, Tao Xie, Lidong Zhou

Publicado 2026-02-17

📖 4 min de leitura☕ Leitura rápida

CC BY 4.0

Autores originais: Tianyu Chen, Shuai Lu, Shan Lu, Yeyun Gong, Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Hao Yu, Nan Duan, Peng Cheng, Fan Yang, Shuvendu K Lahiri, Tao Xie, Lidong Zhou

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você está construindo casas (código de computador) e quer ter certeza absoluta de que elas não vão desmoronar, mesmo que um furacão bata nelas. Para garantir isso, você precisa de um engenheiro de segurança (verificação formal) que escreva um manual de instruções detalhado (provas) explicando por que a casa é segura.

O problema é que escrever esses manuais é extremamente difícil, chato e requer especialistas raros. É como tentar encontrar um manual de instruções escrito à mão para cada tipo de casa que existe: quase não existem.

Aqui entra o SAFE, o novo método apresentado neste artigo. Pense no SAFE como um aprendiz de gênio que aprende sozinho, erra muito, mas nunca desiste.

Aqui está como ele funciona, passo a passo, usando analogias simples:

1. O Problema: A Escassez de Manuais

Antes, os computadores (Inteligências Artificiais) tentavam aprender a escrever esses manuais de segurança apenas lendo o que humanos já tinham escrito. Mas como há muito poucos manuais de segurança para a linguagem de programação Rust (uma linguagem moderna e segura), as IAs ficavam "cegas" e cometiam muitos erros.

2. A Solução: O Ciclo de Auto-Evolução (SAFE)

O SAFE resolve isso criando seu próprio "curriculo" de aprendizado. Ele não espera que alguém lhe dê os livros; ele os escreve, lê, erra, corrige e escreve de novo.

Passo 1: Traduzindo para a "Linguagem da Segurança"

Primeiro, o SAFE pega milhares de pequenos programas comuns (escritos em Python ou Rust básico) e pede a uma IA superpoderosa (GPT-4o) para traduzi-los para a "Linguagem da Segurança" (Verus). É como pegar um esboço de casa e transformá-lo em um projeto arquitetônico oficial que o engenheiro consegue ler.

Passo 2: Criando as Regras do Jogo (Especificações)

Agora que temos os programas, precisamos dizer ao engenheiro o que ele deve verificar. O SAFE começa pedindo ao GPT-4o para inventar regras (ex: "esta função nunca deve dividir por zero").

O Truque: O SAFE não aceita qualquer regra. Ele usa um "juiz automático" (o compilador Verus) para testar se a regra faz sentido. Se a regra for muito vaga ou errada, ele descarta. Se for boa, ele guarda.
A Evolução: Depois de gerar milhares de regras, o SAFE treina um modelo menor e mais rápido com essas regras boas. Na próxima rodada, esse modelo treinado gera regras ainda melhores. É como um aluno que, depois de estudar com um professor, vira professor e ensina a próxima turma, que fica ainda mais inteligente.

Passo 3: Escrevendo os Manuais (Provas)

Com os programas e as regras em mãos, o SAFE tenta escrever o manual de segurança (a prova).

O Desafio: Escrever a prova é difícil. No começo, o modelo erra muito.
O Poder do Juiz: Aqui está a mágica. O Verus (o engenheiro) é rápido e implacável. Ele diz: "Isso está errado" e mostra o erro.
O Aprendizado: O SAFE pega esses erros e cria um novo tipo de lição: "Aqui estava a prova errada, aqui está a mensagem de erro do juiz, e aqui está a prova corrigida". Ele usa isso para ensinar o modelo a se auto-corrigir.

3. O Resultado: Um Mestre da Segurança

O resultado final é um modelo de IA que, mesmo começando sem saber nada sobre segurança formal, aprendeu a escrever manuais de segurança para o Rust com uma precisão impressionante.

Comparação: Se o GPT-4o (o "gênio" original) acertava apenas 14% dos testes, o modelo treinado pelo SAFE acertou 52%.
O Superpoder: Quando o SAFE usa sua habilidade de "se auto-corrigir" (tentar, errar, ler o erro, tentar de novo), a precisão sobe para 79%.

Resumo da Ópera

Imagine um aluno que, em vez de apenas ler a resposta do professor, cria seus próprios exercícios, tenta resolvê-los, o professor corrige, e o aluno usa essa correção para aprender a não errar mais.

O SAFE fez exatamente isso:

Criou seus próprios problemas (programas e regras).
Usou um juiz automático para filtrar o que era bom.
Aprendeu com seus próprios erros para se tornar um especialista em provar que o código é seguro.

Isso é revolucionário porque, pela primeira vez, conseguimos automatizar a criação de segurança para códigos complexos sem depender de milhares de especialistas humanos escrevendo manuais à mão. É como ter uma fábrica que produz seus próprios engenheiros de segurança cada vez mais inteligentes.

Título: Geração Automatizada de Provas para Código Rust via Auto-Evolução (SAFE)

1. O Problema

A garantia de correção em geração de código é um desafio crítico. A verificação formal oferece uma garantia definitiva de que um programa satisfaz propriedades desejadas sob todas as entradas possíveis, mas sua adoção é limitada pela necessidade de esforço humano massivo para construir provas.

O principal obstáculo para automatizar esse processo com Grandes Modelos de Linguagem (LLMs) é a escassez severa de dados. Diferente de códigos de programação comuns, existem muito poucas provas formais disponíveis para treinamento. Especificamente para Rust e sua ferramenta de verificação de ponta, Verus:

Existem menos de 500 arquivos Rust verificados no GitHub.
A criação de especificações formais (pré e pós-condições) e provas (invariantes de loop, lemas) exige expertise especializada e é extremamente demorada.
Abordagens anteriores baseadas em prompting (aprendizado em contexto) têm capacidade de generalização limitada e dependem de engenharia de prompts complexa.

2. Metodologia: O Framework SAFE

O artigo propõe o SAFE (Self-evolving Automated prooF gEneration), um framework que supera a falta de dados humanos através de um ciclo de auto-evolução, onde a síntese de dados e o fine-tuning (ajuste fino) colaboram para aprimorar o modelo. O processo divide-se em três etapas principais:

Etapa 1: Geração de Código Compatível com Verus

Como o Verus não suporta todas as funcionalidades do Rust (ex: certos iteradores, HashMap), o framework utiliza o GPT-4o para "traduzir" milhares de programas pequenos (de datasets como MBPP e CodeNet) para uma sintaxe Rust compatível com o Verus.
Programas que não compilam no Verus são descartados.

Etapa 2: Síntese Auto-Evolucionista de Especificações

O objetivo é gerar pré-condições (requires) e pós-condições (ensures) para as funções Rust.
Ciclo de Evolução:
1. O GPT-4o gera especificações iniciais baseadas em docstrings.
2. Um modelo LLM de código aberto é ajustado (fine-tuned) nessas especificações.
3. O modelo ajustado gera novas especificações de melhor qualidade.
Filtragem de Qualidade: Para evitar especificações incorretas ou triviais, o SAFE utiliza uma métrica quantitativa baseada em testes:
- Corretude: A especificação aceita implementações corretas (baseado em casos de teste originais).
- Completude: A especificidade rejeita implementações incorretas (baseado em casos de teste mutados).
- Apenas especificações com pontuação alta em ambas as métricas são mantidas para o próximo ciclo.

Etapa 3: Síntese Auto-Evolucionista de Provas e Auto-Depuração

O modelo tenta gerar as anotações de prova (invariantes de loop, blocos de prova) para que o Verus verifique o código.
O Papel do Verificador: O compilador Verus atua como um "juiz" autoritário, rejeitando instantaneamente qualquer prova incorreta sem necessidade de anotação humana.
Mecanismo de Auto-Depuração (Self-Debugging): Esta é uma contribuição chave. O framework não descarta as provas incorretas geradas. Em vez disso, cria um conjunto de dados de treinamento composto por:
- Uma prova incorreta ( $P_{\times}$ ).
- A mensagem de erro gerada pelo Verus.
- A prova correta final ( $P_{\checkmark}$ ).
O modelo é ajustado para aprender a corrigir suas próprias provas com base nas mensagens de erro, transformando falhas iniciais em dados de treinamento valiosos.

3. Contribuições Chave

Solução para Escassez de Dados: O SAFE demonstra que é possível criar um dataset massivo de provas formais sintéticas para uma linguagem específica (Rust/Verus) sem depender de dados humanos existentes, superando a barreira de entrada para verificação formal automatizada.
Ciclo de Auto-Evolução: Integra a síntese de especificações e provas em um ciclo iterativo onde o modelo melhora a si mesmo, usando o verificador formal como critério de seleção de dados.
Mecanismo de Auto-Depuração: Aproveita o grande volume de tentativas falhas (provas incorretas) para treinar o modelo a diagnosticar e reparar erros, uma capacidade que modelos puramente generativos não possuem.
Dataset Sintético: Produziu o maior dataset sintético para Verus até a data, contendo 19.017 especificações formais e 9.706 funções Rust verificadas.

4. Resultados Experimentais

Os experimentos foram conduzidos utilizando o modelo DeepSeekCoder (33B) como base, comparado com o GPT-4o e modelos raw (sem ajuste fino).

Benchmarks:
- VerusBench: 139 tarefas escritas por humanos com especificações humanas.
- CodeNet-Test: 1.435 tarefas sintéticas derivadas de programação competitiva.
Desempenho:
- No VerusBench, o modelo SAFE alcançou 43,17% de precisão na geração direta (Accuracy@1), superando o GPT-4o (11,51%) em mais de 3x.
- Com o recurso de auto-depuração (SAFE+), a precisão no VerusBench saltou para 52,52% (Accuracy@2), comparado a 14,39% do GPT-4o.
- No CodeNet-Test, o SAFE alcançou 43,83% (Accuracy@1) vs. 0,28% do GPT-4o.
Eficiência: O modelo ajustado gera provas significativamente mais rápido que o GPT-4o e não requer prompts complexos durante a inferência.

5. Significado e Impacto

O trabalho do SAFE representa um avanço significativo na interseção entre Inteligência Artificial e Verificação Formal.

Democratização da Verificação Formal: Permite que modelos de código aberto, que inicialmente não conhecem ferramentas de verificação como o Verus, aprendam a gerar provas formais complexas.
Escalabilidade: Demonstra que a escassez de dados em domínios especializados (como provas formais) pode ser mitigada através de síntese automática guiada por verificadores formais, em vez de depender de anotação humana massiva.
Segurança de Software: Ao automatizar a geração de provas para Rust (uma linguagem focada em segurança de memória), o framework contribui diretamente para a criação de software mais confiável e livre de bugs críticos, reduzindo a barreira de entrada para engenharia de software de alta confiança.

Em resumo, o SAFE transforma o problema da falta de dados de prova em uma oportunidade de aprendizado iterativo, onde o verificador formal atua como o professor e o modelo de linguagem como o aluno que evolui através de tentativa, erro e correção automática.