A Neuro-Symbolic Approach for Reliable Proof Generation with LLMs: A Case Study in Euclidean Geometry

O artigo propõe uma abordagem neuro-simbólica que combina a recuperação de problemas análogos e a verificação formal com feedback para superar as limitações de raciocínio lógico dos LLMs, demonstrando melhorias significativas na precisão da geração de provas em geometria euclidiana.

O essencial

Imagine que você pediu para um aluno muito inteligente, mas um pouco "sonhador", resolver um problema de matemática difícil. Ele sabe a resposta certa, mas quando tenta escrever o passo a passo (a prova), ele comete erros de lógica, esquece uma regra ou inventa uma justificativa que não existe. Isso é o que acontece com os grandes modelos de linguagem (LLMs) atuais: eles são ótimos em escrever textos que parecem verdadeiros, mas falham quando precisam ser rigorosamente lógicos, como em provas matemáticas.

Este artigo apresenta uma solução inteligente para esse problema, chamando-a de Abordagem Neuro-Simbólica. Pense nela como um sistema de "Tutor + Chefe de Controle de Qualidade".

Aqui está como funciona, explicado de forma simples:

1. O Problema: O "Sonhador" vs. A "Lógica Rígida"

Os modelos de IA atuais funcionam como um escritor criativo que prevê a próxima palavra baseada em padrões. Em matemática, isso é perigoso. Se você pede para provar algo em geometria, o modelo pode "alucinar" um passo que parece plausível, mas que viola as regras da lógica. É como tentar construir uma ponte apenas olhando para fotos de pontes bonitas, sem saber de física ou engenharia.

2. A Solução: O Sistema de Dupla Ação

Os autores criaram um sistema que ajuda a IA a pensar de forma mais estruturada, usando duas ferramentas principais:

A. O "Tutor de Exemplos" (Analogia)

Imagine que você precisa resolver um problema de geometria novo. Em vez de tentar adivinhar do zero, o sistema olha para um banco de dados de milhares de problemas antigos e diz:

"Ei, este problema novo é muito parecido com aquele que você já viu lá atrás! Olha como foi resolvido aquele outro..."

O sistema pega problemas estruturalmente semelhantes (mesmo que os nomes das linhas ou os números sejam diferentes) e mostra a prova correta daquele problema antigo para a IA.

• A Analogia: É como se você estivesse aprendendo a cozinhar um prato novo. Em vez de inventar a receita, você olha para um prato parecido que você já fez com sucesso e usa aquela receita como guia. Isso ajuda a IA a não se perder e a usar as "ferramentas" (teoremas) corretas desde o início.

B. O "Chefe de Controle de Qualidade" (Verificador Simbólico)

Depois que a IA escreve a prova, ela não é enviada diretamente. Ela passa por um "inspetor" rigoroso.

• Como funciona: Este inspetor não é uma IA criativa; é um software matemático puro e duro (um verificador simbólico). Ele lê a prova linha por linha e pergunta: "Isso segue as regras? A conclusão realmente deriva das premissas?"
• O Feedback: Se a IA errar, o inspetor não apenas diz "está errado". Ele aponta exatamente onde: "Você usou o teorema X, mas não provou que as condições para usá-lo foram atendidas."
• O Ciclo: A IA recebe essa crítica, corrige o erro e tenta de novo. Esse ciclo se repete até que a prova esteja perfeita ou o sistema desista.
• A Analogia: É como um programador escrevendo código. Ele escreve, o computador diz "erro na linha 10", ele corrige, o computador diz "erro na linha 12", e ele corrige novamente, até o programa rodar sem erros.

3. Os Resultados: Otimismo Realista

Os pesquisadores testaram isso com problemas de geometria de nível de vestibular (SAT).

• Sem ajuda: A IA sozinha acertava apenas cerca de 10% das provas complexas.
• Com o sistema: A precisão saltou para 80%.
• Economia: Além de acertar mais, o sistema foi inteligente ao escolher quais exemplos mostrar. Em vez de mostrar 18.000 regras de geometria para a IA ler (o que custaria muito dinheiro e tempo), o sistema filtrou e mostrou apenas as 2.500 regras relevantes para aquele problema específico.

