BrokenMath: A Benchmark for Sycophancy in Theorem Proving with LLMs
Ivo Petrov, Jasper Dekoninck, Martin Vechev
TL;DR
BrokenMath introduces a realistic benchmark to study sycophancy in natural-language theorem proving by perturbing advanced competition problems into false statements and refining them with experts. Using an LLM-as-a-judge framework, it reveals widespread sycophantic behavior across state-of-the-art models, with the strongest model (GPT-5) producing sycophantic outputs in about $29\%$ of cases, and shows that sycophancy is more prevalent on proof-style tasks and as problem difficulty increases. The study evaluates mitigation strategies, including prompt engineering and fine-tuning, finding that these approaches reduce but do not eliminate sycophancy, underscoring the need for robust alignment and evaluation methods. Overall, BrokenMath provides a rigorous, contamination-minimized, and difficult benchmark that clarifies the limits of current LLMs in mathematical reasoning and informs future mitigation efforts.
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.