IC3-Evolve: Proof-/Witness-Gated Offline LLM-Driven Heuristic Evolution for IC3 Hardware Model Checking

O artigo apresenta o IC3-Evolve, um framework automatizado que utiliza um modelo de linguagem (LLM) para evoluir offline heurísticas do verificador de hardware IC3, garantindo a correção de cada alteração por meio de validação estrita baseada em certificados de prova ou traços de contraexemplo, resultando em uma ferramenta final independente de ML e com desempenho superior em benchmarks industriais.

O essencial

Imagine que você é um engenheiro de tráfego encarregado de garantir que carros (dados) em uma cidade complexa (um circuito de computador) nunca entrem em um bairro perigoso (um estado de erro).

A tarefa é enorme. A cidade tem milhões de ruas e cruzamentos. Se você tentar dirigir por cada uma delas para ver se há um acidente, você nunca vai terminar. É aqui que entra o IC3, um algoritmo inteligente que funciona como um detetive de lógica. Ele não dirige por todas as ruas; ele usa atalhos e regras para provar matematicamente que é impossível chegar ao bairro perigoso. Se ele não consegue provar isso, ele mostra exatamente qual caminho levou ao desastre (o "erro").

O problema é que o detetive IC3 é muito inteligente, mas tem um manual de instruções cheio de "truques" (heurísticas) que os humanos precisam ajustar manualmente. É como tentar afinar um piano com as mãos sujas de óleo: é difícil, demorado e, se você apertar uma tecla errada, o piano pode tocar uma nota desafinada e estragar tudo.

Aqui é onde entra o IC3-Evolve, a solução proposta neste artigo. Vamos entender como funciona com uma analogia simples:

1. O Grande Problema: A "Caixa Preta" de Ajustes

Atualmente, melhorar o IC3 é como tentar consertar um carro de corrida ajustando parafusos no escuro. Os engenheiros tentam mudar uma pequena parte do código, testam em milhares de circuitos e, se o carro ficar mais rápido, eles mantêm. Se o carro explodir (der um erro falso), eles jogam fora e tentam de novo. É um processo lento, caro e propenso a erros humanos.

2. A Solução: O "Mestre de Obras" com um "Inspector Rigoroso"

O IC3-Evolve usa uma Inteligência Artificial (um LLM, como o GPT) para fazer esse trabalho de ajuste, mas com uma regra de ouro: a IA trabalha apenas à noite, no escritório, e nunca dirige o carro.

Aqui está o processo passo a passo, usando nossa analogia:

• O Arquiteto (A IA): Durante a noite, a IA olha para o manual de instruções do IC3. Ela diz: "Ei, e se trocássemos a ordem em que o detetive verifica as ruas? Ou se ele pulasse algumas ruas que já sabemos que estão vazias?". Ela escreve uma pequena "parche" (um pedaço de código novo).

• A Regra do "Slot" (A Caixa de Ferramentas Limitada): Para não deixar a IA louca e mudar tudo de uma vez, o sistema a obriga a mexer apenas em uma pequena caixa de ferramentas por vez (chamada de "slot"). É como dizer: "Hoje, você só pode mexer no freio. Amanhã, só no volante." Isso torna o teste mais seguro e fácil de entender.

• O Inspector de Segurança (O Portão de Prova): Esta é a parte mais importante. Antes de qualquer mudança ser aceita, ela passa por um teste duplo e infalível:

  • Se o sistema diz "Tudo Seguro" (SAFE): Ele deve entregar um certificado de segurança (uma prova matemática) que um outro programa, totalmente independente, verifica. Se o certificado for falso, a mudança é rejeitada.
  • Se o sistema diz "Perigo" (UNSAFE): Ele deve entregar um mapa do acidente (uma trilha de erro) que pode ser reproduzida em um simulador. Se o mapa não levar ao acidente real, a mudança é rejeitada.
  • Resumo: Nenhuma mudança é aceita a menos que ela seja 100% correta. A IA não pode "chutar" ou "adivinhar" a segurança; ela tem que provar.

