ulamai-Ulam-1-Small-GGUF

GGUF Files for Ulam-1-Small

These are the GGUF files for ulamai/Ulam-1-Small.

Downloads

Note from Flexan

I provide GGUFs and quantizations of publicly available models that do not have a GGUF equivalent available yet, usually for models I deem interesting and wish to try out.

If there are some quants missing that you'd like me to add, you may request one in the community tab. If you want to request a public model to be converted, you can also request that in the community tab. If you have questions regarding this model, please refer to the original model repo.

You can find more info about me and what I do here.

Ulam-1-Small

Ulam-1-Small is a 3.086-billion-parameter mathematical reasoning model developed by Ulam AI. It is a standalone BF16 Transformers model.

Built with Qwen. The model lineage includes Qwen2.5-3B, Qwen2.5-Coder-3B, and WeiboAI/VibeThinker-3B. Upstream lineage and modifications are recorded in NOTICE and provenance.json.

The release is aimed at exploratory mathematical problem solving and proof-style reasoning. It is not a theorem-certification system: strong claims, counterexamples, and purported proofs require independent expert review.

✅ Technical Report

Model details

The model was selected for research-oriented use rather than for closed olympiad proof completion. V-SAO checkpoint 177 was stronger on both SIMOBench judging passes, while checkpoint-20 DPO had the highest mean in the 226-item ErdosBench audit and a safer observed tail among self-declared strong claims. This is an objective-dependent product decision, not a claim that DPO checkpoint 20 dominates all mathematical tasks.

Quick start with Transformers

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))

The checkpoint may emit explicit reasoning delimiters such as <think>...</think>. Applications that expose only a final response should parse or route those spans deliberately rather than assuming they are absent.

Serving with vLLM

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

Example OpenAI-compatible request:

curl http://localhost:8000/v1/chat/completions \
  -H 'Content-Type: application/json' \
  -d '{
    "model": "ulamai/Ulam-1-Small",
    "messages": [{"role": "user", "content": "Solve x^2 - 5x + 6 = 0."}],
    "temperature": 0,
    "max_tokens": 2048
  }'

The 131,072-token architectural setting does not imply that every deployment can serve that length. Choose --max-model-len from available accelerator memory and validate it for the intended workload. Long proof generations may hit the configured output cap.

Release validation

The merged release passed exact greedy-token equivalence against the parent-plus-adapter model on four public fixtures covering arithmetic, algebra, proof reasoning, and 762-token multi-turn context formatting. Every fixture also passed BF16 absolute and normalized logit tolerances with cosine similarity above 0.9998. A native Transformers GPU smoke test used the 2,048-token quick-start cap, and a fresh vLLM 0.25.1 load passed /health, /v1/models, and /v1/chat/completions. Transformers completed at EOS after 1,387 new tokens with trust_remote_code=False; vLLM served the model natively as Qwen2ForCausalLM while configured with a 16,384-token serving window. See equivalence_receipt.json, transformers_smoke_receipt.json, and vllm_smoke_receipt.json.

The GPU validation host was an NVIDIA DGX Spark with an NVIDIA GB10 and 121 GiB of host-visible unified memory. The Transformers run used Python 3.12.13, PyTorch 2.11.0+cu130, and Transformers 5.13.1. This is a tested compatibility configuration, not a minimum-memory claim. The BF16 weight shards alone occupy about 5.75 GiB; model state, CUDA kernels, KV cache, graph capture, and the requested context require additional memory. A minimum accelerator configuration has not yet been characterized.

Intended uses

• mathematical problem solving with human review;
• exploratory proof-style and research reasoning;
• research on compact reasoning models;
• local inference through standard Transformers or vLLM APIs;
• commercial and non-commercial use under the MIT License.

Out-of-scope uses

• treating generated proofs, theorem claims, or counterexamples as formally verified;
• unsupervised theorem announcements or autonomous research publication;
• high-stakes medical, legal, financial, or safety decisions;
• factual citation without checking primary sources;
• tool calling, API orchestration, or autonomous agents without separate testing;
• redistributing benchmark prompts, references, private reviewer material, or hidden evaluations;

See RESPONSIBLE_USE.md for deployment guidance.

Training lineage

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 released artifact is not the checkpoint-20 adapter applied directly to VibeThinker. Every retained final adapter was trained and evaluated against the exact SFT-v2 step-409 parent. The release manifest binds the public files to the parent lineage and adapter hashes.

