BrokenMath: A Benchmark for Sycophancy in Theorem Proving with LLMs

• URL: http://arxiv.org/abs/2510.04721v1
• Date: Mon, 06 Oct 2025 11:41:46 GMT
• Title: BrokenMath: A Benchmark for Sycophancy in Theorem Proving with LLMs
• Abstract summary: We introduce BrokenMath, the first benchmark for evaluating sycophantic behavior in large language models (LLMs)<n>We evaluate state-of-the-art LLMs and agentic systems and find that sycophancy is widespread, with the best model, GPT-5, producing sycophantic answers 29% of the time.
• Score: 5.347237827669862
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large language models (LLMs) have recently shown strong performance on mathematical benchmarks. At the same time, they are prone to hallucination and sycophancy, often providing convincing but flawed proofs for incorrect mathematical statements provided by users. This significantly limits the applicability of LLMs in theorem proving, as verification of these flawed proofs must be done manually by expert mathematicians. However, existing benchmarks that measure sycophancy in mathematics are limited: they focus solely on final-answer problems, rely on very simple and often contaminated datasets, and construct benchmark samples using synthetic modifications that create ill-posed questions rather than well-posed questions that are demonstrably false. To address these issues, we introduce BrokenMath, the first benchmark for evaluating sycophantic behavior in LLMs within the context of natural language theorem proving. BrokenMath is built from advanced 2025 competition problems, which are perturbed with an LLM to produce false statements and subsequently refined through expert review. Using an LLM-as-a-judge framework, we evaluate state-of-the-art LLMs and agentic systems and find that sycophancy is widespread, with the best model, GPT-5, producing sycophantic answers 29% of the time. We further investigate several mitigation strategies, including test-time interventions and supervised fine-tuning on curated sycophantic examples. These approaches substantially reduce, but do not eliminate, sycophantic behavior.

Related papers

• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  Large Language Models (LLMs) exhibit strong informal mathematical reasoning but struggle to generate verifiable proofs in formal languages like Lean.<n>We present LEAP, an agentic framework that enables general-purpose foundation models to achieve state-of-the-art performance on automated formal theorem proving.
  arXiv  Detail & Related papers  (2026-06-02T08:16:42Z)
• Automatically Generating Hard Math Problems from Hypothesis-Driven Error Analysis [16.008582390875656]
  We propose a new benchmark generation pipeline that uses AI-generated hypotheses to identify the specific math concepts and skills that LLMs struggle with.<n>Our pipeline is highly adaptable and can be applied beyond math to explore a wide range of LLM capabilities.
  arXiv  Detail & Related papers  (2026-04-06T03:27:48Z)
• LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
  We present LiveMathematicianBench, a dynamic multiple-choice benchmark for research-level mathematical reasoning.<n>By grounding evaluation in newly published theorems, it provides a realistic testbed beyond memorized patterns.<n>It employs a proof-sketchguided distractor pipeline that uses high-level proof strategies to construct plausible but invalid answer choices.
  arXiv  Detail & Related papers  (2026-04-02T08:22:17Z)
• LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics [5.676144562388248]
  We present a new approach for benchmarking Large Language Model capabilities on research-level mathematics.<n>Existing benchmarks largely rely on static, hand-curated sets of contest or textbook-style problems as proxies for mathematical research.<n>Instead, we establish an updatable benchmark evaluating models directly on the latest research results in mathematics.
  arXiv  Detail & Related papers  (2026-02-27T16:52:52Z)
• Solving Inequality Proofs with Large Language Models [46.71658812761115]
  Inequality proving is crucial across diverse scientific and mathematical fields.<n>This makes it a demanding frontier for large language models (LLMs)<n>We release IneqMath, an expert-curated dataset of Olympiad-level inequalities.
  arXiv  Detail & Related papers  (2025-06-09T16:43:38Z)
• Challenging the Boundaries of Reasoning: An Olympiad-Level Math Benchmark for Large Language Models [86.45058529521258]
  OlymMATH is a novel Olympiad-level mathematical benchmark designed to rigorously test the complex reasoning capabilities of LLMs.<n>OlymMATH features 200 meticulously curated problems, each manually verified and available in parallel English and Chinese versions.
  arXiv  Detail & Related papers  (2025-03-27T11:20:17Z)
• InductionBench: LLMs Fail in the Simplest Complexity Class [53.70978746199222]
  Large language models (LLMs) have shown remarkable improvements in reasoning.<n>Inductive reasoning, where one infers the underlying rules from observed data, remains less explored.<n>We introduce InductionBench, a new benchmark designed to evaluate the inductive reasoning ability of LLMs.
  arXiv  Detail & Related papers  (2025-02-20T03:48:00Z)
• One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs [75.95179490687018]
  Leveraging mathematical Large Language Models for proof generation is a fundamental topic in LLMs research.<n>We argue that the ability of current LLMs to prove statements largely depends on whether they have encountered the relevant proof process during training.<n>Inspired by the pedagogical method of "proof by counterexamples" commonly used in human mathematics education, our work aims to enhance LLMs' ability to conduct mathematical reasoning and proof through counterexamples.
  arXiv  Detail & Related papers  (2025-02-12T02:01:10Z)
• HARDMath: A Benchmark Dataset for Challenging Problems in Applied Mathematics [1.5716764919736026]
  We introduce HARDMath, a dataset featuring challenging applied mathematics problems that require analytical approximation techniques.<n>Our framework auto-generates a large number of problems with solutions validated against numerical ground truths.<n>We evaluate both open- and closed-source LLMs on HARDMath-mini, a sub-sampled test set of 366 problems, as well as on 40 word problems formulated in applied science contexts.
  arXiv  Detail & Related papers  (2024-10-13T20:09:41Z)
• MathHay: An Automated Benchmark for Long-Context Mathematical Reasoning in LLMs [61.74749961334557]
  MathHay is an automated benchmark designed to assess the long-context mathematical reasoning capabilities of LLMs. We conduct extensive experiments on MathHay to assess the long-context mathematical reasoning abilities of eight top-performing models.
  arXiv  Detail & Related papers  (2024-10-07T02:30:07Z)
• Large Language Models Struggle with Unreasonability in Math Problems [41.970853209666224]
  Large Language Models (LLMs) have shown remarkable success on a wide range of math and reasoning benchmarks.<n>We observe that they often struggle when faced with unreasonable math problems.<n>We propose the textbfUnreasonable Math Problems (UMP) benchmark, designed to evaluate LLMs' ability to detect and respond to unreasonable math problem statements.
  arXiv  Detail & Related papers  (2024-03-28T12:04:28Z)
• GSM-Plus: A Comprehensive Benchmark for Evaluating the Robustness of LLMs as Mathematical Problem Solvers [68.77382332826167]
  Large language models (LLMs) have achieved impressive performance across various mathematical reasoning benchmarks. One essential and frequently occurring evidence is that when the math questions are slightly changed, LLMs can behave incorrectly. This motivates us to evaluate the robustness of LLMs' math reasoning capability by testing a wide range of question variations.
  arXiv  Detail & Related papers  (2024-02-29T15:26:14Z)
• LLMs as Factual Reasoners: Insights from Existing Benchmarks and Beyond [135.8013388183257]
  We propose a new protocol for inconsistency detection benchmark creation and implement it in a 10-domain benchmark called SummEdits. Most LLMs struggle on SummEdits, with performance close to random chance. The best-performing model, GPT-4, is still 8% below estimated human performance.
  arXiv  Detail & Related papers  (2023-05-23T21:50:06Z)

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.