Combibench Eval

combibench-eval

CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics — Liu et al. (2025) (arXiv:2505.03171, 2025)

What this evaluates

This benchmark evaluates large language models on formal combinatorial mathematics reasoning within the Lean 4 proof assistant. It probes the model's ability to generate correct, compilable proof scripts and accurately solve fill-in-the-blank combinatorial problems under rigorous automated verification.

Datasets

• CombiBench — total 100; splits: test (100); repo https://github.com/MoonshotAI/CombiBench

Metrics

• pass@N (primary) — range: [0, 1]
  • pass@N measures the fraction of problems solved correctly out of N independent sampling attempts per problem. A problem is marked solved if the generated Lean 4 code compiles without errors, contains no 'sorry', defines no new axioms, preserves the original statement structure, and exactly matches or is formally provably equivalent to the ground truth answer.

Input / output format

Input: A formal Lean 4 theorem statement with proof placeholders replaced by 'sorry's, optionally accompanied by a ground truth solution for fill-in-the-blank variants.

Output: A complete Lean 4 code snippet filling the 'sorry' placeholders, followed by a proof or answer that compiles and satisfies the Fine-Eval verification criteria.

Scoring recipe

def evaluate(prediction, ground_truth, original_stmt):
    code = remove_comments(prediction)
    if 'sorry' in code or defines_new_axioms(code):
        return False
    if not lean_compiles(code):
        return False
    if not matches_structure(code, original_stmt):
        return False
    if code.answer == ground_truth:
        return True
    if lean_proves(f'code.answer == ground_truth', tactics=['rfl', 'norm_num']):
        return True
    if two_stage_enabled:
        return try_two_stage_proof(code.answer, ground_truth, max_chars=42)
    return False

Common pitfalls

• Models may cheat by commenting out all generated code to bypass Lean's compilation check, falsely appearing to pass.
• Assuming numerical or algebraic equivalence (e.g., 10/20 vs 1/2) without formal verification leads to false positives; the protocol requires explicit 'rfl'/'norm_num' proofs or a second-stage LLM proof.
• Ignoring the 42-character limit on second-stage proofs allows models to reverse-engineer ground truths, inflating scores.

Evidence (verbatim from paper)

A code that does not meet these requirements is considered a failure. Otherwise, we believe the proof is successful and check whether the solution provided by LLM and the ground truth match exactly. If the solution and ground truth are exactly matched, we believe that the model has successfully solved the problem. If not, we then try to verify that the answer that LLM predicts is equivalent to the ground truth. To avoid unnecessary LLM calls, we construct a formal statement as follows, asserting that “xx_solution = ground_truth” and try to prove it using two common tactics: ‘rfl’ and ‘norm_num’. Following PutnamBench, we also conducted a comparative experiment, replacing the corresponding sorry with ground truths and letting the model complete the proof. We report pass@N at different sample budgets as the performance metric.

Citation

@misc{liu2025combibench,
  title={CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics},
  author={Liu et al. (2025)},
  year={2025},
  note={arXiv:2505.03171}
}

• arXiv: 2505.03171