LeanTutor: Towards a Verified AI Mathematical Proof Tutor

Este artigo apresenta o LeanTutor, um tutor de provas matemáticas baseado em IA que combina as capacidades de comunicação natural de modelos de linguagem com a correção verificável de provadores de teoremas, e introduz o PeanoBench como um novo conjunto de dados para avaliação.

O essencial

Imagine que você está aprendendo a andar de bicicleta. Você tem dois tipos de "instrutores" disponíveis:

1. O Amigo Conversador (LLM): É um amigo muito falante, inteligente e rápido. Ele pode explicar tudo em linguagem comum, mas às vezes ele inventa coisas, dá conselhos errados ou, pior, te diz exatamente como chegar ao topo da montanha sem deixar você pedalar.
2. O Chefe de Engenharia (Provedor de Teoremas): É um robô extremamente rigoroso. Ele não erra. Se você fizer um movimento errado, ele grita "ERRO!" e não deixa você continuar. O problema é que ele só fala uma língua estranha e difícil (código), e se você não souber essa língua, ele não consegue te ajudar.

O LeanTutor é a criação de um novo tipo de professor que une o melhor dos dois mundos. É como ter um tradutor mágico que faz o "Amigo Conversador" e o "Chefe de Engenharia" trabalharem juntos.

Como funciona o LeanTutor?

O sistema é dividido em três "mágicos" que trabalham em equipe:

1. O Tradutor (Autoformalizador):
   Imagine que você escreve sua prova matemática em português, como se estivesse conversando com um amigo. O "Tradutor" pega o que você escreveu e tenta transformá-lo instantaneamente na língua estranha do "Chefe de Engenharia" (código Lean).

   • O desafio: Se você pular um passo ou escrever algo confuso, o Tradutor precisa entender que você errou, em vez de inventar uma versão correta que não é a sua.

2. O Detetive de Próximos Passos (Gerador de Próximo Passo):
   Se o "Chefe de Engenharia" diz que a prova está travada ou errada, o Detetive entra em ação. Ele olha para onde você está e, usando o código, tenta descobrir qual seria o próximo movimento lógico para continuar. Ele não te dá a resposta final, mas te diz: "Ei, tente usar esta ferramenta aqui".

3. O Professor de Português (Gerador de Feedback):
   Este é o cara que fala com você. Ele pega o erro que o "Chefe" detectou e a sugestão do "Detetive" e transforma tudo em uma dica amigável. Em vez de dizer "Sintaxe inválida no comando X", ele diz: "Parece que você esqueceu de verificar o caso base. Tente simplificar essa parte primeiro".

O Grande Desafio: O "Jogo dos Números Naturais"

Para testar se essa ideia funcionava, os criadores do LeanTutor precisavam de um campo de treinamento. Eles usaram um dataset chamado PeanoBench.

Pense nisso como um livro de exercícios de matemática que contém 371 problemas. O que torna esse livro especial é que, para cada problema, eles têm duas versões:

• A versão escrita por humanos (em português).
• A versão escrita em código (em Lean).

Eles criaram até mesmo "versões erradas" dos exercícios, simulando erros comuns que alunos cometem (como pular um passo ou assumir algo sem provar), para ver se o sistema conseguia identificar e corrigir.

Por que isso é importante?

Hoje em dia, muitos alunos usam IAs (como o ChatGPT) para fazer lições de casa. O problema é que essas IAs muitas vezes:

• Dão a resposta pronta (o aluno não aprende).
• Inventam fatos (alucinações).
• Não conseguem explicar por que algo está errado.

O LeanTutor tenta resolver isso. Ele permite que o aluno fale a língua dele (português), mas garante que a matemática por trás seja verificada com precisão absoluta pelo computador. É como ter um tutor que é paciente e conversador, mas que nunca deixa você passar de nível se não tiver realmente aprendido a lição.

O Resultado?

O sistema funcionou bem! Ele conseguiu:

• Entender provas escritas de forma natural.
• Identificar onde o aluno errou.
• Dar dicas que ajudavam o aluno a pensar, em vez de apenas dar a resposta.

Em resumo: O LeanTutor é como um "ponte" segura entre a linguagem humana e a precisão matemática. Ele quer que a Inteligência Artificial ajude você a aprender a pensar, e não apenas a copiar respostas. É um passo gigante para tornar o ensino de matemática avançada mais acessível e confiável.

Resumo técnico

Título: LeanTutor: Rumo a um Tutor de Prova Matemática com Verificação por IA

1. Problema

O uso de Grandes Modelos de Linguagem (LLMs) como ChatGPT e Claude no ensino superior, especialmente em cursos de prova matemática, apresenta desafios pedagógicos e técnicos significativos:

• Alucinações e Erros: LLMs são propensos a gerar respostas convincentes, mas incorretas, e falham em identificar erros de raciocínio.
• Falta de Pedagogia: Modelos tendem a fornecer respostas diretas em vez de guiar o aluno através do processo de descoberta, prejudicando o desenvolvimento do pensamento crítico.
• Limitações dos Sistemas Atuais: Tutoriais baseados em provadores de teoremas (como Lean) são rigorosos e corretos, mas exigem que os alunos dominem uma sintaxe formal complexa, o que cria uma barreira de entrada alta.
• Necessidade: Existe uma lacuna para um sistema que combine a fluência em linguagem natural dos LLMs com a garantia de correção formal dos provadores de teoremas, oferecendo feedback imediato e privado sem revelar a resposta completa.

2. Metodologia

Os autores propõem o LeanTutor, um sistema de tutoria híbrido que integra LLMs e o provador de teoremas Lean. O sistema opera através de três módulos principais:

1. Autoformalizador / Verificador de Prova:

   • Converte provas escritas pelo aluno em linguagem natural (NL) para código Lean (FL) passo a passo.
   • Utiliza um LLM para a tradução, mas valida cada passo compilando-o no Lean.
   • Se a compilação falhar, o sistema identifica o passo como incorreto.
   • Estratégia de Prompt: Inclui uma "Solução de Referência" (staff solution) em NL e FL, dicionários de teoremas e táticas, e exemplos few-shot para guiar a tradução.

2. Gerador de Próximo Passo (Next Step Generator - NSG):

   • Ativado quando a prova do aluno está incompleta ou incorreta.
   • Realiza uma busca em profundidade (DFS) dirigida por LLM para gerar candidatos a táticas Lean.
   • Filtra os candidatos através de um "verificador de progresso" para garantir que não se usem teoremas proibidos (como o teorema que está sendo provado) e que não haja ciclos na árvore de prova.
   • O objetivo é encontrar um caminho viável para completar a prova sem revelar a solução inteira imediatamente.

3. Gerador de Feedback em Linguagem Natural:

   • Combina o estado da prova, mensagens de erro do compilador Lean e o próximo passo gerado pelo NSG.
   • Produz três tipos de feedback:
     1. Identificação de Erro: Aponta onde o aluno errou.
     2. Dica/Pergunta: Guia o aluno para o próximo passo sem dar a resposta.
     3. Passo Explícito (Bottom-out Hint): Fornece a tática exata se o aluno estiver travado.

3. Contribuições Chave

• Sistema LeanTutor: Uma arquitetura funcional que demonstra a viabilidade de combinar LLMs (para interface natural) com provadores de teoremas (para verificação rigorosa).
• PeanoBench: Um novo conjunto de dados (dataset) contendo 371 provas de Aritmética de Peano.
  • Inclui provas corretas e incorretas em linguagem natural e formal (Lean).
  • As provas incorretas foram geradas programaticamente simulando erros lógicos comuns (como pular passos).
  • As provas corretas foram anotadas com diferentes "personas" (baseadas em equações ou justificações) para variar a linguagem natural.
• Métrica de Autoformalização Fiel: Proposição de uma nova métrica para avaliar a qualidade da tradução NL $\to$ FL.
  • Vai além da simples correspondência de strings ou compilação.
  • Utiliza correspondência de estados de prova: verifica se, após aplicar a tática gerada e a tática de referência, os estados de prova resultantes são sintaticamente idênticos (ignorando nomes de variáveis).
• Abordagem Passo a Passo: Demonstração de que a autoformalização passo a passo (step-by-step) é superior à geração de provas inteiras de uma vez, especialmente para detectar e corrigir erros em provas incorretas.

4. Resultados

• Desempenho do Autoformalizador:

  • O modelo com "Solução de Referência" (Staff Solution) no contexto superou significativamente a linha de base.
  • Precisão de Táticas (Provas Corretas): Aumentou de 32,9% (Base) para 56,8% (Base + Staff Solution).
  • Precisão de Provas (Provas Incorretas): A abordagem passo a passo com Staff Solution alcançou 30,1% de sucesso em formalizar corretamente até o primeiro erro, superando a abordagem de "prova inteira" em 8 pontos percentuais.
  • Observação: O modelo ainda depende fortemente da solução de referência fornecida no contexto; quando a formalização do aluno não correspondia à referência, a precisão caía.

• Avaliação do Sistema Completo (Feedback):

  • Avaliado por especialistas humanos em quatro eixos: Precisão, Relevância, Legibilidade e Vazamento de Resposta (Answer Leakage).
  • LeanTutor vs. Baseline (LLM puro): O LeanTutor superou a linha de base em Precisão e Relevância.
  • Ambos os modelos tiveram desempenho semelhante em Legibilidade.
  • O LeanTutor reduziu significativamente o vazamento de resposta (dar a solução completa) no feedback de "Próximo Passo" em comparação com a linha de base.
  • Nota: A avaliação usando "LLM como Juiz" (GPT-4) mostrou resultados divergentes das avaliações humanas, favorecendo a linha de base, o que reforça a necessidade de avaliação humana para tarefas pedagógicas.

5. Significado e Limitações

• Significado: O trabalho valida a abordagem de "IA Verificada" para educação matemática. Ele resolve o dilema entre a usabilidade (linguagem natural) e a correção (verificação formal), oferecendo um modelo para futuros tutores de IA que não apenas "adivinhem" a resposta, mas verifiquem a lógica.
• Limitações:
  • Dependência de Solução de Referência: O sistema assume que uma prova formalizada correta já existe para o teorema em questão.
  • Correspondência 1:1: A arquitetura atual assume uma correspondência direta entre passos em NL e táticas em Lean, o que pode não escalar para provas complexas com granularidade diferente.
  • Falha na Autoformalização: Se o autoformalizador falhar (não traduzir corretamente a intenção do aluno), o sistema pode fornecer feedback incorreto ou falhar em responder.
  • Conjunto de Dados: O PeanoBench foi criado por autores do artigo, não por alunos reais, embora tenham tentado simular variações de linguagem.

Conclusão

O LeanTutor representa um passo importante rumo a tutores de matemática assistidos por IA que são pedagogicamente eficazes e matematicamente rigorosos. Ao delegar a verificação lógica para o Lean e usar LLMs apenas para a interface e geração de dicas, o sistema mitiga os riscos de alucinação e vazamento de respostas, estabelecendo uma base para futuras pesquisas em sistemas híbridos humano-IA na educação.