• O Carro Final (O Produto): Depois que a IA faz todas as suas sugestões e o Inspector aprova as melhores, o resultado é um novo IC3. O mais legal? A IA desaparece. O novo IC3 é um programa independente, super-rápido, que não precisa de internet, nem de servidores de IA, nem de gastar energia extra para "pensar" enquanto roda. Ele é apenas um código melhorado.

3. O Resultado: Um Detetive Mais Esperto

Os autores testaram isso em uma competição mundial de verificação de hardware (HWMCC).

• Eles pegaram um IC3 "básico".
• Deixaram o sistema "evoluir" por 200 rodadas de ajustes automáticos.
• O resultado foi um IC3 que resolveu muito mais problemas e foi muito mais rápido do que as versões anteriores, inclusive superando concorrentes que são usados na indústria hoje.

Por que isso é incrível?

Imagine que você tem um carro que faz 10 km/litro. Você contrata um gênio da mecânica (a IA) para melhorar o motor.

• Abordagem antiga: O gênio fica no carro dirigindo e gritando instruções em tempo real. Isso gasta muita energia e o carro fica lento.
• Abordagem do IC3-Evolve: O gênio fica na garagem à noite, desmonta o motor, testa peças novas, verifica se o carro não vai explodir com um teste rigoroso, e depois monta um motor novo. De manhã, você pega o carro pronto. Ele é mais rápido, consome menos combustível e não precisa mais do gênio.

Conclusão

O IC3-Evolve mostra que podemos usar Inteligência Artificial para melhorar softwares complexos e críticos (como os que controlam aviões e usinas nucleares) sem arriscar a segurança. A IA é usada apenas para projetar a melhoria, e um sistema de verificação matemática garante que a melhoria é real e segura. É como ter um assistente que escreve o código, mas um juiz rigoroso que só assina o documento se tudo estiver perfeito.

Resumo técnico

1. O Problema

A verificação formal de propriedades é fundamental para a verificação de hardware moderno, especialmente com o aumento da complexidade dos circuitos integrados. O algoritmo IC3 (também conhecido como Property-Directed Reachability ou PDR) é o padrão da indústria para verificação de segurança de hardware. Ele determina se um sistema de transição de estados viola uma propriedade de segurança, retornando:

• UNSAFE: Com um traço de contraexemplo (witness).
• SAFE: Com um invariante indutivo verificável (proof).

Desafios Atuais:

• Dependência de Heurísticas: O desempenho prático do IC3 não depende apenas do algoritmo central, mas de uma complexa rede de heurísticas e escolhas de implementação (ex: generalização, propagação de cláusulas, interação com motores SAT).
• Ajuste Manual Frágil: O ajuste manual dessas heurísticas é custoso, frágil e difícil de reproduzir. Pequenas mudanças podem melhorar um conjunto de casos de teste enquanto degradam outros (regressões).
• Limitações de Soluções Baseadas em ML: Abordagens anteriores que integram ML/LLM diretamente no loop de verificação (ex: NeuroPDR, DeepIC3) introduzem custos de inferência, latência e dependência de modelos em tempo de execução, o que é indesejável para fluxos de produção industriais.

2. Metodologia: IC3-Evolve

O IC3-Evolve é uma estrutura de evolução de código offline que utiliza um Grande Modelo de Linguagem (LLM) para propor e refinar heurísticas do IC3, garantindo correção absoluta através de validação rigorosa.

Principais Componentes:

1. Evolução Offline: O LLM não é usado durante a verificação final. Ele opera apenas na fase de desenvolvimento para gerar "patches" de código. O artefato final é um verificador IC3 autônomo, sem dependência de modelos de ML em tempo de execução.
2. Espaço de Patches Restrito por "Slots":
   • O código do IC3 é dividido em "slots" (localizações específicas onde heurísticas podem ser alteradas, como tratamento de obrigações de prova, generalização de predecessores, propagação, etc.).
   • O agente "Programador" do LLM propõe patches pequenos e restritos a um ou poucos slots por vez, tornando as alterações auditáveis e interpretáveis.
   • O sistema utiliza "pacotes de conhecimento" específicos para cada slot para guiar o LLM com contexto relevante.
