Resumo Técnico: Informalização Simbólica

Declaração do Problema

O artigo aborda o desafio da informalização simbólica: a conversão confiável de matemática formal (provas e teoremas verificados por máquina) em linguagem natural fluente sem perda de precisão. Embora os métodos neurais (Modelos de Linguagem de Grande Escala - LLMs) tenham avançado na autoformalização (do informal para o formal), eles sofrem de "alucinações" e não podem garantir que o teorema formalizado corresponda ao texto original. Inversamente, embora os resultados da formalização possam ser automaticamente verificados, o processo inverso — a informalização — é frequentemente difícil de automatizar simbolicamente.

Tentativas anteriores de informalização simbólica foram criticadas por três razões principais, que este artigo identifica como os requisitos essenciais para um sistema bem-sucedido:

1. Fluência: As saídas muitas vezes carecem da diversidade e flexibilidade da linguagem natural, parecendo rígidas.
2. Produtividade: Os sistemas são difíceis de projetar e implementar.
3. Multilinguismo: As abordagens frequentemente falham em escalar entre diferentes linguagens formais ou linguagens naturais.

O artigo argumenta que a informalização não é meramente uma tradução "fácil", mas um problema de pesquisa complexo que exige um equilíbrio entre a correção semântica (preservação do significado) e a completude linguística (cobertura de toda a gama de expressão matemática).

Metodologia: O Sistema Informath

O artigo apresenta o Informath, um sistema construído sobre uma arquitetura interlingual para abordar os três objetivos de fluência, produtividade e multilinguismo.

1. Arquitetura

O Informath utiliza uma abordagem de interlíngua em dois estágios:

• Interlíngua Formal (Dedukti): Serve como um hub entre vários sistemas de prova (Agda, Lean, Rocq). O Dedukti é um framework lógico minimalista com tipos dependentes e regras de reescrita. Ele atua como a fonte da verdade para o conteúdo formal.
• Interlíngua Linguística (Grammatical Framework - GF): Lida com o lado da linguagem natural. O GF é um formalismo gramatical baseado em um framework lógico semelhante ao Dedukti, projetado para tradução multilingue.

O fluxo de trabalho é: Sistema de Prova $\to$ Dedukti $\to$ Sintaxe Abstrata do GF $\to$ Linguagem Natural.

2. Multilinguismo

O multilinguismo é alcançado mapeando a sintaxe abstrata do Dedukti para a sintaxe abstrata do GF, que é então linearizada em linguagens naturais concretas.

• Sintaxe Abstrata Compartilhada: Os conceitos matemáticos centrais são definidos em uma árvore de sintaxe abstrata (AST) independente de linguagem dentro do GF.
• Biblioteca de Gramática de Recursos (RGL): O Informath utiliza a RGL do GF, que fornece estruturas linguísticas pré-definidas (flexão, concordância, regras sintáticas) para aproximadamente 40 idiomas. Isso permite que a mesma sintaxe abstrata seja renderizada corretamente em inglês, francês, alemão, sueco, etc., lidando com variações gramaticais (ex: gênero, caso, número) automaticamente.

3. Produtividade

Para abordar a dificuldade de implementação, o Informath emprega uma pilha de implantação que abstrai a complexidade do GF e do código Haskell para os usuários finais:

• Tabelas de Símbolos (.dkgf): A camada mais alta e acessível. Os usuários definem anotações lexicais que mapeiam constantes do Dedukti para funções ou templates de string do GF. Isso permite que não-linguistas estendam o sistema para novos conceitos matemáticos sem escrever regras gramaticais.
• Paradigmas Inteligentes: A RGL gera tabelas de inflexão a partir de formas de palavras básicas, reduzindo a necessidade de entrada lexical manual.
• Código Modular: O sistema separa o núcleo estável (MathCore, que lida com a correção semântica) das extensões extensíveis (MathExtensions, que lida com a completude linguística).

4. Fluência e Geração de Linguagem Natural (NLG)

Para alcançar a fluência, o Informath vai além das Linguagens Naturais Controladas (CNLs) básicas, implementando um pipeline de NLG de múltiplas etapas:

• Determinação de Conteúdo e Planejamento de Texto: Decidir o que dizer e em qual ordem.
• Agregação: Mesclar fatos atômicos (ex: converter "x é par e x é primo" para "x é par e primo").
• Escolha Lexical: Selecionar palavras apropriadas via tabelas de símbolos.
• Realização de Superfície: Gerar a string final usando a linearização do GF.
• Classificação (Ranking): O sistema gera milhares de variantes de expressões para uma única afirmação formal. Elas são classificadas usando uma função de penalidade baseada no tamanho da árvore, profundidade, contagem de tokens e regras estilísticas (ex: evitar sentenças que começam com símbolos). Isso garante que a saída seja compacta e soe natural.

A gramática é dividida em MathCore (uma CNL mínima cobrindo todos os construtos do Dedukti) e MathExtensions (aproximando a linguagem completa da matemática). O sistema suporta recursos complexos como:

• Constantes de ligação de variáveis: Lidar com quantificadores e integrais via Sintaxe Abstrata de Ordem Superior (HOAS).
• Quantificação in situ: Posicionar quantificadores dentro de predicados (ex: "todo número natural é par").
• Notação Simbólica: Gerar macros LaTeX para partes simbólicas enquanto mantém as partes verbais naturais.

Principais Contribuições

1. O Sistema Informath: Uma implementação funcional demonstrando que a informalização simbólica pode ser fluente, produtiva e multilingue.
2. Arquitetura Interlingual: Um uso inovador do Dedukti e do GF como duplas interlínguas para desacoplar a lógica formal da variação linguística.
3. Extensão de Baixo Código (Low-Code): Um mecanismo baseado em tabela de símbolos que permite aos usuários estender o sistema para novos domínios matemáticos sem modificar o código central da gramática ou do compilador.
4. Tratamento de Ambiguidade: Uma estratégia para gerenciar a ambiguidade inerente à linguagem natural (ex: escopo de quantificadores, conjunções) através da geração de múltiplas variantes e do uso de verificação de tipo ou classificação para resolvê-las, em vez de impor regras rígidas e inequívocas que sacrificam a fluência.

Resultados

O artigo relata o estado atual do Informath:

• Cobertura: O sistema cobre matemática de graduação (aritmética, teoria dos conjuntos, álgebra, topologia) e foi testado no projeto "100 teoremas".
• Saída Multilingue: Ele gera com sucesso textos fluentes em inglês, francês, alemão e sueco a partir da mesma fonte Dedukti.
• Estudos de Caso:
  • Teoria de Tipos Homotópicos (HoTT): Um estudo de caso no livro de HoTT revelou desafios com tradutores de terceiros (Agda para Dedukti) que explodem a complexidade do código devido aos níveis de universo. No entanto, uma vez convertido, o Informath lidou com sucesso com a informalização, incluindo cenários complexos de "proposições como tipos".
  • Dados Sintéticos: O Informath foi usado para gerar dados sintéticos para ajustar finamente um LLM (Qwen2.5-7B-Instruct), resultando em melhor desempenho de autoformalização em comparação com o baseline.
• Limitações: O sistema ainda não é linguisticamente completo (não cobre toda a linguagem comum da matemática) e a informalização de provas continua sendo um trabalho em progresso, particularmente em relação à ordenação e omissão de passos de prova.

Significância e Alegações

O artigo alega que a informalização simbólica é um complemento necessário à autoformalização neural. Enquanto os LLMs podem gerar código formal, eles não podem garantir a correção; a informalização simbólica fornece uma ponte confiável e explicável que permite aos usuários humanos interagir com sistemas formais em linguagem natural sem ver o código subjacente.

Os autores concluem modestamente que, embora o Informath alcance um nível de fluência além das CNLs básicas, a cobertura total da linguagem comum da matemática permanece um objetivo distante. Os principais desafios abertos são a classificação do crescente número de variantes geradas e a informalização de provas. O artigo enfatiza que, ao contrário da formalização, que pode ser automaticamente verificada, a informalização exige confiabilidade inerente e conhecimento especializado, tornando o desenvolvimento dessas ferramentas um esforço significativo, mas necessário, para o futuro da matemática verificável por máquina e legível por humanos.