Resumo Técnico: Visored: Um Provador de Linguagem Natural Controlada para Matemática Gerada por LLM

Declaração do Problema

Os Grandes Modelos de Linguagem (LLMs) têm demonstrado uma capacidade crescente em raciocínio matemático, mas permanecem propensos a alucinações. Consequentemente, provas geradas por IA são tão confiáveis quanto o processo de verificação. Embora provadores de teoremas automatizados (ATPs) e modelos de prova completa (por exemplo, aqueles que visam Lean ou Rocq) tenham alcançado altas taxas de aprovação em benchmarks como o miniF2F, eles tipicamente requerem um enunciado já formalizado como entrada. O gargalo crítico reside na autoformalização: a tradução da prosa matemática informal em uma forma verificável por máquina.

Esta tradução não é trivial porque a matemática informal depende de um contexto compartilhado, condições laterais implícitas (ex: $x \neq 0$) e abusos de notação que os leitores preenchem automaticamente. Uma tradução direta para uma linguagem formal exige comprometer-se com bibliotecas específicas de lemas, subtipos, convenções de casos de borda e coerções (ex: $\mathbb{N}$ vs. $\mathbb{Z}$ vs. $\mathbb{R}$) que não deixam rastro no texto de origem. Erros nessas decisões raramente se manifestam como erros de compilação, mas sim como "deriva semântica silenciosa", onde um enunciado compila, mas não reflete mais a intenção original.

Metodologia

Visored é um protótipo de pesquisa projetado para preencher a lacuna entre a escrita matemática informal e a verificação formal, introduzindo uma representação intermediária (IR) de tipos dependentes que se situa entre o LaTeX e provadores de baixo nível como o Lean.

Arquitetura Central

O sistema opera como um pipeline (Figura 2 no artigo) consistindo nas seguintes etapas:

1. Entrada de Linguagem Natural Controlada (CNL): O Visored aceita um subconj conjunto controlado de inglês matemático incorporado em LaTeX. O vocabulário (templates de sentenças como "Seja...", "Assuma...", "Então..." e comandos LaTeX) é definido por arquivos de especificação .lpcsv externos, permitindo que a linguagem de superfície seja estendida sem modificar o parser.
2. Sintaxe e Semântica: A entrada é analisada em uma árvore sintática e, em seguida, elaborada em uma AST tipada (sem AST). Esta etapa resolve nomes, atribui tipos e classes, e impõe a bem-definibilidade no momento da verificação de tipos. Seguindo a tradição do PVS, funções parciais (ex: $1/x$, $\sqrt{x}$, $\log x$) carregam argumentos de hipótese implícitos (ex: $x \neq 0$, $x \ge 0$) que devem ser liquidados antes que a expressão seja aceita.
3. IR de Médio Nível (MIR): A AST tipada é reduzida para o Visored MIR, o substrato para o solver.
4. Solver com Limite de Custo: O solver liquida as obrigações de "Então..." e as condições de bem-definibilidade usando um mecanismo orientado por regras e com limite de custo (chamado "Miracle"). Ele emprega um banco de dados de regras de retrocesso (backward) e avanço (forward) (inspirado no ProofGrader) e táticas especializadas (ex: normalizadores algébricos, solvers de cadeia) para fechar passos rotineiros que matemáticos tipicamente omitem.
5. Emissão Opcional de Lean: Provas aceitas podem ser transpiladas para Lean 4. A transpilação envolve o reprocessamento do histórico de normalização e o gerenciamento de testemunhas de coerção entre sistemas numéricos.

Filosofia de Design

O Visored é construído sobre duas observações primárias:

1. Fluência de LLM: Os LLMs são treinados predominantemente em matemática informal. Uma superfície de CNL permanece próxima ao domínio onde os LLMs já são fluentes, evitando a necessidade de o modelo aprender sintaxe de provador de baixo nível (táticas, nomes de lemas de biblioteca) do zero.
2. Tratabilidade: Unir o raciocínio natural e o formal é mais tratável do que a prova automática de teoremas completa. Ao fazer com que o LLM forneça o esboço da prova em CNL, o solver só precisa fechar pequenos passos óbvios, uma tarefa perfeitamente ao alcance da engenharia de agentes moderna.

O sistema trata a análise semântica ascendente (LaTeX $\to$ Visored) como o problema difícil, tratado pelo LLM, enquanto a projeção descendente (Visored $\to$ Lean) é um processo determinístico e mecânico.

Principais Contribuições

