Resumo Técnico: BRIDGE – Construindo Representações em Síntese de Programas Verificados Guiada por Domínio

1. Declaração do Problema

Os Modelos de Linguagem de Grande Escala (LLMs) estão cada vez mais capazes de gerar código, mas, no contexto da verificação formal, os programas gerados frequentemente parecem corretos enquanto abrigam bugs sutis, casos de borda ausentes ou suposições incompatíveis. Em assistentes de prova como o Lean, a verificação de programas não é uma tarefa de geração única, mas um problema de previsão de múltiplos artefatos. Uma verificação bem-sucedida requer a consistência mútua de quatro artefatos acoplados:

1. Código Executável: A implementação.
2. Especificação Formal: Restrições comportamentais (pré-condições, pós-condições, invariantes).
3. Declarações de Teorema: Afirmações que conectam o código à especificação.
4. Tentativas de Prova: Scripts verificados pelo kernel para validar as afirmações.

Os sistemas atuais de LLMs lutam nesse cenário porque tratar esses artefatos de forma independente leva a deriva semântica. Um modelo pode gerar código que passa nos testes, mas falha nas verificações de terminação do Lean; uma especificação que passa na verificação de tipos, mas é vacua; ou um teorema que é provável, mas irrelevante para a tarefa original. O desafio central é traduzir a intenção informal em uma sequência de artefatos onde sintaxe, tipos, estruturas de recursão, contratos e obrigações de prova permaneçam alinhados.

2. Metodologia: O Framework BRIDGE

Os autores propõem o BRIDGE, um framework de prompt estruturado que decompõe o processo de codificação verificável em três domínios interligados: Código, Especificação e Teorema/Prova. Em vez de pedir a um modelo que salte diretamente da linguagem natural para uma prova final, o BRIDGE impõe um fluxo de raciocínio estruturado onde os artefatos se restringem e verificam mutuamente.

2.1 Decomposição de Domínio

• O Domínio do Código: Produz a implementação final em Lean. O BRIDGE compara a geração direta em Lean contra andaimes de raciocínio intermediários.
  • Andaimes Funcionais: Inspirados em OCaml e Haskell, estes incentivam dados imutáveis, correspondência de padrões, recursão estrutural e definições composicionais. Isso alinha-se naturalmente com a teoria de tipos dependentes e a disciplina de terminação do Lean.
  • Andaimes Imperativos: Inspirados em Python e C++, estes incentivam loops e mutação.
  • Insight Chave: O programa intermediário é um andaime de raciocínio, não um artefato fonte certificado. Ele não precisa compilar em sua linguagem fonte; seu propósito é enviesar o modelo para uma estrutura que o Lean possa verificar.
• O Domínio da Especificação: Descreve garantias pretendidas. O BRIDGE utiliza vários estilos de raciocínio (Design por Contrato, Teste Baseado em Propriedades, Desenvolvimento Orientado a Testes, Programação Defensiva) para tornar explícitas suposições, casos de borda e garantias. As especificações são avaliadas não apenas pela verificação de tipos, mas pela não vacuidade e pela sua capacidade de distinguir implementações corretas de plausivelmente incorretas.
• O Domínio do Teorema/Prova: Torna explícitas as afirmações de correção. Os modelos são instruídos a propor propriedades (limites, invariantes, monotonicidade) e tentar provas. Este domínio serve como um diagnóstico para a verificação a jusante, verificando se os teoremas gerados podem ser elaborados e se as provas podem ser concluídas sem sorry (placeholder para objetivos não provados).

2.2 Hipótese de Raciocínio

A hipótese central é que o sucesso da verificação depende da estrutura do raciocínio intermediário. A geração direta força o modelo a recuperar o algoritmo, expressá-lo em Lean, satisfazer restrições de tipos/terminação e inferir especificações simultaneamente. O BRIDGE separa essas pressões. Especificamente, os autores encontram que uma ordenação que começa com geração de código funcional é particularmente eficaz: o modelo primeiro gera código compatível com Lean usando um andaime funcional e, em seguida, usa essa implementação como uma âncora semântica para especificações e declarações de teorema.

3. Contribuições Principais

