Resumo Técnico: Redução dos Custos de Síntese de Provas em Sistemas Rust por Escalonamento de um Conjunto de Dados Inicial

1. Declaração do Problema

A correção do código gerado por Modelos de Linguagem de Grande Escala (LLMs) permanece um desafio significativo, particularmente para software de sistema crítico em termos de segurança e confiabilidade. Embora os LLMs tenham demonstrado capacidades robustas de geração de código, eles frequentemente produzem código sintaticamente correto que viola propriedades de segurança, confiabilidade ou funcionais. Um remédio potencial é exigir que os LLMs gerem provas de correção formal juntamente com o código.

No entanto, gerar provas formais para software de sistema (especificamente usando Verus, uma ferramenta de verificação de última geração para Rust) requer capacidades de raciocínio significativamente superiores às da geração de código padrão. Além disso, o campo sofre de escassez severa de dados. Sistemas Rust verificados existentes são poucos, e os conjuntos de dados disponíveis (por exemplo, SAFE, AlphaVerus) são limitados em escala e diversidade. Trabalhos anteriores demonstraram que apenas modelos comerciais caros e de grande escala (por exemplo, Claude Sonnet 4.5) possuem a capacidade de gerar tais provas efetivamente, enquanto modelos menores ou mais baratos falham. O problema central abordado por este artigo é: Como podemos gerar provas de código efetivamente a um baixo custo sintetizando dados de treinamento de alta qualidade e alto volume para LLMs menores?

2. Metodologia: O Pipeline VeruSyn

Os autores propõem o VeruSyn, um pipeline de síntese de dados projetado para criar o maior conjunto de programas verificados com Verus até a data. O pipeline aborda três limitações específicas de esforços de síntese anteriores: escala limitada, cobertura de recursos estreita e baixa complexidade de raciocínio. O VeruSyn integra três abordagens de síntese distintas de maneira iterativa e coordenada:

2.1 Escalonamento do Número de Programas (Auto-Síntese)

Diferentemente de métodos anteriores que dependem da tradução de suites de benchmark existentes (o que limita o tamanho do conjunto de dados pela fonte), o VeruSyn emprega uma estratégia de auto-síntese.

• Processo: Um LLM é ajustado para gerar diretamente, do zero, programas Rust e suas especificações e provas Verus correspondentes, sem depender de programas fonte pré-existentes.
• Iteração: O processo começa com um modelo base ajustado no conjunto de dados SAFE. Este modelo gera programas iniciais. À medida que a síntese prossegue, o modelo é iterativamente ajustado nos dados recém-gerados, verificados e depurados para melhorar suas capacidades de geração.
• Terminação: A síntese para quando a proporção de programas duplicados em um lote atinge 95%, garantindo diversidade.

2.2 Escalonamento da Cobertura de Recursos (Síntese Baseada em Tutoriais)

Para superar o viés de conjuntos de dados anteriores em direção a invariantes de loop simples, o VeruSyn utiliza o Tutorial Verus como uma fonte de conhecimento estruturada.

• Processo: Especialistas criam manualmente "programas iniciais" que cobrem pontos-chave de conhecimento de cada capítulo do tutorial Verus.
• Síntese: O modelo de geração de provas é instruído a gerar milhares de novos programas para cada inicial, explicitamente guiado pelo capítulo correspondente do tutorial.
• Objetivo: Isso garante uma cobertura sistemática de recursos Verus diversos (por exemplo, quantificadores, aritmética não linear, vetores de bits) que frequentemente faltam em benchmarks algorítmicos, mas são essenciais para a verificação de sistemas do mundo real.

2.3 Escalonamento da Complexidade de Raciocínio (Síntese de Trajetórias de Agente)

Para lidar com provas de sistemas complexos e do mundo real que exigem longas cadeias de raciocínio, o VeruSyn incorpora dados de Cadeia de Pensamento (CoT) derivados de trajetórias de agente.

• Processo: Um agente de codificação de última geração (impulsionado pelo Claude Sonnet 4.5) é encarregado de escrever provas para um pequeno conjunto de problemas de verificação de sistemas do mundo real (do VeruSAGE-Bench).
• Coleta de Dados: O log completo do raciocínio do agente, ações (leitura de arquivos, invocação do Verus, análise de erros, edição de provas) e a trajetória final bem-sucedida são coletados.
• Integração: Essas trajetórias são convertidas em dados de treinamento, fornecendo ao modelo exemplos de como depurar e raciocinar através de erros de verificação complexos em múltiplas etapas.

2.4 Anti-Trapaça e Filtragem

Um componente crítico do pipeline é um processo rigoroso de filtragem para prevenir "trapaça" (por exemplo, modificar especificações para tornar as provas trivialmente verdadeiras, adicionar loops infinitos para pular a verificação ou usar declarações assume).

