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

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

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

• arXiv: 2506.07927