💻 computer science

ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers

Este artigo apresenta o ITPEval, o primeiro benchmark e infraestrutura unificada para avaliar a tradução automatizada de provas formais entre quatro grandes provadores de teoremas interativos, revelando que os modelos de linguagem de grande escala atuais enfrentam dificuldades significativas com a tradução de provas devido a incompatibilidades de bibliotecas e que a verificação de tipos nativa, por si só, frequentemente superestima a fidelidade semântica.

Autores originais: Jiayi Wu, Robert Joseph George, Anima Anandkumar

Publicado 2026-07-23

📖 3 min de leitura☕ Leitura rápida

CC BY 4.0

Autores originais: Jiayi Wu, Robert Joseph George, Anima Anandkumar

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 um mundo onde matemáticos falam quatro idiomas diferentes, mas todos estão tentando resolver exatamente os mesmos quebra-cabeças. Na arena de alto risco da "prova de teoremas formais", computadores atuam como os árbitros definitivos, verificando cada passo de uma prova matemática para garantir que seja 100% correta. No entanto, assim como humanos que falam francês, japonês, suaíli e árabe, esses sistemas de computador (chamados de Provadores de Teoremas Interativos, ou ITPs) têm sua própria gramática, vocabulário e bibliotecas de fatos pré-aprovados. Uma prova escrita perfeitamente em um sistema é frequentemente um emaranhado de palavras sem sentido para os outros. Isso cria um problema solitário: se uma prova brilhante é escrita em uma linguagem, ela não pode ser facilmente usada ou verificada pelos outros. Cientistas têm tentado construir "tradutores universais" para preencher essa lacuna, esperando que a Inteligência Artificial (IA) pudesse aprender a traduzir essas provas matemáticas automaticamente, permitindo que toda a comunidade compartilhe seu trabalho.

Apresentamos o ITPEVAL, um novo estudo que atua como um exame de idiomas massivo e rigoroso para a IA. Os pesquisadores queriam ver se os modelos de IA mais inteligentes de hoje conseguiriam realmente traduzir provas matemáticas formais entre quatro sistemas principais: Lean 4, Rocq, Isabelle e HOL Light. Eles não apenas pediram para a IA adivinhar; eles construíram um campo de testes especializado com mais de 1.500 arquivos de origem e quase 7.000 teoremas. Eles dividiram o teste em dois níveis: um nível "Controlado", com problemas matemáticos simples e autossuficientes (como um teste de vocabulário sem referências externas), e um nível "Ecossistema", usando código de biblioteca real e complexo que depende de regras específicas do sistema (como uma conversa completa com gírias e referências culturais).

Os resultados foram uma mistura de "nada mal" e "ainda muito difícil". Quando a IA tentava traduzir apenas os enunciados dos teoremas (o "quê"), os melhores modelos acertaram cerca de 29,1%. Mas quando solicitada a traduzir as provas propriamente ditas (o "como"), a taxa de sucesso despencou para apenas 10,5%. O estudo descobriu que o maior obstáculo não era a matemática em si ou as diferentes fundações lógicas; era o "ecossistema". A IA teve mais dificuldade quando precisava navegar pelas bibliotecas específicas, convenções de nomenclatura e estilos de automação do sistema de destino. É como se a IA pudesse entender a frase "O gato sentou no tapete", mas falhasse ao ser solicitada a traduzi-la para um dialeto específico que exigisse o uso de uma marca específica de tapete e um tipo específico de gato.

Além disso, os pesquisadores descobriram que simplesmente fazer um computador dizer "Isso parece correto" (uma verificação de tipo) não é suficiente. Eles realizaram uma "verificação de significado" mais profunda e descobriram que, mesmo quando a tradução da IA passava no teste básico do computador, ela era frequentemente matematicamente mais fraca ou ligeiramente diferente do original em 46% dos casos. O estudo sugere que, embora a IA esteja melhorando nos fundamentos, ela ainda precisa aprender a se adaptar à "cultura" única de cada sistema matemático antes que possa ser verdadeiramente um tradutor universal. Os autores também exploraram um teste de "ida e volta", onde traduziram matemática para linguagem natural e vice-versa, descobrindo que os resultados variavam drasticamente dependendo de qual sistema era usado, sugerindo que usar múltiplos sistemas juntos pode ajudar, mas ainda não é uma solução mágica.

Resumo Técnico: ITPEVAL – Benchmarking de Tradução Formal entre Provadores de Teoremas Interativos

1. Declaração do Problema