• Mecanismos: O pipeline usa analisadores sintáticos tree-sitter para verificar a compatibilidade das especificações, detecta palavras-chave proibidas (como assume) e impõe cláusulas decreases para terminação.
• Depuração: Programas não verificados são enviados de volta ao modelo com relatórios de erro para depuração; apenas pares verificados com sucesso são retidos.

3. Principais Contribuições

• Escala do Conjunto de Dados: A síntese de 6,9 milhões de programas Rust verificados com Verus, cada um com uma especificação formal e uma prova. Este é o maior conjunto de dados de seu tipo.
• Diversidade de Recursos: O conjunto de dados cobre 12 a 15 pontos de conhecimento Verus distintos (de 20 pontos-chave), superando significativamente conjuntos de dados anteriores (SAFE e AlphaVerus) que cobriam apenas 4–5 pontos de forma significativa.
• Integração CoT: A inclusão de 4.557 instâncias longas de CoT derivadas de trajetórias de agente em tarefas de sistemas do mundo real.
• Desempenho do Modelo: Um modelo Qwen2.5-Coder-32B-Instruct ajustado que alcança capacidades competitivas de síntese de provas a uma fração do custo dos modelos comerciais.

4. Resultados de Avaliação

Os autores avaliaram o modelo ajustado com VeruSyn em dois benchmarks: VerusBench (150 tarefas algorítmicas) e VeruSAGE-Bench (849 tarefas extraídas de sistemas Rust do mundo real, com 289 excluídas para evitar vazamento de dados).

4.1 Precisão

• Provas de Sistema (VeruSAGE-Bench): Sem depuração, o modelo VeruSyn alcançou uma taxa de sucesso de 39% (Accuracy@100), superando significativamente o modelo Qwen bruto (10%), modelos ajustados com SAFE (6%), modelos ajustados com AlphaVerus (11%) e o comercial o4-mini (15%).
• Com Depuração: Após 5 rodadas de depuração, o modelo VeruSyn atingiu 49% de precisão, comparado a 54% para o caro Claude Sonnet 4.5.
• Provas Algorítmicas (VerusBench): O modelo alcançou 75% de precisão (sem depuração), superando ligeiramente o Claude Sonnet 4.5 (72%).

4.2 Eficiência de Custos

O artigo destaca uma redução dramática no custo:

• Custo por Tarefa: O modelo VeruSyn custa aproximadamente $0,17 por tarefa (sem depuração) e $0,61 (com depuração).
• Comparação: Isso é cerca de 47 vezes mais barato que o Claude Sonnet 4.5 ($8,04 sem depuração) e significativamente mais barato que o o4-mini ($3,39).
• Compromisso: O modelo VeruSyn com 5 rodadas de depuração ($0,61) alcança maior precisão (49%) que o Claude Sonnet 4.5 sem depuração (46%), representando uma redução de custo de 13 vezes para desempenho superior.

4.3 Estudos de Ablação

• Componentes de Dados: Remover tanto os dados de auto-síntese/tutorial (Parte 1) quanto os dados CoT (Parte 2) degradou significativamente o desempenho em tarefas de sistemas do mundo real. A Parte 1 foi crucial para tarefas algorítmicas, enquanto a Parte 2 foi essencial para provas de sistemas complexos.
• Modelo Professor: O uso de um modelo professor mais forte (Claude Sonnet 4.5) para geração de CoT resultou em desempenho a jusante significativamente melhor (39% vs. 15% ao usar o o4-mini como professor).

5. Significado e Alegações

O artigo alega que o VeruSyn demonstra que dados sintéticos de alta qualidade e grande escala podem preencher a lacuna entre modelos de código aberto pequenos e econômicos e modelos comerciais caros no domínio da verificação formal.

• Compromisso Custo-Prova: O trabalho estabelece um novo marco para eficiência de custos, mostrando que um modelo de 32B parâmetros ajustado em dados sintetizados pode superar ou igualar modelos comerciais 4,5 vezes maiores a uma fração do custo de inferência.
• Escalabilidade: A metodologia prova que a auto-síntese e a síntese guiada por tutoriais podem escalar além das limitações das suites de benchmark existentes, criando um suprimento "ilimitado" de dados de treinamento para ferramentas de verificação formal.
• Generalização: Os resultados sugerem que os dados sintetizados ensinam efetivamente aos modelos não apenas a sintaxe, mas os padrões complexos de raciocínio necessários para verificar software de sistema do mundo real, uma capacidade anteriormente considerada exclusiva dos maiores modelos.

Os autores concluem que seu conjunto de dados de treinamento está disponível no HuggingFace, visando reduzir a barreira de entrada para a verificação formal no desenvolvimento de software de sistema.