💻 computer science

Neuro-Symbolic Software Verification: Hyper-charging Local Language Models with Symbolic Reasoning at Scale

Este artigo apresenta o VerIbmc, um pipeline neuro-simbólico que aproveita modelos de linguagem locais de pesos abertos combinados com síntese de invariantes simbólicos e feedback iterativo de verificadores para alcançar o estado da arte em geração de invariantes de laço para verificação de software, oferecendo uma alternativa preservadora de privacidade e de baixo custo às ferramentas proprietárias baseadas em nuvem.

Autores originais: Muhammad A. A. Pirzada, Julian Parsert, Weiqi Wang, Konstantin Korovin, Lucas C. Cordeiro

Publicado 2026-06-16

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Muhammad A. A. Pirzada, Julian Parsert, Weiqi Wang, Konstantin Korovin, Lucas C. Cordeiro

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á tentando provar que uma máquina complexa (um programa de computador) nunca irá quebrar, não importa quantas vezes você a execute. A parte mais difícil dessa prova é entender os "loops" da máquina — partes onde ela repete uma tarefa repetidamente. Para provar que a máquina é segura, você precisa encontrar um Invariante de Loop.

Pense em um Invariante de Loop como uma "regra de segurança" que deve ser verdadeira toda vez que a máquina inicia um novo ciclo de seu loop. Por exemplo, se um loop conta de 10 até 0, a regra de segurança pode ser: "O número está sempre entre 0 e 10". Se você puder provar que essa regra se mantém verdadeira no início, permanece verdadeira após cada etapa e leva a um término seguro, toda a máquina é provada segura.

O problema é que encontrar essas regras automaticamente é incrivelmente difícil. É como tentar adivinhar a combinação secreta de um cofre sem ter nenhuma pista.

O Jeito Antigo vs. O Jeito Novo

O Jeito Antigo (Raciocínio Simbólico):
Tradicionalmente, os computadores tentavam encontrar essas regras usando matemática e lógica rigorosas. É como um contador superpreciso verificando cada número. É muito confiável, mas é lento e frequentemente fica travado em problemas complexos e desordenados. É como tentar resolver um labirinto verificando cada parede, uma por uma.

O Jeito da "Nuvem" (Grandes Modelos de IA):
Recentemente, as pessoas começaram a usar modelos de Inteligência Artificial (IA) massivos para adivinhar essas regras. Essas IAs são como estudantes brilhantes e muito bem instruídos que leram milhões de exemplos de código. Elas conseguem adivinhar a regra certa muito rapidamente. No entanto, para usá-las, você geralmente precisa enviar seu código para um servidor gigante e caro na nuvem (como enviar seus projetos secretos para um estranho). Isso é ruim para empresas que precisam manter a privacidade de seu código e custa muito dinheiro.

A Solução: VerIbmc (O "Super-Ajudante" Local)

Os autores deste artigo construíram um novo sistema chamado VerIbmc. Pense nele como um oficina local onde você pode usar um assistente de IA inteligente sem nunca sair do seu prédio.

Veja como o VerIbmc funciona, usando uma analogia simples:

Imagine que você está tentando resolver um quebra-cabeça difícil (o invariante de loop).

O Detetive Determinístico (Fase 0 e 1): Antes de pedir ajuda à IA, o VerIbmc envia um detetive estrito e lógico (uma ferramenta chamada ESBMC) para examinar o quebra-cabeça. O detetive verifica fatos simples primeiro. Se o quebra-cabeça for fácil, o detetive o resolve instantaneamente. Se o detetive encontrar algumas pistas sólidas (como "o número é sempre positivo"), ele as escreve em um quadro branco.
O Assistente de IA Local (Fase 2): Se o detetive ficar travado, ele chama o Assistente de IA Local. Mas aqui está o truque: a IA não começa do zero. O detetive entrega à IA o quadro branco com as pistas que já encontrou.
O Ciclo de Feedback: A IA adivinha uma solução completa. O detetive a verifica.
- Se estiver errada, o detetive não diz apenas "Não". Eles dizem: "Esta parte está errada, mas esta outra parte está realmente correta". Eles pegam a parte correta, escrevem no quadro branco e pedem para a IA tentar novamente, usando as novas pistas.
- Isso acontece repetidamente até que o quebra-cabeça seja resolvido ou o tempo acabe.

