Resumo Técnico: Ensino de Semântica de Programas a LLMs por Meio de Rastros de Execução Simbólica

Declaração do Problema

Modelos de Linguagem de Grande Escala (LLMs) demonstram alta proficiência na compreensão de código de alto nível, mas lutam com código C de baixo nível, particularmente no que diz respeito à segurança de memória, aritmética de ponteiros e comportamento indefinido. Embora existam benchmarks existentes para compreensão semântica de código, eles frequentemente atingem saturação ou falham em isolar o raciocínio específico necessário para verificação em C.

Uma lacuna crítica identificada neste trabalho é a assimetria no desempenho dos LLMs: os modelos são geralmente confiáveis ao confirmar que uma propriedade se mantém (por exemplo, "nenhuma overflow ocorre"), mas significativamente mais fracos ao detectar quando uma propriedade é violada. Essa fraqueza é exacerbada pelo comprimento do programa; a precisão na detecção de violações degrada-se drasticamente à medida que o comprimento do código aumenta, frequentemente caindo abaixo de 50% para programas de apenas 100–200 linhas. Além disso, esse déficit não correlaciona-se de forma direta com o tamanho do modelo ou especialização em código, sugerindo que os dados de treinamento e objetivos são mais influentes do que a escala isoladamente.

Metodologia

1. Framework de Avaliação

Os autores construíram um benchmark baseado no SV-COMP 2025 (Competição de Verificação de Software), compreendendo 500 tarefas de verificação em C distribuídas em cinco tipos de propriedades:

• Segurança de Memória
• Ausência de Overflows
• Terminação
• Alcançabilidade
• Ausência de Condições de Corrida de Dados (Data Races)

O conjunto de dados foi curado para ser balanceado (50% de propriedades que se mantêm, 50% violadas) e variado em comprimento (0–400 linhas). A verdade fundamental foi estabelecida por ferramentas de verificação formal. O framework avalia 14 modelos de seis famílias, medindo a precisão de classificação binária (mantém vs. violado) sem exigir geração de testemunhos.

2. Pipeline de Treinamento: Rastros de Execução Simbólica

Para abordar a lacuna na detecção de violações, os autores propõem um pipeline de treinamento utilizando artefatos de verificação formal em vez de código bruto ou relatórios de bugs rotulados.

• Fonte de Dados: O pipeline utiliza o conjunto de dados CodeParrot (14 milhões de arquivos C), filtrado para 1 milhão de arquivos autocontidos.
• Execução Simbólica: O motor Soteria (uma ferramenta de execução simbólica de código aberto para C e Rust) é executado nesses arquivos. Diferentemente da execução concreta, o Soteria raciocina sobre todas as entradas possíveis simultaneamente, rastreando estados de memória e condições de ramificação.
• Curadoria de Rastros: Os autores filtram a saída para reter apenas rastros de bugs manifestos—casos onde o Soteria prova que uma violação ocorre em todas as entradas viáveis. Isso resultou em aproximadamente 3.208 rastros de alta qualidade.
• Estratégia de Treinamento: Os autores realizam Pré-treinamento Contínuo (CPT) no modelo Qwen3-8B utilizando esses rastros. Eles ablam sistematicamente variáveis, incluindo:
  • Conteúdo do Rastro: Bugs manifestos vs. bugs latentes vs. rastros sem violação.
  • Formato do Rastro: Saída HTML bruta (preservando tags estruturais) vs. texto simples vs. resumos em linguagem natural informalizados.
  • Modo de Inferência: Decodificação padrão vs. modo de "pensamento" Chain-of-Thought (CoT).

Contribuições Principais

1. Framework de Avaliação Abrangente: Um benchmark de 500 tarefas de verificação em C revelando que a detecção de violações é uma capacidade distinta e mais difícil do que a confirmação de propriedades, com desempenho caindo significativamente para programas mais longos.
2. Pipeline de Treinamento Automatizado: Um método escalável e sem anotação para gerar dados de treinamento executando execução simbólica em código de código aberto genérico. O pipeline filtra bugs manifestos para criar um conjunto de dados de alto sinal.
3. Estratégia de Treinamento Sinérgica: A descoberta de que o Pré-treinamento Contínuo (CPT) em rastros de execução simbólica e o raciocínio Chain-of-Thought (CoT) no momento da inferência são individualmente insuficientes, mas superaditivos em combinação.
   • CPT isoladamente melhora a detecção de violações em ~7,3 pontos percentuais.
   • CoT isoladamente não fornece ganho (e pode degradar o desempenho).
   • CPT + CoT produz uma melhoria de 17,9 pontos percentuais na detecção de violações.
4. Semântica vs. Volume: Evidências de que a melhoria decorre da informação semântica nos rastros (a lógica de por que um bug ocorre) em vez de simplesmente aumentar a exposição ao código. O treinamento nos arquivos fonte C subjacentes sem rastros na verdade degradou o desempenho.

Resultados

• Detecção de Violações: A melhor configuração (Qwen3-8B treinado em 3.208 rastros de bugs manifestos formatados em HTML + inferência CoT) melhorou a detecção de violações de uma linha de base de 49,4% para 67,3%.
• Precisão Geral: O modelo treinado alcançou 72,7% de precisão geral, aproximando-se do desempenho do modelo base Qwen3-32B (76,2%) enquanto o supera substancialmente na detecção de violações (67,3% vs. 56,9%).
• Generalização: As melhorias transferiram-se para todos os cinco tipos de propriedades, incluindo terminação, condições de corrida de dados e alcançabilidade, mesmo que os rastros de treinamento (verificações integradas do Soteria) visassem principalmente segurança de memória e overflows. Isso sugere que o modelo aprendeu padrões gerais de raciocínio de verificação.
• Sensibilidade ao Formato: Preservar o formato HTML estruturado da saída do Soteria foi crítico. Converter rastros para texto simples ou resumos em linguagem natural informal degradou significativamente o desempenho, particularmente quando combinado com CoT.
• Descobertas de Ablação:
  • Treinar em todos os rastros (incluindo não-bugs) prejudicou o desempenho.
  • Treinar em bugs latentes (não provados em todos os caminhos) prejudicou o desempenho.
  • Treinar apenas no código C bruto prejudicou o desempenho.
  • Prompting few-shot com exemplos de rastros não conseguiu replicar os ganhos do CPT.

Significado e Alegações

O artigo afirma que artefatos de verificação formal servem como um recurso potente, anteriormente inexplorado, para treinar LLMs em semântica de código de baixo nível. O significado principal reside em demonstrar que:

1. A escala não é o único motor: Um modelo menor (8B) treinado em rastros semânticos específicos pode superar um modelo muito maior (32B) na tarefa específica de detecção de bugs.
2. A Semântica do Rastro importa: O raciocínio lógico estruturado embutido nos rastros de execução simbólica (por exemplo, condições de caminho, transições de estado de memória) é mais valioso para verificação do que o volume bruto de código.
3. Superaditividade: A combinação de internalizar a lógica de verificação via pré-treinamento e utilizar raciocínio estendido (CoT) na inferência cria uma capacidade que nenhum dos componentes possui isoladamente.

Os autores enfatizam que sua abordagem não requer anotação manual, depende de ferramentas e código de código aberto e produz modelos que generalizam para tarefas de verificação não vistas (incluindo aquelas não verificadas explicitamente pela ferramenta de treinamento, como condições de corrida de dados). Eles concluem que, embora a abordagem melhore a confiabilidade, ela ainda não fecha a lacuna para ferramentas de verificação formal, e trabalhos futuros devem explorar contextos de múltiplos arquivos e loops de aprendizado por reforço.