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

Technical Summary: Failure Modes of Large Language Models on Research-Level Mathematics

Problem Statement
Recent benchmarks suggest Large Language Models (LLMs) are achieving competence in mathematical reasoning, particularly on competition-style problems. However, the "First Proof" benchmark [1] revealed a critical gap: when presented with ten genuine research-level mathematics questions (genuine lemmas from live projects with no public answers), state-of-the-art models failed consistently. Crucially, the models did not admit uncertainty; instead, they generated long, formally structured, and fluently written proofs that were substantively incorrect. The central problem this paper addresses is characterizing why these models fail in this specific manner, moving beyond simple error rates to understand the structural nature of the hallucinations in mathematical proofs.

Methodology
The paper employs a two-pronged approach: a qualitative taxonomy derivation and a quantitative empirical audit.

1. Taxonomy Derivation: The author analyzed the per-question post-mortems provided in the Appendix A of the "First Proof" study. From these expert analyses, four distinct failure modes were identified and formalized.
2. Empirical Audit: To test the validity of this taxonomy, the author generated a corpus of eight one-shot proofs using Gemini 2.5 Flash on three specific questions from the benchmark (Questions 1, 2, and 5).
3. Instrumentation: Two specific tools were built to detect the most prevalent failure modes:
   • Citation-Verification Instrument: A pipeline that extracts citations from proofs and cross-references them against arXiv to detect fabricated papers or lemmas (F1).
   • Premise-Audit Instrument: A two-stage pipeline designed to detect "premise smuggling" (F2). It first uses regex to flag sentences containing universalizing phrases (e.g., "fundamental result," "standard argument," "well-known") and then employs an LLM judge to determine if the flagged sentence asserts a non-trivial, load-bearing claim without justification or citation.

Key Contributions
The paper's primary contribution is the Failure-Mode Taxonomy, which categorizes LLM mathematical failures into four types:

• F1 (Citation Fabrication): The model invents papers, lemmas, or attributions. This is verifiable by checking if the citation exists and contains the claimed result.
• F2 (Premise Smuggling): The model asserts a non-trivial claim as background knowledge (e.g., "it is a fundamental result...") without proof or citation. This is the most insidious mode because there is no citation to verify; the error hides in the assertion itself.
• F3 (Silent Problem Reformulation): The model solves a related but easier problem (e.g., removing non-triviality constraints or changing the mathematical object) and presents it as the solution to the original.
• F4 (Local-to-Global Compatibility Gap): The model executes local steps correctly but fails to verify that these steps are mutually compatible across the entire proof structure (e.g., overlapping charts in geometry).

The paper also introduces the Premise-Audit Instrument as a method to operationalize the detection of F2, a failure mode largely ignored by current mitigation strategies.

Results
The empirical audit of the eight Gemini 2.5 Flash proofs yielded the following findings:

• Universal Failure: None of the eight proofs produced a correct final answer.
• Dominance of F2: While the Citation-Verification instrument found very few fabricated citations (only 6 out of 22 required web checks, and none were confirmed fabrications in the Q1/Q2 subset), the Premise-Audit instrument found that every single proof contained at least one load-bearing premise smuggled as a "fundamental result" or "standard argument."
• Instrument Performance: The Premise-Audit instrument achieved 100% precision (5/5 judge-confirmed flags were true positives) but only 50% recall at the proof level. The missed cases were "implicit" smuggles where the model applied a named theorem outside its hypotheses or used formal manipulations without universalizing language, which the regex-based first stage failed to catch.
• RAG Limitations: The results indicate that Retrieval-Augmented Generation (RAG), the standard proposed fix for LLM hallucinations, would likely fail to address the dominant failure mode (F2). Since the models in this corpus did not cite fake papers but rather asserted false premises as background knowledge, simply retrieving correct papers would not prevent the model from making unjustified assertions.

Significance and Claims
The paper argues that the current narrative of steady progress in LLM mathematical reasoning is misleading when applied to research-level tasks. The specific significance of this work lies in:

1. Reframing the Failure: Demonstrating that the primary barrier to LLMs solving research math is not necessarily the invention of fake citations (F1), but the confident assertion of false premises as established facts (F2).
2. Critique of RAG: Challenging the assumption that grounding models in external databases is a sufficient solution. The paper posits that RAG addresses F1 but leaves F2, F3, and F4 unaddressed.
3. Future Direction: The author concludes that the long-term objective should shift from detecting these failures after the fact to building inference-time pipelines that prevent these modes from occurring. Such systems would need to enforce that every load-bearing claim is either derived from stated premises, grounded in a verified source, or explicitly flagged as unverified before output.

The author maintains a modest stance, acknowledging that the corpus is small (8 proofs) and uses a mid-tier model (Flash) rather than the frontier models tested in "First Proof." However, the paper asserts that the identified failure modes are real, that F2 is precisely definable, and that the current mitigation landscape is misaligned with the actual nature of the errors.