Duas Formas de Pensar (CoT vs. ToT)

O artigo também testou como a IA deve "pensar" enquanto resolve o quebra-cabeça:

Cadeia de Pensamento (Chain-of-Thought - CoT): A IA pensa em linha reta, passo a passo, como se estivesse escrevendo uma única história.
Árvore de Pensamentos (Tree-of-Thoughts - ToT): A IA se ramifica, como uma árvore. Ela tenta vários caminhos diferentes ao mesmo tempo, vê qual parece promissor e então foca sua energia nos melhores caminhos. O artigo descobriu que, para os modelos de IA mais fortes, este método de ramificação foi ótimo, mas para modelos menores e mais fracos, às vezes desperdiçava tempo.

Os Resultados: Por Que Isso Importa

Os pesquisadores testaram este sistema em centenas de diferentes quebra-cabeças de programação usando cinco modelos de IA diferentes de "pesos abertos" (modelos que qualquer pessoa pode baixar e rodar em seus próprios computadores).

Privacidade em Primeiro Lugar: Como tudo roda em uma máquina local, nenhum código sai da organização. É como fazer seu dever de casa de matemática no seu próprio quarto em vez de entregá-lo a um estranho.
Custo-Benefício: Você não precisa pagar taxas caras para grandes empresas de nuvem.
Desempenho: A melhor configuração (usando um modelo local grande chamado GPT-OSS-120B) resolveu 86,4% dos problemas. Isso é melhor do que muitas ferramentas tradicionais e competitivo com as ferramentas de IA baseadas em nuvem e caras.
O Impulso "Gratuito": O sistema descobriu que a fase do "Detetive" (a parte simbólica) resolveu 75 problemas sozinha, sem precisar da IA. Para modelos de IA mais fracos, as pistas do detetive ajudaram-nos a resolver 35 problemas a mais do que conseguiriam resolver sozinhos.

A Conclusão

O VerIbmc prova que você não precisa de supercomputadores na nuvem caros e que invadem a privacidade para verificar a segurança do software. Ao combinar um detetive lógico estrito com um assistente de IA local inteligente que aprende com seus erros, você pode obter resultados de alto nível diretamente no seu próprio computador. É uma forma de tornar a verificação de software privada, acessível e poderosa.

Resumo Técnico: Verificação de Software Neuro-Simbólica com VerIbmc

Declaração do Problema

A síntese de invariantes de laço permanece como um gargalo central na verificação formal de software. Embora existam técnicas simbólicas (ex: interpretação abstrata, resolução de restrições) e métodos baseados em dados de "tentativa e erro" (guess-and-check), elas frequentemente enfrentam dificuldades com escalabilidade, expressividade ou a diversidade de códigos do mundo real. Recentemente, os Grandes Modelos de Linguagem (LLMs) mostraram promessa na geração de candidatos a invariantes ao alavancar padrões aprendidos de corpora de código. No entanto, as abordagens neuro-simbólicas existentes normalmente dependem de modelos proprietários e fechados acessados via APIs de nuvem externas. Essa dependência introduz obstáculos significográficos para a implantação industrial:

Privacidade e Conformidade: O código-fonte deve ser transmitido para serviços de terceiros, levantando preocupações de confidencialidade.
Reprodutibilidade: A dependência de provedores externos complica a integração em pipelines de verificação controlados.
Custo e Sustentabilidade: Modelos de grande escala são computacionalmente caros e energeticamente intensivos, limitando sua praticidade para fluxos de trabalho de verificação contínua.

Os autores postulam que esses desafios exigem uma mudança em direção a modelos de linguagem de pesos abertos (open-weight), implantáveis localmente, que possam operar inteiramente dentro da infraestrutura de uma organização sem expor o código proprietário.

