| --- |
| license: mit |
| base_model: deepseek-ai/DeepSeek-R1-Distill-Qwen-1.5B |
| tags: |
| - math |
| - reasoning |
| - verifiable |
| - rlvr |
| - gguf |
| pipeline_tag: text-generation |
| --- |
| |
| # NPC Reason 1.5B |
|
|
| A math-reasoning model whose every load-bearing arithmetic step emits a mechanically-checkable |
| assertion in the form `<<EXPR = RESULT>>`. Specialized from DeepSeek-R1-Distill-Qwen-1.5B (MIT). |
| The point is not just a final answer. It is that a pure-code checker can re-execute every step and |
| confirm the chain, so "verifiable-rate" is not the model's opinion. Anyone can run the checker. |
|
|
| ## Results (frozen held-out eval, n=500, GSM8K + MATH-500, greedy, format prompt) |
|
|
| | metric | base R1-Distill | SFT (V4 distill) | NPC Reason (RL) | |
| |------------------------|----------------:|-----------------:|----------------:| |
| | verifiable-rate | 0.0% | 76.8% | 76.2% | |
| | accuracy | 61.6% | 65.8% | 66.6% | |
| | verified-and-correct | 0.0% | 58.0% | 59.6% | |
|
|
| verified-and-correct (both axes) is the headline. The full arc is shown on purpose, not just the |
| best column. |
|
|
| ## What actually happened (plain language, no overclaiming) |
|
|
| - **The base model produces zero mechanically-verifiable chains, even when asked for the format.** |
| Only 1 of 500 base outputs even contained a `<<` marker. |
| - **The SFT distillation did the heavy lifting: 0 to 76.8% verifiable.** Training on a corpus of |
| DeepSeek-V4 chains that the frozen verifier confirmed (verifiable AND correct, 7,546 kept of |
| 13,245 generated) transferred the grounding. Accuracy rose (61.6 to 65.8), it was not bought by |
| sacrificing correctness. |
| - **RLVR/GRPO against the frozen verifier was a stable refinement, not a decisive gain.** It moved |
| verified-and-correct +1.6pp (58.0 to 59.6) and accuracy +0.8pp, with verifiable flat (-0.6pp). |
| On n=500 that is roughly 8 problems. The RL model and the SFT model are statistically about even. |
| - **The shipped model is the RL checkpoint** (marginally best on the headline). **The SFT model is |
| statistically equivalent and available** as a fallback. Either is a defensible "NPC Reason". |
| - **The pre-registered 90% verifiable bar was NOT met (stuck near 77%).** It was deliberately not |
| chased into instability. This is the open limitation and the next frontier. |
| - Accuracy includes the greedy no-answer floor. The same greedy decoding is used for base and tuned |
| models, so the comparisons are apples-to-apples. |
|
|
| ## The verifier (the methodological core) |
|
|
| A pure-code Python/SymPy checker, frozen at sha256 `d5d146cf...`, used as BOTH the evaluation |
| metric AND the RL reward (byte-identical both times). A chain is VERIFIABLE iff every load-bearing |
| `<<EXPR=RESULT>>` assertion re-executes correctly AND the final answer composes from the last step. |
| Correctness (final == gold) is a separate, independent axis. The verifier is shipped with the model |
| (`verifier/step_verifier.py`); users run it on the model's own outputs. |
|
|
| ## Methods finding worth keeping |
|
|
| GRPO with this hard, frozen, pure-code verifier reward trained STABLY: KL stayed flat (~0.0002), |
| no length runaway, no mode collapse, no early-stop trip. This is notable because prior RL attempts |
| in related work were unstable. RLVR with a clean verifier reward is a regime where a small model |
| trains without collapsing. The lift was small here, but the stability is the keepable result. |
|
|
| ## Intended use and limits |
|
|
| - Use: math problems where checkable, grounded reasoning steps matter (arithmetic and |
| arithmetic-reducible word problems). Prompt for the `<<EXPR = RESULT>>` format (see USAGE.md). |
| - Math-first. Logic, proofs, and general chain-of-thought are NOT claimed and are future work. |
| - Not a general chat model. The 1.5B reasoning ceiling applies. ~23% of format-prompt chains are |
| still not fully verifiable, the unverified tail. |
| - Simulation/research artifact. Verify outputs with the included checker before relying on them. |
|
|
| ## Lineage and license |
|
|
| - Base: DeepSeek-R1-Distill-Qwen-1.5B (MIT). |
| - Training chains distilled from DeepSeek V4 (distillation permitted; output rights assigned to the |
| user). Released under MIT to match the base. |
| - Attribution: Rama Krishna Bachu, Bottensor (Independent Research). ORCID 0009-0000-1298-0681. |
|
|
| ## Reproducibility |
|
|
| The pre-registration was frozen BEFORE any training and an honest-null clause was in force. |
| Frozen references: |
| - Verifier: `VERIFIER.lock` sha256 `d5d146cf...` |
| - Eval set: `EVAL.lock` sha256 `e1573cab...` |
| - Pre-registration: `PREREG.lock` sha256 `b5a49437...` |
|
|
| GGUF quantizations are provided with a per-quant decision-fidelity check vs the bf16 model |
| (see `gguf_fidelity.md`); pick the recommended quant, do not choose on file size alone. |
|
|