4. Por que isso importa?

Atualmente, confiamos em IAs para muitas coisas, mas em áreas críticas (como medicina, segurança ou engenharia), um erro de lógica pode ser catastrófico.
Este trabalho mostra que, se combinarmos a criatividade e a linguagem da IA com a rigorosa precisão da matemática simbólica, podemos criar sistemas que não apenas "falam" bem, mas que pensam corretamente.

Em resumo: O papel transformou a IA de um "aluno que chuta a resposta" em um "aluno que estuda exemplos parecidos e revisa seu trabalho com um professor rigoroso até acertar". Isso abre portas para usar inteligência artificial em tarefas onde a verdade absoluta é necessária.

Resumo técnico

Resumo Técnico: Uma Abordagem Neuro-Simbólica para Geração de Provas Confiáveis com LLMs

1. O Problema

Os Grandes Modelos de Linguagem (LLMs) demonstram desempenho notável em diversas tarefas, mas falham consistentemente em domínios formais que exigem dedução lógica rigorosa e raciocínio simbólico, como a geração de provas matemáticas.

• Causas da Falha: A arquitetura dos LLMs baseia-se na geração probabilística de sequências aprendidas de grandes conjuntos de dados textuais. Isso resulta em uma tendência a gerar texto "plausível" em vez de inferências formalmente válidas.
• Desafios Específicos: Provas matemáticas exigem coerência lógica sustentada, manipulação simbólica e ausência de ambiguidade. Pequenas alterações superficiais em problemas matemáticos frequentemente levam a quedas drásticas de desempenho nos LLMs, sugerindo que eles dependem mais de correspondência de padrões do que de raciocínio matemático genuíno.
• Necessidade: Há uma demanda crítica por sistemas capazes de gerar conclusões provadamente corretas para aplicações em educação, ciência e tarefas críticas de segurança.

2. Metodologia: Abordagem Neuro-Simbólica

Os autores propõem um sistema híbrido que combina as capacidades generativas dos LLMs com dois componentes estruturados: Guia Analógico e Verificação Simbólica. O estudo de caso foca em problemas de geometria euclidiana (nível SAT) do conjunto de dados FormalGeo-7k.

O fluxo de trabalho é dividido em quatro etapas principais:

A. Abstração do Problema (Seção 3.1)

• Para identificar problemas estruturalmente semelhantes, o sistema abstrai o problema alvo e todo o conjunto de dados.
• Esquema de Abstração: Nomes de entidades (ex: linhas, ângulos) são substituídos por <word> e números por <num>.
• Exemplo: Equal(MeasureOfAngle(ABC), 40) torna-se Equal(MeasureOfAngle(<word>), <num>).

B. Recuperação de Problemas Analógicos (Seção 3.2)

• Um regressor neural é treinado para prever a similaridade de provas entre dois problemas com base na similaridade estrutural de suas descrições abstratas (construção, condições e objetivo).
• Utiliza-se a similaridade de Jaccard sobre os componentes formais.
• O sistema recupera os problemas mais similares (análogos) e utiliza suas provas completas como exemplos few-shot (aprendizado em contexto) para guiar o LLM.
• Otimização de Custo: Em vez de fornecer todo o dicionário de teoremas (196 teoremas), o sistema extrai apenas os teoremas utilizados nas provas dos problemas análogos, reduzindo o contexto de ~18k tokens para ~2.5k tokens em média.

C. Geração de Prova pelo LLM (Seção 3.3)

• O LLM recebe o problema alvo, os exemplos análogos (com provas e respostas) e o dicionário de teoremas filtrado.
• O objetivo é gerar uma prova formal passo a passo, invocando teoremas do dicionário para derivar a conclusão.

D. Verificador Simbólico e Feedback Iterativo (Seção 3.4)