Metodologia: O Pipeline VerIbmc

O artigo apresenta o VerIbmc, um pipeline neuro-simbólico projetado para sintetizar invariantes de laço para programas em C, combinando o raciocínio simbólico com LLMs de pesos abertos hospedados localmente. O sistema utiliza o ESBMC (Efficient SMT-Based Context-Bounded Model Checker) como o oráculo de verificação. O pipeline é desenhado sob o princípio de "escalar apenas quando necessário", priorizando o raciocínio simbólico determinístico e barato antes de invocar o LLM.

Arquitetura Central

O pipeline opera em três fases distintas:

Fase 0 (Verificação de Linha de Base): O ESBMC verifica o programa não anotado. Se o programa for trivialmente seguro ou comprovadamente inseguro, o processo termina imediatamente, evitando esforço desnecessário de síntese.
Fase 1 (Geração de Candidatos Simbólicos): Se a Fase 0 retornar "Desconhecido" (Unknown), o sistema enumera simbolicamente átomos candidatos através da comparação pareada de variáveis de entrada do laço e constantes. Esses átomos são verificados quanto à indutividade usando o ESBMC. O sistema mantém três armazenamentos: Provável ( $P$ ), Desprovável ( $D$ ) e Desconhecido ( $U$ ). Se a conjunção de todos os átomos prováveis for suficiente para provar a pós-condição, o pipeline termina com sucesso sem qualquer chamada de LLM.
Fase 2 (Loop de Refinamento do LLM): Se a fase simbólica for insuficiente, o pipeline entra em um loop iterativo onde um LLM é solicitado a gerar novos invariantes.
- Mecanismo de Feedback: O LLM recebe o programa atual, o conteúdo dos armazenamentos $P$ , $D$ e $U$ como feedback estruturado, e exemplos de poucos disparos (few-shot).
- Decomposição e Recombinação: Quando um candidato gerado pelo LLM falha na verificação, o sistema o decompõe em subfórmulas (átomos). Os átomos são verificados individualmente e adicionados ao respectivo armazenamento. A conjunção de todos os átomos atualmente prováveis é então re-verificada. Isso permite que o sistema aproveite componentes úteis de propostas falhas do LLM.
- Terminação: O loop continua até que um invariante válido seja encontrado, o orçamento de iteração se esgote ou ocorra um tempo limite (timeout).

Estratégias de Inferência

Os autores avaliam quatro estratégias de inferência baseadas em dois eixos de design:

Feedback do Verificador (Prior Simbólico):
- Básico (Basic): Executa o pipeline completo de três fases, utilizando o prior simbólico da Fase 1 e a filtragem por nível de átomo.
- Apenas LLM (LLM-Only): Pula a Fase 1 e a decomposição por nível de átomo, confiando exclusivamente no LLM para gerar invariantes indutivos como um todo. Isso serve como uma linha de base de ablação.
Estrutura de Raciocínio:
- Cadeia de Pensamento (Chain-of-Thought - CoT): Utiliza prompting padrão com exemplos de raciocínio passo a passo (Indutivo, Lógica de Hoare, Cláusula de Horn ou derivação direta).
- Árvore de Pensamentos (Tree-of-Thoughts - ToT): Explora múltiplos estilos de derivação em paralelo durante uma etapa de "exploração" (scouting), pontua-os com base no número de átomos prováveis gerados e concentra o restante do orçamento de iteração nos dois estilos de melhor desempenho.

Contribuições Principais