O ecossistema de prova formal de teoremas é atualmente fragmentado. Embora os grandes modelos de linguagem (LLMs) tenham alcançado um sucesso significativo na prova automática de teoremas e na autoformalização, os resultados verificados permanecem isolados em Provadores de Teoremas Interativos (ITPs) incompatíveis. Cada sistema (por exemplo, Lean 4, Rocq, Isabelle, HOL Light) implementa sua própria fundação lógica, linguagem de táticas e bibliotecas matemáticas. Consequentemente, um teorema provado em um sistema não pode ser invocado diretamente em outro, levando à duplicação de esforços de formalização e limitando os dados de treinamento disponíveis para provadores baseados em aprendizado.

A tradução entre ITPs — a tarefa de converter provas formais entre sistemas preservando a correção — recebeu pouco estudo sistemático. Esforços existentes, como os catálogos "Formalizing 100 Theorems" ou frameworks de interoperabilidade como o Dedukti, focam em rastrear a cobertura ou permitir a troca de provas via representações intermediárias, mas carecem de benchmarks padronizados para avaliar a qualidade da tradução. Além disso, as metodologias de avaliação existentes são insuficientes; a simples verificação de tipos frequentemente gera altas taxas de falsos positivos para correção semântica, e os benchmarks de tradução de código não consideram as profundas diferenças de fundação lógica inerentes aos ITPs.

2. Metodologia e Design do Benchmark

Os autores apresentam o ITPEVAL, o primeiro benchmark projetado para avaliar a tradução automática de provas formais entre quatro dos principais ITPs: Lean 4, Rocq (anteriormente Coq), Isabelle e HOL Light. O benchmark abrange duas fundações lógicas distintas: o Cálculo de Construções Indutivas (CIC) e a Lógica de Ordem Superior (HOL).

2.1. Estrutura de Dados

O benchmark compreende 1.560 arquivos de origem e 6.848 teoremas, organizados em dois níveis distintos para isolar fontes de dificuldade:

Nível A (Controlado): Contém 64 arquivos auto-contidos e axiomatizados (660 lemas) derivados do benchmark Babel-formal. Estes arquivos incluem suas próprias definições e suposições, evitando dependência de bibliotecas específicas de cada provador. Este nível isola questões fundamentais de tradução (ex: teoria de tipos, níveis de universo, argumentos implícitos).
Nível B (Ecossistema): Contém formalizações extraídas de bibliotecas reais da comunidade, expondo desalinhamentos de API, convenções de nomenclatura e diferenças de estilo de prova. Este nível inclui:
- 232 arquivos de Formalizing 100 Theorems (4.924 lemas), alinhados entre todos os quatro sistemas.
- 1.264 arquivos de teorema único do miniF2F (apenas enunciados), fornecendo conteúdo diversificado de matemática competitiva.

O design impõe um requisito de interseção de quatro vias: cada arquivo deve ser formalizado em todos os quatro ITPs para garantir comparações direcionais limpas sem confusões por falta de dados.

2.2. Tarefas de Tradução

O ITPEVAL avalia duas tarefas primárias:

Tradução de Enunciado (Statement Translation): Gerar o código do ITP de destino onde os corpos das provas são substituídos por placeholders (ex: sorry). A verificação exige que o arquivo gerado passe na verificação de tipos no sistema de destino.
Tradução de Prova (Proof Translation): Gerar arquivos de prova completos e compiláveis sem placeholders. A verificação exige que o arquivo inteiro compile com sucesso no provador de destino.

2.3. Infraestrutura de Verificação

Um componente crítico da metodologia é o itpeval, uma infraestrutura de verificação unificada multi-ITP. Para lidar com a heterogeneidade dos modelos de execução dos ITPs (ex: altos custos de inicialização para Isabelle e HOL Light), o sistema emprega:

Backends quentes isolados por estado: Garantindo que cada verificação seja observacionalmente equivalente à verificação de um artefato em um ambiente novo, evitando vazamento de declarações.
Verificação nativa do provador de destino: Todos os rótulos são produzidos pelos próprios ITPs de destino, não por heurísticas superficiais.
Escalonamento adaptativo: Utilizando workers persistentes, agrupamento de sessões e servidores de fork para gerenciar o rendimento enquanto preserva a semântica de verificação por arquivo.

2.4. Verificação de Equivalência Semântica

Reconhecendo que a verificação de tipos é necessária, mas insuficiente para a fidelidade semântica, os autores implementam uma verificação de Equivalência Definicional Estendida Bidirecional (BEq) para alvos Lean 4. Esta verificação determinística verifica se um enunciado $G$ e um enunciado de referência $R$ se implicam mutuamente ( $G \vdash R$ e $R \vdash G$ ) usando busca de prova restrita, evitando variância adicional dependente de modelo.

3. Principais Contribuições

