Proofnet Eval

---
name: proofnet-eval
description: 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. Use when the user wants to benchmark on ProofNet, or asks about evaluating this task. Reports Accuracy.
metadata:
  skill_kind: dataset_eval
  source_arxiv: 2302.12433
  bibtex_key: [REDACTED]
  confidence: high
---

# 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

```python
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

```bibtex
@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