Training datasets

The training lineage uses material derived from:

• ulamai/verified-research-reasoning-trajectories: research-level proof-process, review, reward, and preference views;
• ulamai/verified-math-olympiad-trajectories: directly used olympiad and mathematical trajectory material transformed into supervised and verifier-backed training views.

The public repositories contain inspection samples and schemas, not necessarily every private training row. Exact public revisions and their role in the release are recorded in provenance.json.

Post-training objectives

The full pipeline combines:

• full-weight outcome learning;
• supervised proof refinement;
• verified reward optimization;
• reviewed process supervision;
• privileged-prefix distillation;
• verified direct preference optimization.

The final DPO training set contained 98 preference pairs, with 24 validation pairs. Checkpoint 20 was selected from a dose curve rather than from terminal training loss alone.

Evaluation

SIMOBench

SIMOBench contains 126 synthetic olympiad-style problems graded from 0 to 7, for a maximum of 882. Each checkpoint received one stochastic generation per problem at temperature 0.7, top-p 0.95, and a 65,536-token output allowance.

The primary paired comparison between V-SAO and DPO is 21 V-SAO wins, 12 DPO wins, and 93 ties, for a 14-point V-SAO margin. Both passes were model-assisted single-judge audits of byte-identical generations. They agree on the leader but differ materially in totals; no inter-rater agreement statistic is available.

ErdosBench

The separate 226-item research audit uses A/B/C/D/F/M grades mapped to 4/2.7/1.7/1/0/0 points.

For DPO versus V-SAO, the paired mean difference is 0.043 points per item, with an item-bootstrap 95% interval of [-0.062, 0.148] and a two-sided sign-flip p=0.435. The aggregate mean difference is therefore uncertain. The two-sided Fisher exact test for the observed strong-claim rejection counts gives p=0.175; under independent Jeffreys priors, the posterior probability that DPO's rejection rate is lower is 0.939.

The 226-item package makes the arithmetic reproducible but does not include all raw responses and prompt bytes needed for independent mathematical re-adjudication.

Development-time checkpoint-selection endpoint

Checkpoint 20 scored 7/83 on an automatic private ErdosBench endpoint, reproduced exactly under an independent fresh model load. The DPO dose curve was step 10 = 5/83, step 20 = 7/83, step 30 = 3/83, and step 49 = 3/83. This endpoint was repeatedly inspected during selection: 7/83 is exploratory model-selection evidence, not an unbiased generalization estimate.

Machine-readable summaries and claim boundaries are in evaluation_results.json.

Limitations

• Outputs are not formal proofs and can contain subtle or decisive mathematical errors.
• The selected checkpoint made one rejected and five C-grade self-declared strong claims in the 226-item audit.
• Aggregate DPO-versus-V-SAO ErdosBench superiority is not statistically established.
• SIMOBench uses one generation seed per item and model-assisted single-judge grading.
• The evaluated 65,536-token generation budget is larger than many practical serving budgets.
• The earlier 139-item and later 226-item ErdosBench artifacts have no supplied item mapping.
• The private 83-item endpoint was consumed during checkpoint selection.
• Raw model output may expose <think> reasoning spans or fail the intended terminal answer schema.
• The model was not validated for autonomous tools or agentic API use.
• Compact parameter count limits broad factual knowledge compared with larger general-purpose models.

Reproducibility and integrity

• release_manifest.json inventories the model, tokenizer, and exact source hashes.
• provenance.json describes the public lineage without private storage paths.
• evaluation_results.json contains publishable aggregate results and limitations.
• checksums.sha256 binds every released file except itself.

Use the immutable v1.0.0 tag for reproducible downloads.

License

Ulam-1-Small, including its released model weights, is released by Ulam AI under the MIT License. Upstream lineage, attribution, pinned revisions, and material modifications are recorded in NOTICE and provenance.json; archived upstream license text is retained under UPSTREAM_LICENSES/.

Citation

@misc{ulam2026ulamsmall,
  title        = {Ulam-1-Small: Post-Training for Mathematical Reasoning},
  author       = {{Ulam AI}},
  year         = {2026},
  howpublished = {Hugging Face model release},
  url          = {https://huggingface.co/ulamai/Ulam-1-Small}
}

The complete paper is included under paper/.

Contact

For model questions, licensing, or responsible disclosure, contact Ulam AI through ulam.ai.