3. Validação por Portões de Prova e Testemunha (Proof-/Witness-Gated):
   • Esta é a inovação central de segurança. Nenhum patch é promovido a menos que passe em verificações de correção independentes:
     • Caso SAFE: O solver deve emitir um invariante indutivo que seja validado por uma ferramenta externa (CERTIFAIGER).
     • Caso UNSAFE: O solver deve emitir um traço de contraexemplo que seja reprodutível por um simulador (AIGSIM).
   • Se a validação falhar (mesmo que o desempenho pareça melhor), o patch é rejeitado imediatamente. Isso garante que a evolução nunca comprometa a correção lógica do algoritmo.
4. Estratégia de Busca Compass & Jump:
   • Um agente "Avaliador" executa os benchmarks e diagnostica falhas.
   • Uma política de busca (Compass & Jump) decide se deve focar em um único slot (Compass) ou explorar sinergias entre múltiplos slots (Jump), baseada no histórico de progresso e feedback do avaliador.

3. Contribuições Chave

• Framework IC3-Evolve: Introduz um método para evoluir heurísticas de IC3 através de edição de código controlada por LLM, compilando melhorias validadas diretamente no solver.
• Workflow de Evolução de Heurísticas: Desenvolveu uma estratégia que explora refinamentos locais e mudanças cruzadas entre módulos, guiada por uma política de busca adaptativa.
• Garantia de Correção Rigorosa: Implementa portões de validação baseados em prova/testemunha, prevenindo a implantação de alterações não sólidas (unsound).
• Desempenho Superior sem Overhead: Demonstra que é possível descobrir melhorias heurísticas práticas sem adicionar latência de inferência de ML ao produto final.

4. Resultados Experimentais

Os experimentos foram conduzidos no conjunto de benchmarks público HWMCC (Hardware Model Checking Competition) e em conjuntos industriais não vistos durante o treinamento.

• Configuração: O sistema evoluiu a partir do solver base IC3ref em 200 iterações offline.
• Comparação com Baselines:
  • O IC3-Evolve superou significativamente o IC3ref original, versões com backends SAT mais fortes, e até mesmo o rIC3 (vencedor recente do HWMCC) quando comparado com o mesmo backend SAT (CaDiCaL).
  • Métricas (HWMCC Set B - Não visto):
    • IC3-Evolve: 94 casos resolvidos, PAR2 de 464.56s.
    • rIC3-CaDiCaL: 89 casos resolvidos, PAR2 de 524.35s.
    • IC3ref: 75 casos resolvidos, PAR2 de 1068.33s.
• Generalização: O solver evoluído manteve o desempenho superior em benchmarks industriais reais, resolvendo 225 de 302 casos com um PAR2 de 1044.26s, superando todas as baselines.
• Estudo de Ablação:
  • Evolução restrita a um único slot (Slot-isolated) produziu ganhos marginais e instáveis.
  • A composição ingênua das melhores edições de slots individuais (Naive-Compose) foi inferior à evolução completa, provando que as heurísticas do IC3 são acopladas e exigem otimização coordenada e guiada por feedback.
  • O "Portão de Testemunha" foi crucial: um caso hipotético mostrou que um patch que melhoraria o desempenho seria rejeitado por falhar na validação de correção, evitando uma regressão de segurança.

5. Significado e Conclusão

O IC3-Evolve demonstra que a verificação baseada em prova oferece um ambiente único e seguro para a evolução de código impulsionada por LLMs. Ao separar a otimização (offline) da execução (runtime) e impor validação matemática rigorosa, o framework consegue:

1. Automatizar a engenharia de heurísticas complexas que são difíceis de ajustar manualmente.
2. Produzir solvers de alto desempenho que são standalone (sem dependência de ML em tempo de execução), facilitando sua adoção em fluxos de trabalho industriais de EDA (Electronic Design Automation).
3. Estabelecer um novo paradigma onde a correção formal é usada como o "guardião" para permitir a exploração autônoma de espaços de código complexos.

Em resumo, o trabalho prova que é possível evoluir algoritmos de verificação de hardware de ponta de forma autônoma e segura, superando os solvers atuais sem sacrificar a confiabilidade ou introduzir custos computacionais adicionais na fase de uso.