Datasets · Benchmarks · Verifiers

Find where reasoning fails.
Train the fix.

Ulam builds reasoning datasets that preserve the evidence between prompt and answer: attempts, proof units, tool calls, negative traces, critiques, repairs, preferences, and verifier outcomes. Inspect our public releases or commission reviewed corpora, private holdouts, reward-ready exports, and original mathematics problem sets from AIME through open-research difficulty.

Explore Verified Reasoning See ErdosBench Discuss data access
1,000+trajectory research program · 3 public inspection records
20,000+tiered OlympiadNet records across reviewed and candidate layers
57,648ArxivNet canonical proof-process records
100,000+internally created, unpublished private math problems

Flagship reasoning datasets and private mathematics problems

From inspectable public schemas to large candidate layers and reviewed private packs—built for training, criticism, verification, and evaluation rather than answer-only supervision. Our original problem catalogue spans exact-answer competition mathematics, graduate and PhD problems, verifier-backed RL tasks, and open research.

Research proof processes

Verified Research Reasoning

1,000+ trajectory program

Proof-process data that records where research reasoning becomes valid, conditional, incomplete, or wrong: dependency-linked proof units, gaps, first-bad-step labels, negative traces, rewards, critiques, repairs, preferences, and adversarial tests.

The public inspection release includes 3 canonical trajectories, 29 PVUs, 13 negative traces, 17 evaluation tasks, schema, transcripts, and validators. Machine-checkability applies only where indicated.

Public inspection release · Licensed packs
Inspect Verified Reasoning →
Olympiad proofs · SFT · RLVR

OlympiadNet-Math

20,000+ tiered records

Proof and final-answer data with source solutions kept separate from model attempts, plus proof units, negative traces, preferences, adversarial tests, review queues, and promotion gates.

Strict RLVR rows are an explicitly promoted subset—not a label for the whole corpus. The public release provides 10 inspection examples, schema, and quality-gate definitions.

Public inspection release · Tiered private corpus
Inspect OlympiadNet →
Research corpus · SFT · PRM

ArxivNet — arXiv Math Blueprints

57,648 canonical records

Turns 5,387 TeX source files into structured proof-process data for long-context SFT, proof reconstruction, theorem dependencies, process supervision, critic training, preferences, and adversarial verifier tests.

April 2026 build: 115,296 SFT rows, 166,817 process-step candidates, 159,329 negative traces, 57,648 preference pairs, and 115,296 adversarial tests. Structural validation does not establish mathematical truth.

Large candidate layer · Review required
Discuss ArxivNet access →
AIME · Olympiad · Graduate · Research

Private Mathematics Problems

100,000+ internally created problems

Original, unpublished private mathematics problems for training and evaluation—from AIME and olympiad level through graduate, PhD, and research-level mathematics. Deliveries can mix exact-answer problems, proof tasks, math problems with executable verifiers for RL, and entirely open questions.

  • AIME++ samples exact-answer tasks across AIME, AIME Hard, graduate, and researcher tiers.
  • Math RL Tasks samples graduate- and research-level math problems packaged with executable verifiers and RL environments.
  • SOTA Math samples open-research problems, milestone-based tasks, and bounded counterexample searches.
Private catalogue · Public samples
Discuss problem-set access →

Benchmarks and environments

The evaluation layer shows whether a model can use the data: reason under uncertainty, construct valid proofs, and act correctly through tools.

Research benchmark

ErdősBench

226 research candidates testing obstruction finding, counterexamples, finite experiments, theorem use, proof gaps, partial progress, and calibrated claims.

14-problem public smoke test; private full evaluation.

Explore ErdősBench →
Olympiad benchmark

SimoBench

126 synthetic olympiad-style problems, selected from 1,260 variants, with reference solutions and 0–7 proof scoring for valid, partial, and false solves.

Mathematical grading, not machine-checked formal proof.

Explore SimoBench →
Open Math RL Environments

Math RL Tasks

Graduate- and research-level mathematics problems packaged as executable RL environments, with exact, structured-output, witness, construction, and certificate verifiers.

Open samples spanning foundational, medium-to-hard, and frontier research-math task families.

Explore Math RL Tasks →

Training signals beyond final answers

Use inspectable public data, prover-backed traces, or a private build targeted to your model's actual failures.

LLM benchmarks · Executable RL

LLM benchmark-derived RL tasks

