Ulam-1-Small: A 3B Model for Research Mathematics

Mathematical reasoning is not one objective.

On a closed olympiad problem, the target is a complete proof against a known reference. An elegant partial argument is still incomplete. On a research problem, the situation is different: a correct special case, a useful reduction, a counterexample, or a well-scoped obstruction may be valuable even when the original question remains unresolved.

The corresponding failures are different too. Failing to finish a closed proof costs one problem. Confidently announcing a false theorem can contaminate an entire line of work.

That distinction shaped the release of Ulam-1-Small. We did not select the checkpoint with the highest closed-proof score. We selected the checkpoint that best matched the intended use: a compact assistant for exploratory mathematics, proof-style reasoning, and research workflows in which useful progress and restraint both matter.

Ulam-1-Small is a standalone merged model. It does not require access to a private parent checkpoint or a separate PEFT adapter.

The BF16 weight shards occupy about 5.75 GiB. That is not a minimum-memory claim: model state, kernels, KV cache, graph capture, and the requested context all require additional memory. The 131,072-token architectural configuration is also not a promise that every deployment can serve that length. Practical context should be chosen from the available accelerator memory and validated on the intended workload.

The immutable release tag is v1.0.0.

The public lineage passes through Qwen2.5-3B, Qwen2.5-Coder-3B, and WeiboAI’s VibeThinker-3B before the Ulam post-training stages:

Qwen2.5-3B
  → Qwen2.5-Coder-3B
  → WeiboAI/VibeThinker-3B
  → Ulam rlvr_math full-weight stage
  → Ulam SFT checkpoint 535
  → Ulam SFT-v2 step 409
  → canonical V-SAO seed 101 adapter
  → prompt-balanced DPO checkpoint 20
  → merged standalone Ulam-1-Small

The final artifact is not a small adapter applied directly to VibeThinker. Every retained final adapter was trained and evaluated against the exact SFT-v2 step-409 parent, and the public release binds the lineage, revisions, adapter hashes, tokenizer, and merged files through provenance.json, release_manifest.json, and checksums.

Ulam-1-Small combines several training objectives rather than relying on one final fine-tuning pass:

The training views were derived from mathematical records with explicit provenance and verification boundaries. The lineage uses material from our Verified Research Reasoning Trajectories and Verified Math Olympiad Trajectories work. The public dataset repositories expose schemas and inspection samples; they do not necessarily contain every private training row used in the release.

The final DPO stage was intentionally small: 98 training preference pairs and 24 validation pairs. The pairs included correct-versus-longer-correct examples and correct-versus-wrong examples, with prompt-disjoint validation. This was not a “train until the loss stops improving” exercise. We saved a dose curve and selected an intermediate checkpoint using a separate development endpoint.

On the repeatedly inspected 83-item automatic ErdősBench development endpoint, the prompt-balanced DPO run followed a peaked curve:

Training-domain preference metrics continued to improve later in the run, while the external endpoint deteriorated. That is a useful warning for small preference datasets: terminal loss is not the same thing as the best deployment checkpoint.

The boundary around this result matters. The endpoint was repeatedly inspected during development and therefore consumed for model selection. The 7/83 result is not an unbiased generalization estimate, and all seven successful items were literature-triage labels rather than finite-exact research solutions. Its role was narrower: choose the DPO dose, reproduce that choice after a fresh model load, and then evaluate the retained checkpoints on separate release audits.

The most important release decision came from comparing two different mathematical profiles.

V-SAO checkpoint 177 was the stronger closed-proof model on SIMOBench, a 126-problem synthetic olympiad-style evaluation graded from 0 to 7. It led the released DPO checkpoint in both judging passes over the same generation bytes.

The precise conclusion is straightforward: V-SAO checkpoint 177 is the stronger checkpoint for closed, reference-backed proof completion under these audits. The released DPO checkpoint preserved about 98% of its primary total, but it did not win this evaluation.

The research-style audit produced a different profile. On the separate 226-item ErdősBench review, DPO checkpoint 20 had the highest mean score and fewer rejected self-declared strong claims:

This is not evidence that DPO broadly dominates V-SAO on research mathematics. The paired mean difference was 0.043 points per item, with a bootstrap 95% interval of [-0.062, 0.148] and a two-sided sign-flip value of p = 0.435. The aggregate advantage is uncertain.

