ProofNetVerif is a benchmark to evaluate both reference-based and reference-free metrics for statement autoformalization introduced in
Improving Autoformalization using Type Checking. This benchmark is compatible with Lean v4.8.0.
Reference-based metric evaluation:
Input: lean4_formalization, lean4_prediction
Output: correct
Reference-free metric evaluation:
Input: nl_statement, lean4_prediction
Output: correct
Note: Developing an accurate… See the full description on the dataset page:
https://huggingface.co/datasets/PAug/ProofNetVerif.
