Resumo Técnico: CircuitProver

Declaração do Problema

O design de circuitos integrados (IC) moderno enfrenta um gargalo crítico na verificação funcional devido ao aumento da complexidade. A metodologia dominante, a verificação de modelos (model checking), verifica cada instância de design separadamente, expondo apenas resultados de passar/falhar ou contraexemplos. Consequentemente, o raciocínio por trás de uma prova permanece trancado dentro das heurísticas do solver, e um raciocínio semelhante deve ser reconstruído repetidamente em designs relacionados. Embora a prova de teoremas interativa (ITP) ofereça artefatos de prova explícitos e reutilizáveis, sua aplicação ao hardware permanece amplamente manual, exigindo um esforço significativo de especialistas para formalização, descoberta de invariantes e construção de provas.

As ferramentas existentes carecem de conhecimento reutilizável: o model checking esconde o raciocínio, enquanto os atuais frameworks de ITP (por exemplo, Coq, ACL2) dependem fortemente de especialistas humanos. Na emergente "era dos agentes", onde agentes autônomos participam da geração e otimização de hardware, as ferramentas de verificação devem não apenas verificar a correção, mas também acumular e preservar artefatos de prova explícitos e estratégias de raciocínio para guiar agentes futuros.

Metodologia: CircuitProver

O artigo apresenta o CircuitProver, um framework de verificação baseado em Lean 4 e orientado a agentes, projetado para a verificação de hardware com acumulação de provas. Ele visa designs de hardware parametrizados (especificamente Chisel), permitindo que uma única prova estabeleça a correção para toda uma família de instâncias de hardware, em vez de verificar designs instanciados individualmente.

O framework opera através de três fases distintas:

Fase I: Auto-formalização de Hardware

O CircuitProver traduz automaticamente implementações de hardware parametrizadas e especificações em linguagem natural em modelos executáveis em Lean 4.

• Tradução: Um tradutor Chisel-para-Lean ($\mathcal{T}_{impl}$) determinístico converte designs de hardware em um modelo semântico unificado em Lean 4 ($L_D$). Este modelo preserva parâmetros de design, interfaces de E/S, estados de registradores e comportamentos de transição usando tipos de vetores de bits sensíveis à largura (width-aware).
• Validação: A tradução é validada via co-simulação exaustiva de baixa largura de bits para garantir que o modelo Lean se comporte identicamente ao design Chisel original.
• Formulação de Especificação: Um agente de raciocínio ($\mathcal{F}_{spec}$) interpreta especificações em linguagem natural ($S$) dentro do contexto de hardware para gerar propriedades formais em Lean 4 ($L_S$), preservando parâmetros simbolicamente.

Fase II: Prova de Teoremas de Hardware Orientada a Agentes

Um agente de raciocínio orientado a hardware constrói iterativamente provas verificadas por máquina através da interação com o provador de teoremas Lean 4. O fluxo de trabalho inclui:

1. Planejamento de Prova e Construção de Esqueleto: Em vez de busca direta por táticas, o agente decompõe a prova de correção em obrigações intermediárias estruturadas.
   • Para designs combinacionais, foca na correção de computação de um único ciclo, gerando lemas para aritmética e lógica de vetores de bits.
   • Para designs sequenciais, constrói provas de transição local de um passo e descobre invariantes indutivos para conectar a correção passo a passo com o comportamento global.
2. Prova Iterativa: O agente ($\mathcal{F}_{proof}$) gera scripts de prova, invoca o Lean e analisa o feedback (estados de prova e mensagens de erro). Ele refina o raciocínio, introduz lemas ou fortalece invariantes com base no feedback do Lean até que todas as obrigações sejam cumpridas.

Fase III: Biblioteca de Provas Reutilizáveis

Trajetórias de prova bem-sucedidas são destiladas em duas bibliotecas complementares para suportar tarefas futuras:

• Biblioteca de Guia de Prova: Armazena estratégias em linguagem natural explicando como uma prova foi decomposta, por que lemas específicos foram escolhidos e como adaptar planos com base no feedback. Ela captura a "rota" para a construção da prova.
• Biblioteca de Teoremas Verificados pelo Lean: Armazena fatos independentes de módulo e verificados por máquina. As provas são desacopladas de definições de módulos específicos e reformuladas sobre parâmetros simbólicos e interfaces genéricas, permitindo que lemas verificados (ex: lógica de carry-skip) sejam reutilizados em diferentes designs de hardware.

Principais Contribuições

1. Verificação de Hardware Nativa para Agentes: Introdução do CircuitProver, um framework que integra auto-formalização, prova de teoremas por agentes e bibliotecas de provas reutilizáveis.
2. Auto-formalização de Hardware: Um pipeline que traduz implementações Chisel e especificações de linguagem natural em representações unificadas e verificáveis em Lean 4.
3. Fluxo de Trabalho de Prova de Teoremas por Agentes: Um fluxo de trabalho orientado a hardware onde agentes constroem provas iterativamente usando feedback, abordando especificamente designs parametrizados e semântica de largura fixa.
4. Biblioteca de Provas Reutilizáveis: Um mecanismo para destilar traços de prova em estratégias de linguagem natural e artefatos formais, permitindo a transferência de conhecimento entre tarefas de verificação.
5. Suíte de Benchmarks: A primeira suíte de benchmarks para avaliar a prova de teoremas de hardware por agentes, cobrindo 63 tarefas Chisel parametrizadas (aritmética, controle, memória, diversos) e módulos de nível de processador.

Resultados Experimentais

Os autores avaliaram o CircuitProver contra um agente vanilla (mesmo LLM e configuração, mas sem bibliotecas reutilizáveis ou orientação de hardware) e Chicala/Stainless.

• Taxa de Sucesso: O CircuitProver provou com sucesso 100% (63/63) das tarefas do benchmark. O agente vanilla resolveu 92,1% (58/63), e o Chicala/Stainless teve dificuldades com a robustez do front-end, falhando ao compilar muitos designs.
• Eficiência: Comparado ao agente vanilla, o CircuitProver reduziu:
  • A média de rodadas de prova em 50,0%.
  • O tempo de verificação em 23,2%.
  • As Linhas de Código (LoC) de prova em 16,3%.
• Escalabilidade: Em módulos de nível de processador maiores (multiplicadores/divisores XiangShan e Rocket), o CircuitProver reduziu o tempo de verificação em 56,8% e o LoC de prova em 54,4% comparado ao agente vanilla.
• Estudos de Ablação:
  • A remoção da Biblioteca de Teoremas reduziu a taxa de sucesso de 100% para 95,2% (60/63), indicando que a biblioteca ajuda a resolver casos difíceis.
  • A remoção da Guia de Prova aumentou o número de rodadas necessárias para cobertura total de 18 para 29, mostrando que a orientação acelera o processo de busca.
• Escalonamento de Modelo: O desempenho escalou com a capacidade do LLM, sendo que o modelo mais forte (Opus 4.8) alcançou 100% de sucesso, enquanto modelos mais fracos (Haiku 4.5) resolveram apenas 31/63 tarefas.

Significância e Alegações

O artigo afirma que o conhecimento de prova reutilizável é um habilitador crítico para a verificação automatizada de hardware na era dos agentes. Ao mudar de saídas de verificação isoladas e implícitas para artefatos de prova explícitos e acumulados, o CircuitProver demonstra que:

1. A acumulação de provas reduz significativamente o esforço redundante em tarefas de verificação relacionadas.
2. A orientação voltada para hardware é essencial para uma busca de prova eficiente, particularmente para designs parametrizados e sequenciais.
3. A prova de teoremas por agentes pode alcançar cobertura total em diversos benchmarks de hardware onde a verificação de modelos tradicional falha em fornecer raciocínio reutilizável e o ITP manual é excessivamente trabalhoso.

Os autores posicionam o CircuitProver como um passo em direção a ferramentas de verificação que não apenas validam o hardware, mas também aprendem e melhoram ao longo do tempo, destilando padrões de raciocínio bem-sucedidos em bibliotecas reutilizáveis.