Mo Int 20 Eval

mo-int-20-eval

Proving Olympiad Algebraic Inequalities without Human Demonstrations — Wei et al. (2024) (arXiv:2406.14219, 2024)

What this evaluates

Evaluates the ability of automated theorem provers and LLMs to formally prove complex algebraic inequalities at the International Mathematical Olympiad level using a deductive search engine in Lean.

Datasets

• MO-INT-20 — total 20; splits: test (20)

Metrics

• number of solved problems (primary) — range: other
  • Count of problems successfully proven within the 90-minute time limit out of the total 20 problems.

Input / output format

Input: Algebraic inequality problems translated into Lean formal language.

Output: A complete formal proof in Lean that successfully verifies the inequality.

Scoring recipe

solved_count = 0
for problem in test_set:
    proof = prover.generate_proof(problem, time_limit=90*60)
    if lean_verify(proof) == "success":
        solved_count += 1
return solved_count

Common pitfalls

• Problems are strictly limited to a 90-minute solving time per instance.
• LLM-based provers may fail due to context length limits when expression trees grow too large during search.
• Training data contamination is a concern, though authors verified test problems are absent from training sets.

Evidence (verbatim from paper)

We evaluate AIPS on an Olympiad-level algebraic inequality problem test set. It outperforms the state-of-the-art methods in terms of the number of solved problems, demonstrating the strong algebraic intuitions developed by the learned value network.

Citation

@misc{wei2024provingolympiad,
  title={Proving Olympiad Algebraic Inequalities without Human Demonstrations},
  author={Wei et al. (2024)},
  year={2024},
  note={arXiv:2406.14219}
}

• arXiv: 2406.14219