The product-relevant signal was in the tail. Among responses that declared a strong theorem, counterexample, or comparable result, DPO had one rejected claim in 17, while V-SAO had four in 16. That subset is small and was not an independent protected experiment; a two-sided Fisher exact test gives p = 0.175. It should not be presented as a settled population-level result.

It was still operationally important. Six rows with a catastrophic or empty outcome accounted for most of the aggregate difference between the checkpoints. For a research assistant, avoiding a confidently false result can matter more than gaining a small average advantage on routine rows.

That is why we release DPO checkpoint 20 as Ulam-1-Small and retain V-SAO checkpoint 177 as the stronger closed-proof specialist. This is an objective-dependent choice, not a claim that one checkpoint is universally better.

Model releases often compress a long training and selection process into a parameter count and one benchmark score. We want Ulam-1-Small to be inspectable at a finer level.

The repository includes:

• provenance.json, recording the public model lineage and pinned revisions;
• release_manifest.json, inventorying the model, tokenizer, and source hashes;
• evaluation_results.json, exposing aggregate results, paired comparisons, and claim boundaries;
• checksums.sha256, binding the released files;
• release, security, and responsible-use notes;
• the full technical report.

The merged release also passed exact greedy-token equivalence against the parent-plus-adapter model on four public fixtures covering arithmetic, algebra, proof reasoning, and multi-turn formatting. The BF16 logit checks passed their absolute and normalized tolerances with cosine similarity above 0.9998. Fresh Transformers and vLLM smoke tests validated native loading without trust_remote_code=True.

These receipts do not prove mathematical correctness. They establish a different boundary: the public artifact is the model we intended to release, and its reported lineage and serving path can be checked.

import torch
from transformers import AutoModelForCausalLM, AutoTokenizer

model_id = "ulamai/Ulam-1-Small"

tokenizer = AutoTokenizer.from_pretrained(model_id)
model = AutoModelForCausalLM.from_pretrained(
    model_id,
    dtype=torch.bfloat16,
    device_map="auto",
)

messages = [
    {
        "role": "user",
        "content": "Prove that the sum of the first n odd integers is n squared.",
    }
]

inputs = tokenizer.apply_chat_template(
    messages,
    add_generation_prompt=True,
    tokenize=True,
    return_dict=True,
    return_tensors="pt",
).to(model.device)

with torch.inference_mode():
    output = model.generate(
        **inputs,
        do_sample=False,
        max_new_tokens=2048,
    )

completion = output[0, inputs["input_ids"].shape[-1]:]
print(tokenizer.decode(completion, skip_special_tokens=True))

For an OpenAI-compatible local endpoint, the model can be served through vLLM:

vllm serve ulamai/Ulam-1-Small \
  --dtype bfloat16 \
  --max-model-len 16384 \
  --served-model-name ulamai/Ulam-1-Small

The model may emit explicit reasoning delimiters such as <think>...</think>. Applications that display only a final answer should parse or route those spans deliberately rather than assuming they are absent. Long proof generations may also hit the configured output cap, so serving limits should be treated as part of the evaluated system rather than as an implementation detail.

Ulam-1-Small is intended for mathematical problem solving with human review, exploratory proof-style reasoning, research on compact reasoning models, and local inference through standard model-serving tools. The MIT release permits commercial and non-commercial use of the released weights, subject to the upstream notices included in the repository.

It is not a theorem-certification system. Generated proofs can contain subtle or decisive errors. A claimed theorem, refutation, or counterexample still needs independent expert review and, where possible, formal or executable verification. We have not validated this release for autonomous tool use, API orchestration, or unsupervised research publication.

The model is also compact. That is useful for deployment and experimentation, but it limits broad factual knowledge compared with much larger general-purpose systems. Mathematical citations, literature claims, and theorem statements should be checked against primary sources.

The main lesson from Ulam-1-Small is not that three billion parameters are enough for every mathematical task.

It is that checkpoint selection should match the intended loss function.

A model chosen for olympiad proof closure may not be the checkpoint we want for open-ended research assistance. A model with a slightly lower closed-proof total may be preferable when it preserves useful progress and reduces the observed rate of catastrophic overclaiming. A final training checkpoint may be worse than an intermediate dose even while the training objective continues to improve.

Those distinctions disappear when evaluation is reduced to one leaderboard number.

Ulam-1-Small is our attempt to make them explicit: publish the tradeoff, release the selected artifact, preserve the receipts, and state clearly where the evidence ends.

Explore Ulam-1-Small on Hugging Face, read the technical report, inspect the evaluation and provenance files, and test the model on mathematics that matters to you.