Pipeline Neuro-Símbólico: Um sistema completo que integra LLMs de pesos abertos servidos localmente com o ESBMC para a síntese automatizada de invariantes de laço, operando inteiramente em infraestrutura interna.
Avaliação Sistemática de Estratégias: Uma comparação abrangente das variantes de LLM puro, guiada por símbolos e de Árvore de Pensamentos (ToT), demonstrando o impacto do feedback simbólico e das estruturas de raciocínio.
Ganhos de Feedback Simbólico: Demonstração de que fornecer átomos de invariantes prováveis como contexto para o LLM gera ganhos consistentes, particularmente para modelos mais fracos (ex: Llama-3.1-8B ganha +35 benchmarks resolvidos sobre uma linha de base de LLM puro).
Análise de Engenharia de Prompt: Avaliação de diferentes estilos de prompting (CoT vs. ToT) e templates de raciocínio (Indutivo, Lógica de Hoare, Cláusula de Horn) na síntese de invariantes.
Benchmarking de Larga Escala: Uma avaliação extensa através de cinco famílias de modelos (de 7B a 120 bilhões de parâmetros), quatro estratégias de inferência e cinco famílias de benchmarks (520 problemas, 499 efetivos), totalizando 10.400 resultados por problema.

Resultados Experimentais

A avaliação foi conduzida em um servidor com quatro GPUs NVIDIA RTX A6000 usando cinco modelos de pesos abertos: GPT-OSS-120B, GPT-OSS-20B, Qwen2.5-32B, Qwen2.5-7B e Llama-3.1-8B.

Desempenho Geral: A melhor configuração única (GPT-OSS-12B com a estratégia Basic) resolveu 431 de 499 problemas (86,4%).
Comparação com o Estado da Arte (SOTA):
- O VerIbmc supera substancialmente as ferramentas simbólicas tradicionais (CPA-Checker, 2ls, ESBMC-Kind) e ferramentas puramente neurais (Code2Inv) quando executadas no mesmo hardware local.
- Em conjuntos de benchmarks compartilhados, o VerIbmc é competitivo ou ligeiramente inferior às ferramentas mais fortes aumentadas por LLM (Clause2Inv, LaM4Inv, LORIS) que dependem de APIs externas caras (ex: GPT-4). Notavelmente, o VerIbmc alcança esses resultados sem transmitir código para a nuvem.
- O VerIbmc escala unicamente para o conjunto completo de benchmarks SV-COMP (154 problemas), incluindo programas com arrays, laços aninhados e ponteiros, que muitas ferramentas concorrentes não conseguem expressar devido a limitações de frontend.
Impacto da Fase Simbólica: A Fase 1 simbólica resolveu 75 problemas sem qualquer chamada de LLM. Para modelos mais fracos, o aumento simbólico proporcionou ganhos significativos (até +35 problemas adicionais resolvidos para o Llama-3.1-8B).
ToT vs. CoT: O prompting ToT mostrou um compromisso entre diversidade e precisão. Embora tenha alcançado pares problema-modelo únicos inacessíveis ao CoT, frequentemente incorreu em um overhead de tempo de execução (wall-clock) e, para modelos mais fracos, resultou em uma diminuição líquida de problemas resolvidos devido ao esgotamento do orçamento de iteração. Para os modelos mais fortes (GPT-OSS-120B), a diferença de desempenho entre CoT e ToT foi insignificante.
Capacidade do Modelo: Os resultados indicam que a capacidade do modelo é o principal motor da precisão. A lacuna entre os modelos mais fortes e os mais fracos foi significativamente maior do que a variância de desempenho introduzida pela mudança de estratégias dentro do mesmo modelo.

Significância e Alegações

O artigo alega que o VerIbmc demonstra que uma abordagem neuro-simbólica baseada em LLMs pode ser aplicada efetivamente à síntese de invariantes de uma maneira que preserva a privacidade e é eficiente em termos de energia. Ao operar inteiramente em infraestrutura local com modelos de pesos abertos, a abordagem elimina a necessidade de modelos de fronteira proprietários caros travados atrás de APIs.

Os autores enfatizam que seu método é correto por construção (sound by construction): cada candidato a invariante é validado por um verificador formal (ESBMC) antes da aceitação. Embora o sistema seja incompleto devido à indecidibilidade do problema, ele fornece um caminho prático, escalável e reproduzível para a verificação assistida por IA de software de produção. O trabalho dá um passo em direção a pipelines de verificação prontos para a indústria, onde a privacidade de dados e a eficiência de recursos são requisitos críticos.