Clean-room task families turn Terminal-Bench, Terminal-Bench Science, GPQA Diamond, Humanity's Last Exam, CritPt, SciCode, and GDPVal capability surfaces into executable environments. The catalogue also covers document agents, banking, cybersecurity, long-context reasoning, and reliability.

These are synthetic or task-derived environments—not redistributed benchmark questions. Rewards use exact checks, schemas, certificates, simulators, or stateful verifiers by family.

Browse task families →
Formal proof traces

UlamAI Prover + LLM

LLMs propose tactics or proof edits; Lean checks them. Retain proof states, premise retrieval, accepted and rejected actions, errors, repairs, backtracking, and terminal outcomes.

Useful for tactic SFT, critics, proof repair, preference data, RLVR, and regression. Formal status applies to Lean-accepted proof steps.

View UlamAI Prover →
Private and targeted

Custom failure-driven builds

Bring representative attempts, tool logs, proofs, or evaluation results. Ulam localizes recurring failures and returns positives, negatives, critiques, repairs, preference pairs, verifier contracts, and sealed holdouts.

Delivered as JSONL or Parquet with stable IDs, provenance, splits, quality status, and training-view exports.

One improvement loop

Benchmarks reveal the failure. Verifiers make it measurable. Training data turns the repair into a repeatable signal.

problem → attempt/action → observation → verifier verdict → first failure → critique/repair → training export

01 MeasureRun ErdősBench, SimoBench, MathCode, or customer tasks.
02 DiagnoseLocate the first meaningful error and its dependencies.
03 BuildCreate positives, negatives, repairs, preferences, and variants.
04 VerifyAttach deterministic, Lean, simulator, or reviewer outcomes.
05 Re-runMeasure improvement on sealed holdouts and refreshed tasks.

Dataset catalogue and technical details

Verification and intended use determine whether an asset belongs in training. Derived task families are clean-room environments inspired by a benchmark's capability surface, not copies of its original questions.

Compare products, verification boundaries, and access