• Um verificador externo, baseado em lógica simbólica e raciocínio algébrico (utilizando o solucionador SMT Z3), avalia a prova gerada.
• Ciclo de Feedback: Se a prova estiver incorreta, o verificador fornece feedback estruturado sobre o primeiro erro encontrado. O LLM usa esse feedback para tentar novamente.
• Tipos de Erros Identificados:
  1. Violação de Sintaxe: Erros de chamada de teorema ou argumentos inválidos.
  2. Violação de Premissas: Uso de teoremas cujas premissas não foram derivadas anteriormente.
  3. Objetivo Não Alcançado: A prova é sintaticamente correta, mas não deriva a resposta final ou a resposta difere da inferida pelo verificador.
• O ciclo continua até uma prova válida ser encontrada ou atingir um limite de tentativas.

3. Contribuições Principais

1. Sistema Neuro-Simbólico: Proposta de um sistema que integra guia analógico e feedback de verificação para auxiliar LLMs na geração de provas.
2. Verificador Simbólico Personalizado: Desenvolvimento de um verificador para provas de geometria que avalia a prova inteira (não apenas a resposta numérica) e fornece feedback explicativo.
3. Ganhos de Desempenho: Demonstração de melhorias significativas na precisão das provas, com ganhos de 58% a 70% para o modelo OpenAI o1 e 52% a 64% para o Gemini-2.5-Flash.
4. Redução de Custos: Uso de recuperação analógica para filtrar o dicionário de teoremas, reduzindo drasticamente o tamanho do contexto de entrada (tokens).
5. Reprodutibilidade: Liberação de código, dados e scripts de avaliação.

4. Resultados Experimentais

Os experimentos foram realizados no conjunto FormalGeo-7k (6.981 problemas), amostrando 50 problemas de diferentes níveis de dificuldade (1 a 5).

• Desempenho Geral:
  • A pipeline completa (analogia + verificador + múltiplas execuções) atingiu 80% de precisão agregada.
  • O modelo base (sem analogia, sem verificador, primeira tentativa) atingiu apenas 10%.
  • Mesmo sem múltiplas execuções (apenas uma tentativa com verificador), a precisão foi de 68% (vs. 10% do baseline).
• Contribuição dos Componentes (Ablação):
  • Recuperação de Analogia: Aumentou a precisão de 10% para 48% na primeira tentativa sem retries.
  • Feedback do Verificador: Adicionar retries (repetições com correção) aumentou a precisão em ~20% para o método proposto e ~28% para o modelo base.
  • Múltiplas Execuções: Melhorou ainda mais os resultados, especialmente em problemas mais difíceis (níveis 4 e 5).
• Robustez: Os resultados foram consistentes ao serem replicados no modelo Gemini-2.5-Flash, demonstrando que a abordagem é generalizável para diferentes famílias de LLMs.
• Precisão de Resposta vs. Prova: O modelo base frequentemente acertava o número final, mas falhava em gerar a prova correta que o justificava. O método proposto corrigiu essa lacuna, alcançando 100% de acerto na resposta numérica e 80% na prova formal.

5. Significado e Impacto

• Confiabilidade em IA: O trabalho demonstra que é possível superar as limitações de "alucinação" lógica dos LLMs ao acoplá-los a verificadores formais e guias estruturados.
• Aplicações Práticas: A abordagem abre caminho para o uso de LLMs em tarefas críticas de segurança e sistemas STEM (Ciência, Tecnologia, Engenharia e Matemática), onde a correção formal é obrigatória.
• Eficiência: A técnica de filtragem de contexto via analogia resolve o problema de custo e escalabilidade ao reduzir a quantidade de informações necessárias no prompt.
• Futuro: Os autores planejam expandir a abordagem para outros domínios formais além da geometria, explorar verificações mais expressivas (como lógica temporal) e aplicar o sistema no contexto educacional para fornecer feedback personalizado a estudantes.

Em suma, o artigo valida que a combinação de raciocínio analógico (para guiar a geração) e verificação simbólica (para corrigir e validar) é uma estratégia eficaz para transformar LLMs em ferramentas confiáveis para geração de provas matemáticas formais.