datasets
Training and evaluation data, with the modality, task and licence stated up front. Listed live from the Hugging Face Hub.
ProofBench
ProofBench Dataset
ProofBench is a comprehensive benchmark dataset for evaluating AI models on mathematical proof generation and verification. The dataset contains competition-level mathematics problems from prestigious international competitions, along with both AI-generated and reference solutions, expert ratings, and detailed marking schemes.
Dataset Overview
Total Problems: 435
Competitions: PUTNAM, IMO, USAMO, EGMO, APMO, TST
Years Covered: 2022-2025
AI Models:… See the full description on the dataset page: https://huggingface.co/datasets/wenjiema02/ProofBench.lean-proof-or-refute-300
Lean Proof-or-Refute 300
Lean Proof-or-Refute 300 is a compact collection of 300 formal reasoning
problems grounded in Lean 4 and Mathlib. Each problem starts from a verified
Mathlib theorem, makes one small numerical or operator mutation, and asks the
model to return either:
a Lean certificate proving the mutated proposition; or
a Lean certificate proving the exact negation of the complete proposition.
The model receives the related source theorem, a bounded source excerpt… See the full description on the dataset page: https://huggingface.co/datasets/xlr8harder/lean-proof-or-refute-300.emailbench
emailbench
Large language models (LLMs) are becoming foundational to email security products. Increasingly, they power classification, threat detection, triage, and analyst workflows. While hundreds of public benchmarks measure general reasoning and cybersecurity, none are designed to measure whether an LLM understands email communication and email security as first-class domains.
emailbench fills that gap. It is a compact, high-quality benchmark for email understanding, built… See the full description on the dataset page: https://huggingface.co/datasets/proofpoint-ai/emailbench.single-turn-eval-stage1_proof_pr_delta_variants-n32
Single-turn eval — violetxi/stage1_proof_pr_delta_variants
Generated by teaching/inference/single_turn_eval_vllm.py. One row per problem; samples is the list of model responses, scores is per-sample correctness, and mean/best/worst are the aggregates used by mean@N / best@N / worst@N.
Eval results (n_samples_per_example = 32)
Overall
metric
value
n_examples
1006
mean@32
0.1922
best@32
0.4175
worst@32
0.0457
pass_rate
0.4175… See the full description on the dataset page: https://huggingface.co/datasets/violetxi/single-turn-eval-stage1_proof_pr_delta_variants-n32.
