Proofnet Eval

proofnet-eval

ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics — Azerbayev et al. (2023) (arXiv:2302.12433, 2023)

What this evaluates

Evaluates a model's ability to translate between natural language mathematics and Lean 3 formal statements (autoformalization and informalization). It measures syntactic validity, semantic correctness, and lexical similarity to assess reasoning over undergraduate-level theory.

Datasets

• ProofNet — total 371; splits: test (-1); repo https://github.com/zhangir-azerbayev/ProofNet

Metrics

• Accuracy (primary) — range: [0, 1]
  • Percentage of generated statements that correctly match the ground truth formalization or informalization.
• Typecheck rate — range: [0, 1]
  • Proportion of generated samples that are well-formed statements in Lean's dependent type theory. Samples that simply copy the prompt are excluded from positive counts.
• BLEU — range: [0, 1]
  • BLEU-4 score with smoothing, computed after splitting both predictions and references on whitespace.
• Compile rate — range: [0, 1]
  • Proportion of generated LaTeX samples that successfully compile with pdflatex.

Input / output format

Input: Natural language theorem statement (for autoformalization) or Lean 3 formal statement (for informalization).

Output: Lean 3 code (for autoformalization) or LaTeX-formatted natural language (for informalization).

Scoring recipe

def score(preds, golds):
    typecheck_rate = sum(1 for p in preds if lean_typechecks(p) and not is_copy_from_prompt(p)) / len(preds)
    compile_rate = sum(1 for p in preds if latex_compiles(p)) / len(preds)
    accuracy = sum(1 for p, g in zip(preds, golds) if is_semantically_equivalent(p, g)) / len(preds)
    bleu = compute_bleu_4_with_smoothing(preds, golds, split_on_whitespace=True)
    return {'typecheck_rate': typecheck_rate, 'compile_rate': compile_rate, 'accuracy': accuracy, 'bleu': bleu}

Common pitfalls

• BLEU scores can decrease while actual formalization accuracy increases, making BLEU a poor guide for code/math tasks.
• Typecheck rate can be inflated by models simply copying prompt examples; the evaluation explicitly excludes prompt copies.
• Informalization compilation failures often stem from mathlib-specific Unicode characters that pdflatex does not accept, not from logical errors.

Evidence (verbatim from paper)

In addition to reporting autoformalization accuracy, we also report typecheck rate, which is the proportion of a model's samples that are well-formed statements in Lean's dependent type theory. If a model simply copies a formal statement from its prompt, we do not consider that a positive sample when calculating typecheck rate.

Citation

@misc{azerbayev2023proofnet,
  title={ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics},
  author={Azerbayev et al. (2023)},
  year={2023},
  note={arXiv:2302.12433}
}

• arXiv: 2302.12433