Ulam builds proof-process datasets, private math benchmarks, and verifier-backed RLVR environments for teams steering reasoning models with SFT, reward modeling, process supervision, RLVR, and private evaluation.
The product is a full improvement loop: create the right data, measure proof reliability on hidden tasks, convert failures into trainable objects, and serve verifier rewards through UlamGym while keeping private rubrics and holdouts sealed.
Start with data, measure with private benchmarks, and close the loop with verifier-backed RLVR tasks. Each product can stand alone; together they create a recurring training signal for mathematical reasoning.
Research-level Erdős-like problems for evaluating mathematical research behavior: finite experiments, obstruction finding, counterexamples, proof-gap detection, partial progress, and calibrated uncertainty.
The public repository exposes the format; the full benchmark, hidden tasks, rubrics, and answer keys stay private.
Hidden Olympiad-style rounds with 0-7 proof rubrics, answer/proof separation, blind judging, and traps for equality cases, exact constants, unsupported geometry lemmas, invalid bounds, and number-theory shortcuts.
Built to distinguish “right answer” from valid proof and to surface trainable false-solve patterns.
One-time or recurring data builds from research trajectories, OlympiadNet-Math, arXiv blueprints, agentic workflows, and newly generated problems targeted to a model’s observed reasoning weaknesses.
Delivered with stable IDs, splits, metadata, verifier status, holdout notes, and training-view exports.
Verifier-backed reward environments for proof repair, counterexample search, premise selection, lemma graphs, exact-answer olympiad tasks, statement fidelity, and informal proof critique.
Trainers see prompts, rewards, vectors, and redacted replays; hidden manifests and rubrics remain server-side.
Benchmarking Research: monthly private rounds with 200 hidden or refreshed problems, 4–6 model configs, proof-validity judging, skill regressions, false-solve taxonomy, raw JSONL outputs, judge cards, and technical readouts every 2–3 weeks.
Ulam can license existing corpora or build custom packs around a model's observed weaknesses. Every pack is designed to be usable by training teams: schema docs, stable IDs, data splits, verifier status, and holdout notes.
| Asset | Scale | Best Use | How It Steers the Model | Status |
|---|---|---|---|---|
| Research-level trajectories | 1,000+ trajectories | Strict and near-strict RLVR pilots, process supervision, proof repair, private evals | Teaches search, failed branches, critiques, repairs, final proofs, and preference comparisons. | High-quality trajectories |
| April 2026 arXiv math build | 57,648 canonical records from 5,387 TeX files | Long-context SFT, theorem dependency extraction, proof reconstruction, research triage | Supplies proof-process scaffolds, negative traces, PRM steps, adversarial tests, and review queues. | Candidate / review required |
| OlympiadNet-Math | 20,000+ problems | Final-answer training, proof-validity tasks, verifier development, hidden benchmark variants | Separates answer-level rewards from proof-heavy reasoning where edge cases and exact constants matter. | Reviewed + candidate layers |
| Agentic workflow rows | 3,395 rows | Tool-conditioned behavior, workflow SFT, verifier-backed tasks, preference training | Trains models to condition on tool observations, structured outputs, verifier feedback, and task state. | Verifier metadata included |
Build SFT, preference, proof-repair, counterexample, and verifier rows around the exact skills a model lacks: rigor, calibration, theorem use, edge cases, or tool-conditioned reasoning.
Run private benchmark rounds that score final answers separately from proof correctness and identify the first wrong inference rather than only checking answer resemblance.
Use UlamGym as a verifier-only reward API: public prompts for policy rollouts, hidden manifests for scoring, scalar rewards, reward vectors, strictness labels, and redacted replays.
Convert model failures into new SFT rows, DPO pairs, proof-critic prompts, RLVR tasks, and held-out variants for the next benchmark round.
High-quality trajectories from attempts on open Erdős-style problems and other open problems from arXiv. These traces are built for hard reasoning, failure localization, verifier-backed scoring, and private evaluation tracks.
5,387 local TeX files were transformed into a proof-process scaffold: SFT rows, RLVR task rows, PVU/PRM steps, negative traces, preference pairs, adversarial tests, and review queues.
| Generated View | Rows | Notes |
|---|---|---|
| Canonical records | 57,648 | Rich proof-process records under the Ulam RLVR schema. |
| SFT rows | 115,296 | Flattened supervised examples for proof-style and critique-style training. |
| RLVR task rows | 115,296 | Coarse verifier/reward scaffolds; not yet strict verified reward data. |
| PVU / PRM step rows | 166,817 | Proof Verification Unit and process-reward-model training candidates. |
| Negative traces | 159,329 | Invalid, partial, or adversarial proof-process traces for critique and judge training. |
| Preference pairs | 57,648 | Comparison data for reward modeling and preference optimization. |
| Adversarial tests | 115,296 | Stress tests for verifier and judge behavior. |
OlympiadNet-Math is our main math olympiad corpus. V1 is immediately useful for final-answer training and RLVR; V2 targets harder proof/source gaps and is currently a large candidate layer plus review queue.
| Dataset | Rows | Strict RLVR | SFT / Candidate Use | Summary |
|---|---|---|---|---|
| OlympiadNet-Math v1 | 12,911 reviewed rows | 828 strict positive-weight rows | 12,083 candidate / zero-weight rows | Final-answer oriented, simpler verifier contracts, viable now for supervised final-answer and proof-style SFT. |
| OlympiadNet-Math v2 | 9,661 canonical rows | 34 promoted rows | 6,213 source-solution rows; 1,014 reviewed generated candidates; 2,075 newly solved sidecar candidates | Proof/source-gap oriented. Valuable for filtered SFT and promotion work, but not a clean gold RLVR set yet. |
RLVR: use the v1 strict train subset plus the 34 promoted v2 rows.
SFT: use Reviewed-v1 preferentially, and filtered v2 source-solution / generated-candidate rows with explicit quality caveats.
V2 candidates need independent adjudication, answer/solution reconciliation, verifier contracts, adversarial tests, and explicit eligible_for_rlvr=true before strict RLVR use.
The workflow corpus is SFT/RLVR-ready for tool-conditioned assistant behavior, structured observations, verifier-backed tasks, and preference-pair training after RLVR.
Four-way split: train 2,332, eval_id 291, eval_ood 480, and sample_preview 292. Curriculum tags run from initial to core to post.
Rows carry flat messages arrays, token estimates, length buckets, tool-use IDs, and observation turns that teach the model to condition on tool output.
All structural invariants pass, verifiers are green on 3,395 golden and 4,863 adversarial checks, and contamination checks are clean on six hard OOD axes.
1,513 rows include preference pairs for DPO/IPO after RLVR. Negative traces are verifier-ready but not interleaved as full trajectories, which is suitable for RLVR and should be flagged before trajectory-level DPO use.
Teams can start with one-time data access, a custom dataset build, a private benchmark track, or UlamGym access. The strongest setup combines all three: data, recurring evaluation, and verifier-backed RL tasks.
Research trajectories, OlympiadNet-Math, arXiv blueprints, agentic workflow rows, or custom packs targeted to a model's failure modes. Delivered with stable IDs, metadata, splits, samples, and verifier-status notes.
Private benchmark refreshes, proof-level judging, 4–6 model configs, skill regressions, false-solve taxonomy, judge cards, and a technical readout every 2–3 weeks.
Verifier-only reward API, prompt/export bundle, hidden manifests, redacted trainer replays, reward vectors, usage metering, and monthly RLVR task refresh from benchmark failures.
A model team selects target skills and submits checkpoints or configs. Ulam runs private tasks, judges proof validity, identifies trainable failures, exports SFT/preference/RLVR artifacts, and serves the next round through UlamGym while keeping hidden verifier internals private.
Ulam data packs are meant to be used directly by model and RL teams. The same canonical records can be exported as SFT rows, RLVR tasks, process-reward steps, proof-critic prompts, preference pairs, private eval items, or Gym prompt rows.
Problem IDs, source class, domain, difficulty, normalized statement, expected final answer when available, source or reference solution, proof outline, and checker or reviewer status.
Attempts, failed branches, first-bad-step labels, critique notes, repair rationales, counterexamples, final proofs, and preference pairs for good vs. bad reasoning branches.
Strictness labels, reward-policy tags, verifier type, hidden-manifest references, adversarial checks, quality gates, eligible-for-RLVR flags, and scorer-safe diagnostic fields.
Train/eval/holdout splits, decontamination notes, retired benchmark items, public-inspection samples, private answer keys, and upgrade paths from candidate rows to verified reward data.
| Dataset family | Included signal | Training views | Holdout / verifier note |
|---|---|---|---|
| Research trajectories | Open-problem search, failed branches, critiques, repairs, final proof assets, preference comparisons. | SFT traces, proof-repair rows, DPO pairs, process-reward steps, private research evals. | Best for high-signal reasoning work where partial progress and proof hygiene matter. |
| OlympiadNet-Math | Final-answer and proof-oriented problems, domain tags, difficulty bands, reference solutions, verifier candidates. | Answer-level RLVR, proof-style SFT, judge training, Synthetic IMO-style hidden variants. | Final-answer problems are easier to score automatically; proof-heavy tasks need proof-validity grading. |
| arXiv math blueprints | Theorem/proof candidates, proof units, dependency scaffolds, negative traces, adversarial tests, review queues. | Long-context SFT, theorem dependency extraction, proof reconstruction, critique, research assistant training. | Experimental TeX-derived layer; valuable scaffold, upgraded through human/domain review or formal checks. |
| Agentic workflows | Messages, tool observations, verifier metadata, golden/adversarial checks, preference pairs, OOD splits. | Tool-use SFT, workflow RLVR, verifier-conditioned behavior, post-RL preference training. | Useful when the target model must reason with tools, observations, and structured task state. |
Delivery: JSONL or Parquet, schema notes, stable IDs, source metadata, split manifests, sample loaders, score/export scripts, and verifier-status columns.
Custom builds: target a model’s failures directly — geometry overclaims, wrong constants, missing equality cases, invalid divisibility steps, weak counterexample search, or tool-use brittleness.
Start with the public research schema repository and ErdosBench: inspect examples, review how canonical records flatten into RLVR/SFT/PRM views, and test the benchmark format. Commercial training packs, private holdouts, reviewer notes, hidden verifier manifests, and larger corpora are available under separate access terms.