• IR de Tipo Dependente para Autoformalização: O Visored introduz uma IR semanticamente rica onde cada decisão sem rastro de superfície no LaTeX (subtipos, lemas de biblioteca, convenções de casos de borda, casts) é tornada explícita.
• Extensibilidade Baseada em Especificação: A superfície de CNL é definida por arquivos de configuração externos em vez de parsers codificados, permitindo que o vocabulário seja ajustado para convenções matemáticas específicas (livro didático, competição, pesquisa) sem recompilar o sistema.
• Diagnósticos Localizados: Diferente de sistemas que fornecem um único veredito de aceitação/rejeição após uma compilação completa do Lean, o Visored fornece diagnósticos localizados na etapa de elaboração ou resolução. Isso permite um loop de "verificar-e-revisar" onde um LLM pode identificar e corrigir erros específicos.
• Imposição de Bem-Definibilidade: O sistema impõe a bem-definibilidade (ex: garantindo que $x \neq 0$ antes de $1/x$) via argumentos de hipótese implícitos liquidados pelo solver, em vez de depender das convenções de totalização do provador alvo.
• Integração de Escolas Existentes: O Visored sintetiza elementos de Mizar/Naproche (superfície CNL), PVS (bem-definibilidade no tempo de verificação de tipos), Lean/Rocq (tipos dependentes) e ProofGrader (resolução baseada em regras com orçamento de custo) em um único pipeline voltado para LLM.

Resultados Experimentais

Os autores relatam um estudo de cobertura no split miniF2F-valid (244 problemas), que serviu tanto como conjunto de desenvolvimento quanto de avaliação.

• Desempenho: Um agente de codificação de LLM (Claude), guiado por um documento de habilidades descrevendo a superfície de CNL, produziu provas verificadas pelo Visored para 222 de 244 problemas (91%).
• Detalhamento:
  • Indução: 100% (8/8)
  • Álgebra: 98% (86/88)
  • Teoria dos Números: 97% (66/68)
  • AMC/AIME: 93% / 87%
  • IMO (Olimpíada): 35% (7/20)
• Análise de Falha: Os problemas não resolvidos foram atribuídos a lacunas no banco de regras do Visored (ex: ausência da desigualdade AM-GM, falta de tipos de campos finitos, identidades trigonométricas) ou regressões no protótipo, e não à incapacidade do LLM de encontrar a estratégia da prova. Os autores afirmam explicitamente que o agente falhou em resolver esses problemas porque a "maquinaria" necessária ainda não foi implementada no sistema.
• Custo de Transpilação: O esquema de emissão esparsa atual resulta em uma saída Lean altamente verbosa, com uma razão mediana de contagem de linhas de $\approx 250\times$ comparada a provas de Lean escritas à mão, atingindo uma cauda de $\approx 25.000\times$. Isso se deve ao reprocessamento dos passos de normalização e testemunhas de coerção.

Significância e Alegações

O artigo posiciona o Visored não como um provador de teoremas automatizado competitivo, mas como uma prova de conceito para uma nova infraestrutura para verificar e organizar a matemática informal produzida por IA.

• Alegações Modestas: Os autores explicitamente declaram que não reivindicam prova automática de teoremas competitiva, nem extrapolam resultados para divisões de teste não utilizadas. A cobertura de 91% é apresentada como um limite inferior do que o design pode expressar, não como uma taxa de aprovação ajustada.
• Mudança no Gargalo: O trabalho apoia a visão de que a restrição vinculante na matemática de IA está mudando de "gerar ideias" para "verificar e organizá-las em escala".
• Modos de Utilidade: O Visored é projetado para funcionar em quatro modos:
  1. Verificador em tempo de inferência: Um verificador em tempo real para saídas de LLM.
  2. Loop de autoformalização: Um mecanismo para LLMs reescreverem provas baseadas em diagnósticos localizados.
  3. Sinal de recompensa denso: Fornecendo feedback por passo para Aprendizado por Reforço (RL).
  4. Gerador de dados CNL: Criando um corpus renovável de provas de leitura natural e formalmente verificadas.

O artigo conclui que a combinação de uma superfície de CNL, uma IR de tipo dependente e um solver baseado em regras cria um pipeline onde as falhas são localizadas e acionáveis, oferecendo uma rota mais confiável da prosa informal para provas verificadas pelo kernel do que as abordagens atuais de autoformalização direta. Os problemas não resolvidos representam um backlog de regras e maquinária ausentes, não uma limitação fundamental do design.