datasets
Training and evaluation data, with the modality, task and licence stated up front. Listed live from the Hugging Face Hub.
MathVista
Dataset Card for MathVista
Dataset Description
Paper Information
Dataset Examples
Leaderboard
Dataset Usage
Data Downloading
Data Format
Data Visualization
Data Source
Automatic Evaluation
License
Citation
Dataset Description
MathVista is a consolidated Mathematical reasoning benchmark within Visual contexts. It consists of three newly created datasets, IQTest, FunctionQA, and PaperQA, which address the missing visual domains and are tailored to evaluate logical… See the full description on the dataset page: https://huggingface.co/datasets/AI4Math/MathVista.MathVerse
Dataset Card for MathVerse
Dataset Description
Paper Information
Dataset Examples
Leaderboard
Citation
Dataset Description
The capabilities of Multi-modal Large Language Models (MLLMs) in visual math problem-solvingremain insufficiently evaluated and understood. We investigate current benchmarks to incorporate excessive visual content within textual questions, which potentially assist MLLMs in deducing answers without truly interpreting the input diagrams.
To… See the full description on the dataset page: https://huggingface.co/datasets/AI4Math/MathVerse.IneqMath
Solving Inequality Proofs with Large Language Models
Introduction
Inequality proving, crucial across diverse scientific and mathematical fields, tests advanced reasoning skills such as discovering tight bounds and strategically applying theorems. This makes it a distinct and demanding frontier for large language models (LLMs), offering insights beyond general mathematical problem-solving. Progress in this area is hampered by existing… See the full description on the dataset page: https://huggingface.co/datasets/AI4Math/IneqMath.mathlib_handler_benchmark_410This dataset is used in the paper Assisting Mathematical Formalization with A Learning-based Premise Retriever. It contains data for training and evaluating a premise retriever for the Lean theorem prover.
The dataset is described in detail in the GitHub repository. It consists of proof states and corresponding premises from the Mathlib library. The data is designed to train a model to effectively retrieve relevant premises for a given proof state, assisting users in the mathematical… See the full description on the dataset page: https://huggingface.co/datasets/ruc-ai4math/mathlib_handler_benchmark_410.ai4math-lean
ai4math-lean
21 Lean 4 formal mathematics datasets with machine-verified labels.
Every problem has been verified against lean-server v4.21.0 on UVA's HPC cluster.
Results are embedded in each row as both structured verification JSON and flattened convenience columns.
Quick Start
from datasets import load_dataset
# Load a single dataset
ds = load_dataset("charliemeyer2000/ai4math-lean", "deepseek_prover")
# Load a large dataset with streaming
ds =… See the full description on the dataset page: https://huggingface.co/datasets/charliemeyer2000/ai4math-lean.AI4Math_MathVista-baseline_7B-rollout8AI4Math_MathVista-multimodal-rollout8AI4Math_MathVista-multimodal_7B-rollout8AI4Math_MathVerse-baseline-rollout8AI4Math_MathVerse-multimodal-rollout8AI4Math_MathVista-baseline-rollout8AI4Math_MathVerse-multimodal_7B-rollout8AI4Math_MathVerse-baseline_7B-rollout8