# Ineqmath Eval

> This benchmark evaluates large language models' ability to perform informal mathematical reasoning on Olympiad-level inequality problems. It probes step-wise deductive chain integrity by decomposing proofs into bound estimation and relation prediction subtasks, requiring models to generate logically sound derivations rather than just final answers. Use when the user wants to benchmark on IneqMath, or asks about evaluating this task. Reports LLM-as-judge accuracy.

- Skill: `qhjqhj00/ineqmath-eval` (Agent Skill)
- Install (CLI): `npx skillmds add qhjqhj00/ineqmath-eval`
- Raw SKILL.md: https://api.skillmd.com/api/skills/qhjqhj00/ineqmath-eval/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: AI & ML
- Author: qhjqhj00 (https://skillmd.com/u/qhjqhj00)
- Updated: 2026-09-08
- Page: https://skillmd.com/skills/qhjqhj00/ineqmath-eval

---


# ineqmath-eval

> Solving Inequality Proofs with Large Language Models — Sheng et al. (2025) (arXiv:2506.07927, 2025)

## What this evaluates

This benchmark evaluates large language models' ability to perform informal mathematical reasoning on Olympiad-level inequality problems. It probes step-wise deductive chain integrity by decomposing proofs into bound estimation and relation prediction subtasks, requiring models to generate logically sound derivations rather than just final answers.

## Datasets

- **IneqMath** — total ?; splits: test (-1); repo https://github.com/lupantech/ineqmath

## Metrics

- `LLM-as-judge accuracy` **(primary)** — range: [0, 1]
  - Computed by an LLM-as-judge framework that scores both final answer correctness and step-wise derivation soundness. The metric represents the proportion of instances where the model's proof is logically complete and mathematically valid.

## Input / output format

**Input**: Two mathematical expressions f(x) and g(x) over variables x in a specified domain D, along with the inequality proof problem statement.

**Output**: For bound estimation: the optimal constant C* (sup or inf). For relation prediction: the correct relational operator (>, ≥, =, ≤, <, or none of the above), accompanied by a step-by-step derivation.

## Scoring recipe

```python
def compute_metric(predictions, gold):
    correct = 0
    for pred, gold_inst in zip(predictions, gold):
        answer_ok = (pred['answer'] == gold_inst['answer'])
        steps_ok = llm_judge_score(pred['derivation'], gold_inst['expected_steps'])
        if answer_ok and steps_ok:
            correct += 1
    return correct / len(predictions)
```

## Common pitfalls

- Models often produce correct final answers but fail to provide logically sound or complete derivations, which the LLM-as-judge framework penalizes.
- The informal natural language format lacks machine-checkable proof steps, making automated verification difficult and relying heavily on the judge model's consistency.
- Domain constraints (e.g., x_i > 0) are frequently overlooked by models, leading to invalid extremal constants.

## Evidence (verbatim from paper)

> A novel LLM-as-judge framework evaluates both final answers and step soundness, revealing that even top models like o1 achieve less than 10% overall accuracy under scrutiny, exposing a critical gap between correct final answers and sound deductive chains.

## Citation

```bibtex
@misc{sheng2025solvinginequalityproofs,
  title={Solving Inequality Proofs with Large Language Models},
  author={Sheng et al. (2025)},
  year={2025},
  note={arXiv:2506.07927}
}
```

- arXiv: 2506.07927