datasets
Training and evaluation data, with the modality, task and licence stated up front. Listed live from the Hugging Face Hub.
Mathlib-Normalized-Sexpr
Mathlib Normalized S-Expressions
Lean 4 proof states from Mathlib, paired with the tactic applied at each
step, in three representations extracted directly from the Lean kernel:
Source-faithful S-expressions of the goal and every hypothesis, as
Lean elaborated them.
Normalized S-expressions of the same state, with stable local-context
indices suitable for model input.
Annotated tactic syntax -- the original tactic's syntax tree with
identifier leaves resolved to the constants… See the full description on the dataset page: https://huggingface.co/datasets/jajostrains/Mathlib-Normalized-Sexpr.travelplanner-benchmark-normalized
TravelPlanner Benchmark (Normalized)
Normalized, typed, parquet-first packaging of the TravelPlanner benchmark for planning-centric agent evaluation.
Upstream dataset: osunlp/TravelPlanner
Upstream code: OSU-NLP-Group/TravelPlanner
Paper: TravelPlanner: A Benchmark for Real-World Planning with Language Agents
1) What is included
This dataset repo contains:
benchmark config (train/validation/test) in typed parquet.
reference_entries config: flattened reference-info… See the full description on the dataset page: https://huggingface.co/datasets/tuandunghcmut/travelplanner-benchmark-normalized.