Indimathbench Eval

indimathbench-eval

IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch — Biyani et al. (2025) (arXiv:2512.00997, 2025)

What this evaluates

This benchmark evaluates the ability of LLMs to autoformalize natural language mathematical problems into correct Lean 4 theorems and subsequently prove them. It probes semantic equivalence, syntactic structural similarity, and automated theorem proving success rates on Olympiad-level geometry and algebra problems.

Datasets

• IndiMathBench — total 312; splits: test (312); repo https://github.com/prmbiy/IndiMathBench

Metrics

• BEq (primary) — range: [0, 1]
  • Evaluates logical equivalence by attempting to prove each theorem using the other. The formalization is correct only if both directional proofs succeed using heuristic and LLM-guided tactics.
• GTED — range: [0, 1]
  • Measures syntactic similarity by representing Lean theorems as operator trees and computing the normalized cost of transforming the candidate theorem into the human-annotated ground truth.
• Success Rate (pass@1) — range: [0, 1]
  • Fraction of problems where the model generates a Lean-verifiable proof within a single or multi-turn interaction.

Input / output format

Input: Natural language problem statement, optionally augmented with Mathlib documentation and iterative compiler feedback.

Output: Lean 4 theorem statement (in sorry-format for autoformalization) or a complete Lean proof script.

Scoring recipe

def score_autoformalization(candidate, ground_truth):
    beq_pass = prove(candidate, ground_truth) and prove(ground_truth, candidate)
    gted_score = normalized_tree_edit_distance(candidate, ground_truth)
    return beq_pass, gted_score

def score_theorem_proving(proof_script, theorem):
    return lean_compile_and_verify(proof_script, theorem)

Common pitfalls

• Syntactic compilation success does not guarantee semantic correctness; BEq is required for logical equivalence.
• Geometry problems are significantly harder due to Mathlib's limited support for Olympiad-style geometry.
• BEq requires successful proofs in both directions; passing only one direction is insufficient.

Evidence (verbatim from paper)

Evaluating autoformalization quality presents unique challenges due to the rigorous logical nature of formal mathematical statements, where seemingly minor syntactic variations can alter meaning. To provide a comprehensive assessment, we employ two complementary evaluation metrics that have demonstrated high inter-annotator agreement with human evaluations (Liu et al., 2025b). - Bidirectional Equivalence (BEq) (Liu et al., 2025c) evaluates logical equivalence by attempting to prove each theorem using the other. Given two Lean 4 theorems in sorry-format, theorem_A and theorem_B, BEq employs a diverse set of heuristic and LLM-guided tactics to establish proofs in both directions. The formalization is deemed correct only if both directional proofs succeed, ensuring true logical equivalence rather than superficial syntactic similarity. - Generalized Tree Edit Distance (GTED) (Liu et al., 2025b) measures syntactic similarity by representing Lean theorems as operator trees and computing the normalized cost of transforming the candidate theorem into the human-annotated ground truth. Scores range from 0 to 1 per comparison, with higher values indicating greater structural correspondence.

Citation

@misc{biyani2025indimathbench,
  title={IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch},
  author={Biyani et al. (2025)},
  year={2025},
  note={arXiv:2512.00997}
}

• arXiv: 2512.00997