Asset Best for Verification boundary Access
Verified Research Reasoning
1,000+ trajectory program		 RLVR, process supervision, critics, first-bad-step detection, proof repair Review and machine-checkability recorded per unit; not blanket formal verification 3 public inspection records · Licensed reviewed packs and holdouts
OlympiadNet-Math
20,000+ tiered records		 Olympiad SFT, proof attempts, preference data, promoted RLVR tasks Quality tiers and promotion gates; only a strict subset is positive-weight RLVR 10 public inspection records · Tiered private corpus
ArxivNet
57,648 canonical records		 Long-context math SFT, reconstruction, PRM, critics, preferences Structurally validated candidate layer; mathematical review required Private candidate and review-ready exports
Private Mathematics Problems
100,000+ internally created, unpublished problems		 AIME and olympiad training or evaluation, graduate and PhD reasoning, RLVR, and open-research work Exact-answer contracts where appropriate; RL tasks are math problems with executable verifiers; open problems use scoped computation and expert review Private packs and holdouts · Public samples: AIME++, Math RL Tasks, and SOTA Math
AIME++
Exact-answer mathematics		 Competition-to-hard exact-answer RLVR, scalable curricula, and sealed private evaluation Integer normalization and exact match; boxed-answer parsing is reported separately Private packs · View sample
AIME-Graduate
Graduate mathematics with an exact-answer contract		 Graduate-level RLVR with a deterministic terminal reward Integer normalization and exact match; boxed-answer parsing is reported separately Private packs · View sample
AIME-Researcher
Research-level mathematics with an exact-answer contract		 Research-level exact-answer RLVR and frontier difficulty profiling Integer normalization and exact match; boxed-answer parsing is reported separately Private packs · View sample
Math RL
Foundational research-oriented RL suites		 Broad mathematical curricula and deterministic verifier integration Task-specific exact, structured-output, or certificate verifiers Private suites · View sample
MathH RL
Medium-to-hard research-oriented RL suites		 Verifier-backed capability evaluation and advanced certificate curricula Task-specific exact and certificate verifiers, including theorem-tactic and structured-witness checks Private suites · View sample
MathR RL
Frontier research-oriented RL suites		 Research-math agent training, difficult private evaluation, and high-value certificate generation Strict task-specific exact, witness, construction, and certificate verifiers Private suites · View sample
CritPt-derived
Physics RL environments		 Benchmark-targeted post-training and clean-room private evaluation Deterministic or exact checks, packaged verifier code, executable tests, and schema checks Private Python environments · View sample
GDPVal-derived
Synthetic professional-work RL environments		 Long-horizon professional agents, artifact production, quantitative reasoning, and cross-file consistency Deterministic dense rewards across correctness, instruction following, traceability, artifact integrity, consistency, quality, and safety Private Harbor-compatible environments · View sample
GDP.pdf-derived
Long-horizon multi-document agent RL		 Retrieval, rule reconciliation, quantitative reasoning, evidence attribution, optimization, and structured decisions Deterministic dense and sparse grading requires correct values, physical-page or source-record evidence, and passing prerequisite chains Private DocumentEnv delivery · View sample
GPQA Diamond-derived
Graduate-science RL environments		 Benchmark-targeted post-training, clean-room evaluation, and repeatable science-reasoning rewards Deterministic or exact checks, packaged verifier code, executable tests, and schema checks Private Harbor-compatible environments · View sample
Humanity's Last Exam-derived
Frontier-reasoning environments		 Benchmark-targeted post-training, clean-room evaluation, and difficult reasoning curricula Deterministic or exact checks, packaged verifier code, executable tests, and schema checks Private Harbor-compatible environments · View sample
Terminal-Bench-derived
Hard terminal-agent environments		 Terminal-agent post-training and clean-room private evaluation Deterministic or exact checks, packaged verifier code, executable tests, and structured-output checks Private Harbor-compatible environments · View sample
Terminal-Bench-Science-derived
Scientific-agent environments		 Scientific-agent RL, hidden-instance generalization, reusable solver evaluation, and mathematical science Exact checks, certificate or witness validation, stateful simulator scoring, executable tests, and schema checks Private Harbor-compatible environments · View sample
Terminal-Bench Science Hard
Hard scientific-agent RL environments		 Numerical implementation, experimental design, system identification, uncertainty-aware control, transfer, and robustness Hidden numerical packets and executable scientific-campaign evaluators with aggregate, robustness, integrity, and protocol gates Private scientific environments · View sample
SciCode-derived
Scientific coding RL environments		 Scientific coding-agent RL and weighted numerical evaluation Weighted numerical checks, executable tests, and structured-output checks Private Python environments · View sample
SciDiamond-derived
Synthetic advanced-science RL		 Advanced-science RLVR curricula and locked-test evaluation Deterministic exact four-option rewards, packaged verifier code, and executable tests Private Harbor-compatible environments · View sample
Tau-Banking-derived
Stateful banking-agent environments		 Stateful tool-use RL, banking-policy compliance, and database-state evaluation Deterministic outcome and compliance checks, packaged verifier code, and executable tests Private Python environments · View sample
CyberSec-derived
Synthetic cybersecurity repair environments		 Defensive coding-agent RL and local incident or security-system repair Deterministic partial-credit checks, packaged verifier code, and structured-output checks Private Python environments · View sample
AA-LCR-derived
Long-context reasoning environments		 Long-context structured reasoning, precise extraction, and private-gold evaluation Deterministic JSON verification with shaped field rewards and strict pass/fail Private Python environments · View sample
AA-Omni-derived
Factual-reliability and abstention environments		 Factual-reliability RL, calibration, and abstention behavior Deterministic verification with correct, incorrect, partial, and not-attempted outcomes Private Python environments · View sample
ErdősBench
Research reasoning benchmark		 Research behavior, proof gaps, counterexamples, calibrated progress Judge and proof audit; not formal theorem certification Public smoke test · Private full benchmark
SimoBench
Olympiad proof benchmark		 Olympiad proof construction, partial credit, false-solve analysis 0–7 mathematical grading against references Public research benchmark · Private refreshes
Custom data packs Model-specific weaknesses and private regression suites Verifier contract designed around the target task Private engagement

Training views: SFT, DPO, critic and repair data, RLVR/GRPO tasks, process-reward steps, private evaluation, and regression tests.

RL tasks: math problems with executable verifiers, explicit answer contracts, reward rules, adversarial checks, and private train/development/holdout variants.

Environment delivery: task families can use Harbor-compatible containers, Python agent environments, stateful simulators, or custom Gym-style APIs while private manifests and answer keys remain protected.

Start with a dataset you can inspect.

Review Verified Reasoning, OlympiadNet, AIME++, Math RL Tasks, SOTA Math, and the benchmark-derived task samples—or discuss private mathematics problems, ArxivNet, larger reviewed packs, sealed holdouts, and custom data built around your model's actual failures.

Discuss data access Browse public datasets