Failure Modes of Large Language Models on Research-Level Mathematics: A Taxonomy and an Empirical Characterisation

Resumo Técnico: Modos de Falha de Grandes Modelos de Linguagem em Matemática de Nível de Pesquisa

Definição do Problema
Benchmarks recentes sugerem que os Grandes Modelos de Linguagem (LLMs) estão alcançando competência em raciocínio matemático, particularmente em problemas de estilo de competição. No entanto, o benchmark "First Proof" [1] revelou uma lacuna crítica: ao serem apresentados com dez questões de matemática genuína de nível de pesquisa (lemmas genuínos de projetos ativos sem respostas públicas), os modelos de última geração falharam consistentemente. Crucialmente, os modelos não admitiram incerteza; em vez disso, geraram provas longas, formalmente estruturadas e fluentemente escritas, mas substantivamente incorretas. O problema central que este artigo aborda é caracterizar por que esses modelos falham dessa maneira específica, indo além de simples taxas de erro para compreender a natureza estrutural das alucinações em provas matemáticas.

Metodologia
O artigo emprega uma abordagem de duas frentes: uma derivação de taxonomia qualitativa e uma auditoria empírica quantitativa.

1. Derivação de Taxonomia: O autor analisou os pós-mórtems por questão fornecidos no Apêndice A do estudo "First Proof". A partir dessas análises de especialistas, quatro modos de falha distintos foram identificados e formalizados.
2. Auditoria Empírica: Para testar a validade desta taxonomia, o autor gerou um corpus de oito provas de disparo único (one-shot) usando o Gemini 2.5 Flash em três questões específicas do benchmark (Questões 1, 2 e 5).
3. Instrumentação: Duas ferramentas específicas foram construídas para detectar os modos de falha mais prevalentes:
   • Instrumento de Verificação de Citação: Um pipeline que extrai citações de provas e as cruza com o arXiv para detectar artigos ou lemmas fabricados (F1).
   • Instrumento de Auditoria de Premissa: Um pipeline de dois estágios projetado para detectar o "contrabando de premissas" (F2). Ele primeiro utiliza regex para sinalizar sentenças contendo frases universalizantes (ex: "resultado fundamental", "argumento padrão", "bem conhecido") e, em seguida, emprega um juiz de LLM para determinar se a sentença sinalizada afirma uma alegação não trivial e de carga lógica (load-bearing) sem justificativa ou citação.

Principais Contribuições
A principal contribuição do artigo é a Taxonomia de Modos de Falha, que categoriza as falhas matemáticas de LLMs em quatro tipos:

• F1 (Fabricação de Citação): O modelo inventa artigos, lemmas ou atribuições. Isso é verificável ao checar se a citação existe e contém o resultado alegado.
• F2 (Contrabando de Premissa): O modelo afirma uma alegação não trivial como conhecimento de base (ex: "é um resultado fundamental...") sem prova ou citação. Este é o modo mais insidioso porque não há citação para verificar; o erro reside na própria afirmação.
• F3 (Reformulação Silenciosa do Problema): O modelo resolve um problema relacionado, porém mais fácil (ex: removendo restrições não triviais ou alterando o objeto matemático) e o apresenta como a solução para o original.
• F4 (Lacuna de Compatibilidade Local-Global): O modelo executa etapas locais corretamente, mas falha em verificar se essas etapas são mutuamente compatíveis em toda a estrutura da prova (ex: sobreposição de cartas em geometria).

O artigo também introduz o Instrumento de Auditoria de Premissa como um método para operacionalizar a detção de F2, um modo de falha amplamente ignorado pelas estratégias de mitigação atuais.

Resultados
A auditoria empírica dos oito textos do Gemini 2.5 Flash rendeu os seguintes achados:

• Falha Universal: Nenhuma das oito provas produziu uma resposta final correta.
• Dominância de F2: Embora o instrumento de Verificação de Citação tenha encontrado poucas citações fabricadas (apenas 6 de 22 exigiam verificações na web, e nenhuma foi confirmada como fabricação no subconjunto Q1/Q2), o instrumento de Auditoria de Premissa encontrou que cada uma das oito provas continha pelo menos uma premissa de carga lógica contrabandada como um "resultado fundamental" ou "argumento padrão".
• Desempenho do Instrumento: O instrumento de Auditoria de Premissa alcançou 100% de precisão (5/5 sinalizações confirmadas pelo juiz foram verdadeiros positivos), mas apenas 50% de recall ao nível da prova. Os casos perdidos foram "contrabandos implícitos", onde o modelo aplicou um teorema nomeado fora de suas hipóteses ou usou manipulações formais sem linguagem universalizante, o que o primeiro estágio baseado em regex falhou em capturar.
• Limitações de RAG: Os resultados indicam que a Geração Aumentada por Recuperação (RAG), a solução padrão proposta para alucinações de LLM, provavelmente falharia em abordar o modo de falha dominante (F2). Como os modelos neste corpus não citaram artigos falsos, mas sim afirmaram premissas falsas como conhecimentos estabelecidos, simplesmente recuperar artigos corretos não impediria o modelo de fazer afirmações injustificadas.

Significância e Alegações
O artigo argumenta que a narrativa atual de progresso constante no raciocínio matemático de LLMs é enganosa quando aplicada a tarefas de nível de pesquisa. A significância específica deste trabalho reside em:

1. Reenquadramento da Falha: Demonstrar que a principal barreira para LLMs resolverem matemática de pesquisa não é necessariamente a invenção de citações falsas (F1), mas a afirmação confiante de premissas falsas como fatos estabelecidos (F2).
2. Crítica ao RAG: Desafiar a suposição de que fundamentar modelos em bases de dados externas é uma solução suficiente. O artigo postula que o RAG aborda F1, mas deixa F2, F3 e F4 sem resposta.
3. Direção Futura: O autor conclui que o objetivo de longo prazo deve mudar da detecção dessas falhas após o fato para a construção de pipelines de inferência que impeçam a ocorrência desses modos. Tais sistemas precisariam garantir que cada alegação de carga lógica seja derivada de premissas declaradas, fundamentada em uma fonte verificada ou explicitamente sinalizada como não verificada antes da saída.

O autor mantém uma postura modesta, reconhecendo que o corpus é pequeno (8 provas) e utiliza um modelo de nível médio (Flash) em vez dos modelos de fronteira testados no "First Proof". No entanto, o artigo afirma que os modos de falha identificados são reais, que o F2 é precisamente definível e que o cenário de mitigação atual está desalinhado com a natureza real dos erros.