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

• URL: http://arxiv.org/abs/2606.24902v1
• Date: Fri, 12 Jun 2026 14:58:20 GMT
• Title: Failure Modes of Large Language Models on Research-Level Mathematics: A Taxonomy and an Empirical Characterisation
• Abstract summary: The "First Proof" benchmark posed ten research-level mathematics questions to the strongest publicly available LLMs.<n>I identify four failure modes: citation fabrication (F1), premise smuggling (F2), silent problem reformulation (F3), and local-to-global compatibility gaps (F4)<n>I then audit eight one-shot proofs generated by Gemini 2.5 Flash on Questions 1, 2, and 5 of the benchmark, using two instruments built specifically to surface F1 and F2.
• Score: 0.8594140167290097
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The "First Proof" benchmark [1] posed ten research-level mathematics questions to the strongest publicly available LLMs and found them consistently wrong-not silent, but confidently, fluently wrong. This paper asks why. Working from the per-question post-mortems in First Proof's Appendix A, I identify four failure modes: citation fabrication (F1), premise smuggling (F2), silent problem reformulation (F3), and local-to-global compatibility gaps (F4). I then audit eight one-shot proofs generated by Gemini 2.5 Flash on Questions 1, 2, and 5 of the benchmark, using two instruments built specifically to surface F1 and F2. The central finding is uncomfortable for anyone who sees retrieval-augmented generation (RAG) as the obvious fix: not one of the eight proofs contained a confirmed fabricated citation, yet every single one contained at least one load-bearing claim asserted as a "fundamental result" or "standard argument" with no justification attached. That failure mode-F2, premise smuggling-is invisible to citation verification by design. A premise-audit instrument I introduce flags it at 100% precision (5/5 judge-confirmed flags are true positives) and 50% proof-level recall in this corpus. The taxonomy and the audit together suggest that the right long-term objective is building inference-time pipelines that prevent these failure modes from occurring, not just detecting them after the fact. Index Terms--Large language models, mathematical reasoning, hallucination, premise smuggling, failure-mode taxonomy.

Related papers

• NovGauge: A Fine-Grained Benchmark for Diagnosing LLMs' Capability in Paper Novelty Assessment [54.4265627247104]
  Large language models (LLMs) are increasingly used in peer review at major AI conferences.<n>Existing benchmarks assess novelty as a single holistic score.<n>We present NovGauge, a human-anchored benchmark for fine-grained novelty assessment diagnosis.
  arXiv  Detail & Related papers  (2026-09-10T08:34:56Z)
• HALLMARK: Diagnosing Three Failure Modes in LLM Citation Verifiers [30.02579334273979]
  GPTZero found 53 papers with hallucinated citations among NeurIPS 2025's accepted set.<n>No shared benchmark compares verifiers and gives detailed failure diagnostics.<n>Hallucination benchmark: 2,526 Bib entries spanning 14 types, three difficulty tiers, six diagnostic sub-tests per entry.
  arXiv  Detail & Related papers  (2026-07-20T13:21:27Z)
• Auditing the Audit: Five Failure Modes in Benchmark-Validity Audits [0.30586855806896046]
  We name five classes of pipeline failure and demonstrate each in a self-audit over safety benchmarks and open-weight instruction-tuned models.<n>We position the gate as a withholding and disclosure protocol for assurance-grade evidence, supplementary to (not a replacement for) classical construct-validity evidence.
  arXiv  Detail & Related papers  (2026-07-01T05:30:07Z)
• Do LLMs Game Formalization? Evaluating Faithfulness in Logical Reasoning [20.336209492846752]
  Formal verification guarantees proof validity but not formalization faithfulness.<n>We investigate whether frontier models exploit this gap when generating Lean 4 proofs.<n>We find no evidence of systematic gaming in unified generation.
  arXiv  Detail & Related papers  (2026-04-21T13:37:49Z)
• CausalT5K: Diagnosing and Informing Refusal for Trustworthy Causal Reasoning of Skepticism, Sycophancy, Detection-Correction, and Rung Collapse [1.4608214000864057]
  CausalT5K is a diagnostic benchmark of over 5,000 cases across 10 domains.<n>Unlike synthetic benchmarks, CausalT5K embeds causal traps in realistic narratives.<n>Preliminary experiments reveal a Four-Quadrant Control Landscape where static audit policies universally fail.
  arXiv  Detail & Related papers  (2026-02-09T17:36:56Z)
• SIN-Bench: Tracing Native Evidence Chains in Long-Context Multimodal Scientific Interleaved Literature [92.88058660627678]
  "Fish-in-the-Ocean" (FITO) paradigm requires models to construct explicit cross-modal evidence chains within scientific documents.<n>We construct SIN-Bench with four progressive tasks covering evidence discovery (SIN-Find), hypothesis verification (SIN-Verify), grounded QA (SIN-QA) and evidence-anchored synthesis (SIN-Summary)<n>We introduce "No Evidence, No Score", scoring predictions when grounded to verifiable anchors and diagnosing evidence quality via matching, relevance, and logic.
  arXiv  Detail & Related papers  (2026-01-15T06:25:25Z)
• ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings [9.764411884491052]
  We present ProofBridge, a framework for automatically translating entire NL theorems and proofs into Lean 4.<n>At its core is a joint embedding model that aligns NL and FL (NL-FL) theorem-proof pairs in a shared semantic space.<n>Our training ensures NL-FL theorems are mapped close together in this space if and only if the NL-FL pairs are semantically equivalent.
  arXiv  Detail & Related papers  (2025-10-17T14:20:50Z)
• The Missing Parts: Augmenting Fact Verification with Half-Truth Detection [20.011177314734887]
  Many real-world claims are half-truths, factually correct yet misleading due to the omission of critical context.<n>We introduce the task of half-truth detection, and propose PolitiFact-Hidden, a new benchmark with 15k political claims annotated with sentence-level evidence alignment and inferred claim intent.<n>We present TRACER, a modular re-assessment framework that identifies omission-based misinformation by aligning evidence, inferring implied intent, and estimating the causal impact of hidden content.
  arXiv  Detail & Related papers  (2025-08-01T10:06:38Z)
• Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
  Chain-of-Thought prompting has become the de facto method to elicit reasoning capabilities from large language models (LLMs)<n>To mitigate hallucinations in CoT that are notoriously difficult to detect, current methods operate as opaque boxes and do not provide checkable evidence for their judgments, possibly limiting their effectiveness.<n>We propose a retrospective, step-aware formal verification framework $Safe$. Rather than assigning arbitrary scores, we strive to articulate mathematical claims in formal mathematical language Lean 4 at each reasoning step and provide formal proofs to identify hallucinations.
  arXiv  Detail & Related papers  (2025-06-05T03:16:08Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof.<n>Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment.
  arXiv  Detail & Related papers  (2024-07-14T01:43:07Z)
• Proving Theorems Recursively [80.42431358105482]
  We propose POETRY, which proves theorems in a level-by-level manner. Unlike previous step-by-step methods, POETRY searches for a sketch of the proof at each level. We observe a substantial increase in the maximum proof length found by POETRY, from 10 to 26.
  arXiv  Detail & Related papers  (2024-05-23T10:35:08Z)
• AmbiFC: Fact-Checking Ambiguous Claims with Evidence [57.7091560922174]
  We present AmbiFC, a fact-checking dataset with 10k claims derived from real-world information needs. We analyze disagreements arising from ambiguity when comparing claims against evidence in AmbiFC. We develop models for predicting veracity handling this ambiguity via soft labels.
  arXiv  Detail & Related papers  (2021-04-01T17:40:08Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.