🤖 AI

When Agda met Vampire

Este artigo apresenta uma integração simples e correta entre o assistente de provas Agda e o provador automático Vampire, permitindo que este último resolva obrigações de prova em lógica clássica e as traduza de volta para termos construtivos, automatizando assim demonstrações complexas que anteriormente exigiam dias de trabalho manual.

Autores originais: Artjoms Šinkarovs, Michael Rawson

Publicado 2026-02-24

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Artjoms Šinkarovs, Michael Rawson

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ê tem dois especialistas muito diferentes trabalhando no mesmo projeto de construção de um edifício complexo (que, neste caso, é um software matemático perfeito e livre de erros).

O primeiro especialista é o Agda. Ele é um arquiteto extremamente rigoroso, meticuloso e um pouco "chato". Ele só aceita construções que sigam regras estritas de lógica construtiva. Se você pedir para ele construir uma parede, ele exige que você mostre exatamente cada tijolo e como ele se encaixa. Ele não aceita atalhos. Se algo não for provado passo a passo, ele diz: "Não, isso não é seguro". O problema é que, para tarefas simples e repetitivas (como provar que dois tijolos são iguais), o Agda exige que o humano faça todo o trabalho manual, o que é cansativo e demorado.

O segundo especialista é o Vampire. Ele é um detetive super-rápido e agressivo, especialista em lógica clássica. Ele não se importa com os detalhes minuciosos de como você chegou à conclusão, desde que a conclusão seja verdadeira. Ele usa "atalhos" e regras de inferência que o Agda acharia suspeitas. O Vampire é incrivelmente rápido em resolver quebra-cabeças complexos, mas ele não sabe falar a língua do Agda. Se você pedir algo para ele, ele responde em um dialeto que o Agda não entende.

O Problema: Dois Mundos que não se Falam

A equipe de pesquisadores (Artjoms e Michael) percebeu que estava perdendo muito tempo fazendo o Agda provar coisas que o Vampire poderia resolver em um piscar de olhos. Mas eles não podiam simplesmente deixar o Vampire construir o prédio, porque o Agda não aceitaria o trabalho dele (seria como usar cimento de uma marca que o engenheiro chefe não confia).

A solução deles foi criar um tradutor mágico (uma ponte) entre os dois.

A Solução: A Ponte de Tradução

O papel descreve como eles criaram um sistema onde:

O Agda pede ajuda: Quando o Agda fica preso em uma tarefa chata, ele usa um recurso especial (chamado "reflexão") para olhar para o problema, transformá-lo em uma linguagem simples e padrão (como um "inglês básico" da lógica) e enviar para o Vampire.
O Vampire resolve: O Vampire pega esse problema, corre muito rápido e encontra a solução. Ele devolve uma prova longa e complexa, cheia de passos lógicos.
O Tradutor (Prolog) atua: Aqui entra a mágica. Eles usaram uma linguagem de programação chamada Prolog (que é ótima em seguir regras e encontrar caminhos) como um tradutor.
- O Prolog pega a prova "agressiva" do Vampire.
- Ele remove as partes que o Agda não gosta (como negações duplas ou suposições de que o mundo não está vazio).
- Ele reescreve a prova, tijolo por tijolo, transformando-a em uma prova "construtiva" e segura que o Agda adora.
O Agda aprova: O Agda recebe a prova reescrita, verifica cada passo, vê que tudo está dentro das regras e diz: "Ok, isso é válido!".

A Analogia da Receita de Bolo

Pense no Agda como um chef que exige que você liste cada ingrediente e cada movimento exato da mão para provar que o bolo ficou bom.
O Vampire é um cozinheiro que prova o bolo, diz "está perfeito" e vai embora, sem dar a receita.

O sistema deles funciona assim:

O Chef (Agda) diz: "Preciso provar que este bolo está bom, mas não tenho tempo de escrever a receita agora."
Ele manda a descrição do bolo para o Cozinheiro Rápido (Vampire).
O Cozinheiro Rápido prova o bolo e grita: "Está perfeito! Usei farinha, ovos e açúcar!" (mas de um jeito que o Chef não entende).
Um Tradutor pega o grito do Cozinheiro, traduz para a linguagem do Chef e escreve a receita completa, passo a passo, garantindo que todos os ingredientes estejam lá.
O Chef lê a receita traduzida, confirma que está tudo certo e assina o documento.

O Resultado na Prática

Os autores testaram isso em um projeto real: provar propriedades matemáticas complexas sobre números complexos e raízes de unidade (essenciais para algoritmos de processamento de sinais, como o FFT).

Sem a ferramenta: Um desenvolvedor experiente levou dois dias inteiros para provar essas coisas manualmente no Agda.
Com a ferramenta: O sistema fez tudo automaticamente em uma fração de segundo.

Por que isso é importante?

A grande sacada deste trabalho é que eles não precisaram reescrever o Agda nem o Vampire. Eles apenas construíram uma "ponte" simples entre eles.

O Agda continua sendo o guardião da segurança (ninguém precisa confiar no Vampire cegamente, pois o Agda verifica a prova final).
O Vampire continua sendo o motor de velocidade.
O esforço de engenharia foi pequeno, mas o ganho de produtividade foi enorme.

Em resumo, eles mostraram que, ao encontrar um "dialeto comum" simples entre duas linguagens complexas, é possível fazer a máquina trabalhar muito mais rápido, liberando os humanos para fazerem o que realmente importa: pensar em ideias criativas, em vez de perder tempo com tarefas repetitivas.

Título: Quando Agda encontrou o Vampire

Autores: Artjoms Šinkarovs e Michael Rawson (Universidade de Southampton, Reino Unido)

1. O Problema

Os assistentes de prova baseados em tipos dependentes (como Agda, Lean e Rocq) fornecem fundamentos expressivos para matemática mecanizada e software verificado. No entanto, a automação nesses sistemas enfrenta dois desafios principais:

Carga de Trabalho Manual: Muitas obrigações de prova são rotineiras (ex: isomorfismos, propriedades simples de codificação), mas exigem esforço manual intensivo, desviando o foco de insights matemáticos profundos.
Divergência Lógica: A maioria dos Provedores de Teoremas Automatizados (ATPs) opera em Lógica de Primeira Ordem Clássica, enquanto os assistentes de prova baseados em tipos dependem da Teoria de Tipos Construtiva.
- ATPs clássicos não possuem termos de prova verificáveis internamente pelo assistente.
- A reconstrução de provas clássicas em termos construtivos é complexa e muitas vezes falha em sistemas dependentes, diferentemente do que ocorre em sistemas como Isabelle/HOL (onde o Sledgehammer funciona bem devido à similaridade lógica).

O objetivo do artigo é integrar assistentes de prova e ATPs de forma leve, preservando as garantias de correção do assistente, sem exigir modificações invasivas em nenhum dos sistemas.

2. Metodologia

Os autores propõem uma integração leve baseada na identificação de um fragmento expressivo comum entre a lógica de tipos dependentes e a lógica de primeira ordem: o fragmento Horn equacional.

O fluxo de trabalho (round-trip) funciona da seguinte maneira:

Reflexão e Extração (Agda):
- Utiliza-se o mecanismo de reflexão do Agda para extrair o objetivo atual (o "hole") e o ambiente (lemas e definições).
- Macros convertem definições Agda (tipos de dados indutivos, funções por padrões, teoremas) para o formato SMT-LIB, que o Vampire pode entender.
- Restrições: O fragmento suporta tipos de dados indutivos simples (sem parâmetros/índices complexos), funções não-dependentes e igualdade proposicional.
Prova Automatizada (Vampire):
- O problema traduzido é enviado ao Vampire, um ATP de ponta baseado no cálculo de superposição.
- O Vampire tenta refutar a negação do objetivo (prova por refutação), gerando uma prova clássica em forma de cláusulas (formato TSTP).
Transformação da Prova (Conversão Clássica para Construtiva):
- Observação Chave: O cálculo de superposição do Vampire, quando aplicado a cláusulas Horn, é construtivamente válido.
- Técnica de Friedman/A-translation: O sistema transforma a prova de refutação ( $\Gamma, \neg G \vdash \bot$ ) em uma prova direta ( $\Gamma \vdash G$ ). Isso é feito substituindo sistematicamente o $\bot$ (falso) na prova pelo objetivo $G$ . Como $G \to G$ é uma tautologia, a prova resultante é válida no Agda.
Reconstrução (Prolog):
- Um script em Prolog lê a prova TSTP do Vampire.
- O Prolog realiza uma busca com retrocesso (backtracking) para mapear cada passo de inferência do Vampire (Resolução, Fatoração, Superposição) para um termo de prova correspondente no Agda.
- O script lida com renomeação de variáveis e simetria de igualdade.
- O termo de prova reconstruído é emitido como código Agda.
Verificação:
- O Agda verifica o tipo do termo reconstruído. Se passar, a prova é aceita como correta e segura, sem depender da confiança no Vampire.

3. Contribuições Principais

Fragmento Horn Equacional: Identificação de uma sub-linguagem que permite traduções bidirecionais simples e seguras entre tipos dependentes e lógica de primeira ordem.
Integração Leve via Reflexão: Demonstração de que é possível integrar ATPs sem modificar o núcleo do assistente de prova (Agda), usando apenas suas facilidades de reflexão.
Mecanismo de Reconstrução em Prolog: Desenvolvimento de um motor de reconstrução conciso (menos de 500 linhas de código) que traduz provas de ATPs para termos construtivos, explorando a semântica natural do Prolog para lidar com unificação e renomeação.
Validação Prática: O sistema foi testado em um caso real de pesquisa envolvendo a formalização de raízes da unidade em um corpo complexo, um problema que anteriormente exigia dois dias de trabalho de um especialista em Agda.

4. Resultados

Caso de Estudo (Raízes da Unidade): O sistema automatizou a prova de 12 teoremas (8 sobre propriedades de anéis e 4 sobre raízes da unidade) necessários para verificar uma representação de números complexos em Agda.
- Tempo: As provas foram geradas automaticamente em frações de segundo.
- Comparação: O que exigia dois dias de trabalho manual foi resolvido instantaneamente.
- Qualidade: As provas geradas, embora verbosas (cerca de 300 linhas de código Agda para algumas), são corretas e verificadas pelo tipo-checker do Agda.
Eficiência: O uso de portfólios de estratégias do Vampire (CASC) mostrou-se altamente eficaz para problemas de Agda, mesmo sem um seletor de premissas sofisticado.

5. Significado e Implicações

Viabilidade da "Hammer" em Tipos Dependentes: O trabalho prova que a abordagem de "martelo" (usar ATPs externos para encontrar provas e reconstruí-las internamente) é viável para sistemas de tipos dependentes, superando a barreira da lógica clássica vs. construtiva.
Baixo Custo de Engenharia: A solução não requer modificações profundas no Agda ou no Vampire, tornando-a fácil de manter e adaptar para outros assistentes (como Lean ou Idris) ou outros ATPs (como E ou Zipperposition).
Futuro: Os autores sugerem que o fragmento pode ser expandido para incluir lógica clausal completa (usando representações de dupla negação), tipos parametrizados e famílias indexadas, aproximando-se ainda mais da automação total em assistentes de prova modernos.

Em resumo, o artigo apresenta uma ponte robusta entre a verificação formal rigorosa e a potência da prova automática, demonstrando que a automação pode ser integrada de forma segura e eficiente em sistemas de tipos dependentes complexos.