Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving on Inequalities

TL;DR

Ineq-Comp introduces a bottom-up benchmark to diagnose compositional generalization in automated theorem proving for inequalities by starting from seed Lean 4 proofs of classical inequalities and applying controlled transformations to generate simple and multi-step variants. The study systematically evaluates a spectrum of provers, revealing a persistent gap: current systems struggle to reuse and compose basic reasoning strategies, even when provided with seed solutions or exposed to algebraic transformations. Key findings show heavy reliance on low-level tactics like sum-of-squares ($nlinarith$) and limited transfer of in-context demonstrations or fine-tuning to out-of-distribution variants, underscoring a fundamental brittleness in formal compositional reasoning. The work contributes a scalable dataset (Ineq-Simp, Ineq-Mix, Ineq-Real) and a framework for evaluating and extending compositional reasoning in formal proofs, highlighting a critical area for improving alignment between AI provers and human mathematical intuition.

Abstract

LLM-based formal proof assistants (e.g., in Lean) hold great promise for automating mathematical discovery. But beyond syntactic correctness, do these systems truly understand mathematical structure as humans do? We investigate this question in context of mathematical inequalities -- specifically the prover's ability to recognize that the given problem simplifies by applying a known inequality such as AM/GM. Specifically, we are interested in their ability to do this in a compositional setting where multiple inequalities must be applied as part of a solution. We introduce Ineq-Comp, a benchmark built from elementary inequalities through systematic transformations, including variable duplication, algebraic rewriting, and multi-step composition. Although these problems remain easy for humans, we find that most provers -- including Goedel, STP, and Kimina-7B -- struggle significantly. DeepSeek-Prover-V2-7B shows relative robustness, but still suffers a 20% performance drop (pass@32). Even for DeepSeek-Prover-V2-671B model, the gap between compositional variants and seed problems exists, implying that simply scaling up the model size alone does not fully solve the compositional weakness. Strikingly, performance remains poor for all models even when formal proofs of the constituent parts are provided in context, revealing that the source of weakness is indeed in compositional reasoning. Our results expose a persisting gap between the generalization behavior of current AI provers and human mathematical intuition. All data and evaluation code can be found at https://github.com/haoyuzhao123/LeanIneqComp.

Figures (4)

• Figure 1: Left: Starting from a seed problem, we apply transformations that are intuitive to humans. Type i data are generated by duplicating the original inequality using distinct variable names and multiplying the two resulting inequalities. Type ii data are created via algebraic manipulations. These transformed problems are trivial to solve if one has already understood the seed problem, and we would expect minimal performance drop between solving the seed problem and its transformed variations. Mid: Pass@32 accuracy of various models on the original seed problems and their transformed counterparts (Type i and Type ii). All models, except DeepSeek-Prover-V2, exhibit substantial performance degradation on the transformed problems. Notably, even DeepSeek-Prover-V2-7B experiences a drop of over 20%. Right: Average success rate (Pass@1 within 3200 attempts) on the subset of problems each model is able to solve. While seed problems have relatively high solve rates across models, the transformed variants become significantly more challenging. For example, even for the strongest model---DeepSeek-Prover-V2-7B--- its success rate drops from 50% on seed problems to 25% on their transformed counterparts. The drop suggests that current provers are sensitive to surface form rather than the underlying semantic equivalence of mathematical reasoning.
• Figure 2: Pass@N accuracy of various LLM-based theorem provers on the Ineq-Mix (Left) and Ineq-Real (Right) subsets under increasing computational budgets (x-axis). Surprisingly, the automatically generated Ineq-Mix problems---created by applying simple, human-intuitive compositional transformations to pairs of seed inequalities---are more challenging for current models than the real-world problems in Ineq-Real. Most models, including Goedel-Prover, STP, and Kimina, solve fewer than 7% of Ineq-Mix problems even with 128 attempts, while DeepSeek-Prover-V2 achieves a modest 22%. In contrast, on Ineq-Real, the model performance are at least doubled. This result highlights a critical weakness in formal theorem provers: reasoning compositionally across structurally simple subproblems is harder than solving complex, real-world inequalities.
• Figure 3: Pipeline for evaluating if composition can be learned through naive fine-tuning. We split the seed problems into ${\mathcal{P}}_{\text{train}}$, which contains 25 problems utilizing AMGM, and ${\mathcal{P}}_{\text{held-out}}$, which contains the remaining 50 problems. The pipeline consists of three steps: (1) generate data by prompting LLM given the proof of seed problems in context and keep only the proofs that pass Lean compilation; (2) fine-tune Goedel-Prover-SFT; (3) evaluate type i and ii problems and Ineq-Mix on ${\mathcal{P}}_{\text{held-out}}$.
• Figure 4: SFT base ablation. The performance of the fine-tuned model on different type of problems in Ineq-AMGM (ID), Ineq-Cauchy (OOD) and Ineq-MISC (OOD). We group different types of problems in Ineq-Cauchy and Ineq-MISC together as OOD and report the accuracy under Pass@3200. Although fine-tuning significantly improved in-distribution (ID) Type i performance, it did not lead to meaningful improvements on out-of-distribution (OOD) generalization tasks or algebraic transformation problems.