Benchmark Alinhado de Quatro Vias: Um conjunto de dados de 1.560 arquivos e 6.848 teoremas através de Lean 4, Rocq, Isabelle e HOL Light, estruturado em níveis controlados e de ecossistema para quantificar o custo das dependências de biblioteca.
Infraestrutura de Verificação Unificada: Um cliente isolado por estado (itpeval) que permite a avaliação escalável e reprodutível entre ITPs heterogêneos com semântica de verificação nativa.
Avaliação Sistemática de LLMs: Uma avaliação de cinco modelos de fronteira e de pesos abertos (GPT-5.5, Claude Sonnet 4.6, Gemini 3.1 Pro, DeepSeek-V4-Pro, Qwen3-235B-A22B) em 12 pares de tradução direcionados.
Análise de Fidelidade Semântica: A aplicação de BEq para demonstrar que a verificação de tipos nativa sozinha pode superestimar substancialmente a correção semântica.
Estudo Exploratório de Ida e Volta (Round-Trip): Uma investigação sobre loops de autoformalização e auto-informalização para avaliar padrões de verificação dependentes do alvo e os benefícios potenciais do contexto multi-ITP.

4. Resultados

4.1. Desempenho de Tradução

Tradução de Enunciado: O modelo com melhor desempenho, GPT-5.5, alcançou uma taxa pass@1 de 29,1% no total. O DeepSeek-V4-Pro seguiu com 27,1%. O desempenho caiu significativamente para outros modelos (Gemini em 14,0%, Qwen e Claude abaixo de 10%).
Tradução de Prova: O desempenho foi substancialmente inferior, com o GPT-5.5 alcançando apenas 10,5% de pass@1 no total.
Lacuna de Níveis (Tier Gap): O nível controlado (Tier A) foi consistentemente mais fácil que o nível de ecossistema (Tier B). Para tradução de prova, o GPT-5.5 atingiu 29,7% em arquivos controlados, mas apenas 5,2% em arquivos de ecossistema. Isso indica que o desalinhamento de biblioteca (APIs, nomenclatura, automação) é a maior fonte observada de falha, em vez das diferenças de fundação lógica.
Assimetria Direcional: A dificuldade de tradução varia significativamente conforme o alvo. Isabelle e HOL Light são alvos fortes para tradução de enunciado, mas Isabelle torna-se o alvo mais difícil para tradução de prova. A similaridade da fundação lógica (ex: CIC para CIC) não garante taxas de sucesso mais altas; as convenções do ecossistema de destino desempenham um papel maior.

4.2. Equivalência Semântica (BEq)

Ao aplicar a verificação BEq aos enunciados Lean 4 verificados do miniF2F:

Apenas 54,0% das traduções verificadas passaram na verificação de equivalência.
O Claude Sonnet 4.6 apresentou a maior taxa de passagem BEq (83,8%) entre as traduções verificadas, enquanto os outros variaram entre 34,5% e 48,4%.
Este resultado demonstra que um enunciado pode ser sintaticamente válido (passar na verificação de tipos), mas semanticamente mais fraco ou deslocado em relação ao teorema original.

4.3. Ida e Volta (Round-Trip) e Autoformalização

Em um estudo de ida e volta multi-ITP (NL $\to$ Formal $\to$ NL $\to$ Formal), o Rocq e o HOL Light verificaram aproximadamente um terço das saídas em ambos os passos de formalização, enquanto o Lean 4 ficou próximo de 11% e o Isabelle caiu para 4,3% no passo final. O contexto multi-ITP mostrou benefícios potenciais para combinações específicas de modelo-alvo (ex: melhorando as taxas de pass-1 do passo 1 do Lean 4 de 4,8% para 10,6%), mas os resultados não foram uniformes em todos os sistemas.

5. Significância e Alegações

O artigo afirma que o ITPEVAL fornece o primeiro benchmark sistemático de quatro vias para tradução formal, revelando que a principal barreira para a tradução entre ITPs não é a fundação lógica em si, mas as dependências de nível de ecossistema (bibliotecas, APIs e idiomatismos de prova).

Os autores enfatizam que:

A verificação nativa é essencial: Heurísticas de superfície ou apenas a verificação de tipos são insuficientes para avaliar a fidelidade semântica.
A infraestrutura importa: A avaliação confiável entre ITPs requer verificação isolada por estado para evitar fatores de confusão como o vazamento de declarações.
Direções futuras: O campo deve priorizar a recuperação, o mapeamento de bibliotecas e o alinhamento de APIs em vez de apenas a tradução fundamental. O artigo também nota limitações, incluindo o cenário de avaliação zero-shot, a restrição do BEq aos alvos Lean 4 e o potencial de contaminação de dados de treinamento em datasets públicos como o miniF2F.

O trabalho estabelece uma base para medir o progresso na tradução formal, sugerindo que sistemas futuros devem abordar o problema do "desalinhamento de biblioteca" para alcançar uma interoperabilidade robusta entre os ecossistemas de provas formais.