Dataset · Hugging Face

PAug/ProofNetVerif

Name: ProofNetVerif
Creator: PAug
License: mit
Keywords: task_categories:text-generation, task_categories:translation, language:en, license:mit, size_categories:1K<n<10K, format:parquet, modality:text, library:datasets, library:pandas, library:mlcroissant, library:polars, arxiv:2406.07222, region:us, code

ProofNetVerif 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. Tasks 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… See the full description on the dataset page: https://huggingface.co/datasets/PAug/ProofNetVerif.

View on Hugging FaceReport an issue

Author / organization	PAug
License (as declared)	mit
Downloads	221 (as reported by Hugging Face)
Likes	1
Created	5 February 2025
Last updated at source	24 March 2025

code

Embed this entry

<iframe src="https://silytics.si/embed/item/6dea769b-6007-42c4-8bb6-4363b52d87e8" width="420" height="190" style="border:0" loading="lazy" title="Silytics entry"></iframe>

Free, no tracking. More about feeds and embeds.

Recent changes

16 Oct 2026 Description: ProofNetVerif 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. → ProofNetVerif 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.

Changes detected by Silytics between refreshes of the source.

More from PAug

PAug/ProofNetSharpDataset

Silytics shows public metadata from Hugging Face and links to the original. Information may be incomplete or out of date. Last refreshed 16 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.