1. Um Framework de Múltiplos Artefatos: O BRIDGE introduz uma abordagem estruturada para codificação verificável que decompõe a tarefa em domínios interligados de Código, Especificação e Teorema/Prova, usando raciocínio entre artefatos para reduzir a deriva semântica.
2. Raciocínio Funcional Melhora a Síntese: Em um benchmark Lean de 178 problemas, o raciocínio intermediário alinhado funcionalmente melhora a correção executável do Lean em até 1,5× comparado ao prompt direto. Alcança taxas de sucesso comparáveis com aproximadamente 2× menos avaliações em Lean, indicando maior eficiência de amostragem.
3. Artefatos a Jusante Melhorados: O prompt no estilo BRIDGE produz artefatos formais mais úteis. Gera mais declarações de teorema que elaboram com sucesso no Lean e mais tentativas de prova concluídas alinhadas com a implementação. O prompt guiado por especificação também melhora a geração de código convencional (até 17,5 pontos percentuais em Python).
4. Viés Indutivo Aprendível: O Ajuste Fino Supervisionado (SFT) em traços funcionais no estilo BRIDGE supera o ajuste fino de traços diretos correspondentes (por exemplo, um ganho de 9,1 pontos percentuais no benchmark VERINA). Isso sugere que o framework captura um viés indutivo aprendível, em vez de ser um efeito de prompt único.

4. Resultados Experimentais

Os autores avaliaram o BRIDGE em um benchmark Lean personalizado de 178 problemas e em benchmarks públicos, incluindo VERINA, CLEVER e um piloto DAFNYBENCH com suporte de solucionador.

• Correção Executável: Usando andaimes funcionais, a taxa de aprovação no benchmark de 178 tarefas aumentou de 44/178 (Direto) para 59/178 (Funcional) na configuração mínima do núcleo. Com rodadas de reparo, a diferença permaneceu positiva (83/178 vs. 77/178).
• Eficiência de Amostragem: Os andaimes funcionais alcançaram sucesso comparável com aproximadamente metade do número de avaliações em Lean comparado ao prompt direto, reduzindo o custo de verificação de candidatos.
• Transferibilidade: Os benefícios transferiram-se para benchmarks públicos. No VERINA, o prompt funcional melhorou as taxas de aprovação em até 6,3 pontos percentuais. No DAFNYBENCH, melhorou o verified pass@5 em 7,3 pontos percentuais.
• Diagnósticos de Prova: Em um experimento de prova completa, o código funcional produziu mais provas concluídas sem sorry (34/178 vs. 20/178 com provador SFT funcional) e gerou implementações mais curtas e limpas que foram mais fáceis para modelos de prova descarregarem.
• Ganhos de SFT: O ajuste fino em traços funcionais melhorou o desempenho no VERINA de 20,3% para 29,4%, demonstrando que a estrutura de raciocínio pode ser internalizada pelo modelo.

5. Significado e Limitações

O artigo afirma que a representação do raciocínio importa. Ao estruturar o processo de geração para alinhar com o sistema de verificação alvo (Lean), o BRIDGE reduz falhas de sintaxe, tipos e terminação. O framework fornece um viés indutivo orientado à verificação que conecta código, especificações, declarações de teorema e tentativas de prova, tornando o pipeline mais fácil de inspecionar e mais passível de busca de prova a jusante.

Afirmações Modestas e Limitações:

• Não é Verificação Completa: O BRIDGE estuda a "frente" da síntese verificada. Não afirma resolver a verificação semântica completa em escala. Especificações e declarações de teorema geradas podem ainda ser fracas, vacuas ou excessivamente moldadas pela implementação.
• Escopo: A avaliação foca em tarefas locais e algorítmicas. Os autores ainda não testaram o BRIDGE em bibliotecas formais grandes, programas ricos em estado ou provas de longo horizonte.
• Dependência do Modelo: Os resultados variam entre modelos, prompts e orçamentos de busca. O BRIDGE é apresentado como um viés indutivo útil, em vez de uma melhoria universal independente do modelo subjacente.
• Trabalho Futuro: Os autores observam que o próximo passo é fechar o ciclo entre os artefatos do BRIDGE e uma busca de prova mais forte, potencialmente integrando provadores de teoremas que usam ferramentas, recuperação de bibliotecas formais e aprendizado por reforço a partir de recompensas verificáveis.

Em resumo, o BRIDGE demonstra que decompor a codificação verificada em etapas de raciocínio estruturadas e alinhadas ao domínio melhora significativamente a qualidade e a verificabilidade dos artefatos gerados, oferecendo um caminho para uma síntese formal mais confiável sem exigir a automação completa do processo de prova.