datasets
Training and evaluation data, with the modality, task and licence stated up front. Listed live from the Hugging Face Hub.
olympiad-proof-problems
Olympiad-Proof-Problems
Dataset Description
This dataset contains mathematical problems and solutions from CSV data.
Dataset Summary
Total Examples: 39764
Format: Problem-solution pairs
Source: olympiad_proof_problems_clean.csv
Language: English
Domain: Mathematics
Data Fields
prompt: The mathematical problem statement
completion: The complete solution (including working steps)
source: Original source identifier
id: Unique identifier for each… See the full description on the dataset page: https://huggingface.co/datasets/TamasSimonds/olympiad-proof-problems.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.