Large Lemma Miners: Can LLMs do Induction Proofs for Hardware?

1. Declaração do Problema

A Verificação Formal (FV) é crítica para garantir a correção de projetos de hardware (RTL). No entanto, verificar projetos industriais complexos permanece um gargalo devido à natureza "nível de bit" da maioria das ferramentas de verificação de modelos. Essas ferramentas têm dificuldade em construir provas matemáticas de alto nível, independentes de bits, necessárias para propriedades complexas.

A abordagem padrão para resolver isso é a Prova por Indução, que requer lema auxiliares (reforços indutivos) para provar uma propriedade. Atualmente, a geração desses lemas é uma tarefa manual e intensiva em mão de obra, realizada por engenheiros especialistas em FV. O artigo aborda a questão: Os Grandes Modelos de Linguagem (LLMs) podem automatizar a mineração desses lemas auxiliares para construir argumentos indutivos válidos para verificação de hardware?

2. Metodologia: Uma Abordagem Neurosimbólica

Os autores propõem um framework neurosimbólico que combina as capacidades generativas dos LLMs com o rigor de ferramentas simbólicas formais. O sistema não depende exclusivamente da saída do LLM; em vez disso, usa o LLM para gerar candidatos e um solucionador formal para verificar e filtrá-los.

A. Componentes Principais

1. Frameworks de Prompting de LLM: Duas estratégias distintas são usadas para gerar lemas candidatos:

   • Não Agente (Prompt Único): Usa um prompt de Few-Shot contendo $k$ exemplos de triplas (Design RTL, Propriedade, Lemmas Indutivos). Os exemplos são selecionados via similaridade semântica (usando transformadores de sentença) de um pool pré-construído de Cadeia de Pensamento (CoT). O LLM é amostrado $n$ vezes com o mesmo prompt para reunir candidatos diversos.
   • Agente (Interação Iterativa): Enquadra a geração de lemas como um loop. O LLM propõe lemas, que são verificados pela ferramenta formal. Se a verificação falhar, a ferramenta fornece feedback (indicando quais lemas falharam e por quê) e uma mensagem de "reparo". O LLM então refina suas sugestões em turnos subsequentes (até 5 iterações).

2. Algoritmo de Raciocínio Formal (FINDINDSTRENGTH):

   • Este algoritmo recebe o conjunto de lemas candidatos gerados pelo LLM e tenta encontrar um subconjunto que forme um Reforço Indutivo válido.
   • Reforço Indutivo: Um conjunto de lemas $L$ tal que $L \land \text{Propriedade}$ é um invariante indutivo (satisfaz iniciação e consecução).
   • Processo:
     1. Filtragem: Verifica se os lemas individuais são invariantes indutivos (usando 1-indução) ou se valem até uma profundidade limitada (usando Verificação de Modelo Limitada, BMC).
     2. Ordenação: Prioriza lemas conhecidos por serem invariantes indutivos sobre aqueles que valem apenas dentro de um limite.
     3. Busca de Subconjunto: Itera através dos prefixos da lista ordenada para encontrar o menor subconjunto que, quando conjuntado com a propriedade alvo, forma um invariante indutivo válido.
   • Ferramentas: Implementado usando EBMC (uma ferramenta de verificação formal) com $k$-indução e BMC.

B. Conjunto de Dados

O framework foi avaliado em 110 tarefas de verificação compreendendo:

• 58 designs em SystemVerilog (de fontes como VCEGAR, VIS, v2c e designs personalizados de FIFO/Arbiter/CAM).
• 47 exemplos derivados de programas C: Código C traduzido em Máquinas de Estado Finito (FSMs) em SystemVerilog para testar a generalização.
• Pool CoT: Um pequeno conjunto de exemplos escritos manualmente usados para prompting de Few-Shot.

3. Contribuições Principais

1. Geração Neurosimbólica de Lemmas: Demonstra o primeiro caso de uso de LLMs especificamente para minerar lemas auxiliares para a construção de provas formais em verificação de hardware.
2. Framework de Prompting Dual: Implementa e compara uma abordagem estática de Few-Shot contra uma abordagem Agente iterativa, mostrando que esta última pode guiar o LLM para longe de caminhos incorretos.
3. Avaliação Empírica: Fornece um estudo abrangente em 110 tarefas, destacando que os LLMs podem gerar com sucesso argumentos indutivos não triviais para designs RTL de código aberto de tamanho médio.
4. Tratamento de Alucinações: Prova que, embora os LLMs alucinem (produzindo lemas sintaticamente inválidos ou logicamente incorretos), uma camada de filtragem formal pode extrair efetivamente as provas corretas do ruído.

4. Resultados Experimentais

Os experimentos foram conduzidos em instâncias da Amazon EC2 usando seis LLMs de última geração (GPT-5, Claude 3.7, Claude 4 Sonnet, Claude 4.5 Sonnet, Claude 4.5 Haiku, Claude 4.5 Opus).

• Taxa de Sucesso: O framework gerou com sucesso argumentos indutivos comprovadamente corretos para 84% das 110 tarefas de verificação.
  • Configuração Agente: Resolveu 92/110 exemplos (84% de taxa de sucesso).
  • Configuração Não Agente: Resolveu 84/110 exemplos (76% de taxa de sucesso).
• Desempenho do Modelo: O Claude 4.5-Opus teve o melhor desempenho, resolvendo 88 exemplos na configuração Agente.
• Comparação com Ferramentas SOTA:
  • Os autores identificaram 31 benchmarks "desafiadores" onde ferramentas industriais de última geração (JasperGold, VC-Formal, rIC3) falharam em provar a propriedade dentro de um tempo limite de 10 minutos.
  • A abordagem baseada em LLM resolveu instâncias que essas ferramentas SOTA não conseguiram, particularmente em casos que exigiam reforços indutivos complexos (por exemplo, designs específicos de FIFO e Arbiter).
  • Em alguns casos onde o LLM encontrou o lema correto, mas a verificação formal esgotou o tempo, o resultado ainda foi considerado um sucesso em termos de geração de lemas, pois o gargalo foi o tempo de execução da ferramenta de verificação, e não o raciocínio do LLM.
• Análise de Erros:
  • Os LLMs ocasionalmente alucinaram sintaxe SVA (por exemplo, operadores inválidos, variáveis não definidas) ou usaram caracteres não ASCII.
  • A configuração Agente foi mais eficiente, frequentemente encontrando soluções com menos lemas totais ao refinar iterativamente o espaço de busca.

5. Significado e Impacto

• Valor Industrial: Esta abordagem tem o potencial de reduzir significativamente o esforço manual exigido por engenheiros de Verificação Formal. Ao automatizar a descoberta de lemas auxiliares, reduz a barreira para a aplicação de métodos formais em projetos de hardware complexos.
• Além da Memorização: Os resultados sugerem que os LLMs estão realizando raciocínio genuíno em vez de simples memorização, pois generalizaram com sucesso para exemplos derivados de C e lidaram com variações na instanciação de parâmetros e nomeação de registradores.
• Direções Futuras: Os autores planejam estender o framework para lidar com múltiplas propriedades simultaneamente, escalar para projetos industriais maiores e validar a abordagem em um cenário industrial real.

Conclusão: O artigo estabelece que os LLMs, quando acoplados a ferramentas de verificação formal em um loop neurosimbólico, são um método viável e poderoso para automatizar a parte mais difícil das provas de indução em hardware: a descoberta de lemas auxiliares.