---
language:
  - en
library_name: transformers
pipeline_tag: text-generation
base_model: HuggingFaceTB/SmolLM3-3B
license: other
license_name: webai-non-commercial-license-ver.-1.0
license_link: https://huggingface.co/webAI-Official/webAI-ColVec1-4b/blob/main/LICENSE.md
tags:
  - formal-logic
  - reasoning
  - lora
  - model-merging
  - wise-ft
  - reinforcement-learning
  - grpo
  - smollm3
  - twil-lm
---

# TwIL-LM3

A 3B reasoning model for **formal logic** tasks, built from
[`HuggingFaceTB/SmolLM3-3B`](https://huggingface.co/HuggingFaceTB/SmolLM3-3B) through LoRA
supervised fine-tuning, checkpoint fusion, WiSE-FT weight interpolation, and entropy-weighted
GRPO reinforcement learning.

It improves in-domain formal-logic performance by **+26% relative** over its base model
(macro gate 0.336 → 0.422) **and improves held-out benchmark performance at the same time**
(+0.022 core average). It is the only arm in this project that gains on both tracks, which is
why it is the recommended release of the pair.

## Results

### Track A — in-domain formal logic

The **macro gate** is the mean of five objective scores: entailment labelling, multiple-choice
answering, procedural reasoning, Lean proof critique, and rule induction (scored by its
continuous derivation score). MCQ and procedural are credited as `max(exact_match, loose_match)`.
`n = 200` prompts per objective, greedy decoding, 2048 max new tokens.

| objective | SmolLM3-3B | TwIL-LM3 | Δ |
|---|---:|---:|---:|
| rule_induction | 0.103 | **0.319** | +0.216 |
| entailment_label | 0.335 | **0.575** | +0.240 |
| lean_critic | 0.630 | **0.660** | +0.030 |
| procedural | 0.105 | 0.110 | +0.005 |
| mcq_answer | 0.505 | 0.445 | −0.060 |
| **macro gate** | **0.3356** | **0.4218** | **+0.0862** |

Four of five objectives improve. MCQ answering regressed by six points, and that loss is
averaged into the macro above rather than excluded.

### Track B — held-out benchmarks

Nothing in this suite was trained on. Scores are re-derived from saved generations with
delimiter-aware answer extractors rather than read from harness metrics.

| | SmolLM3-3B | TwIL-LM3 | Δ |
|---|---:|---:|---:|
| core average | 0.790 | **0.812** | **+0.022** |
| suite average (14 datasets) | 0.661 | **0.669** | **+0.008** |

This model **passes the per-capability floor**: no core or held-out transfer metric drops by
more than the 0.02 tolerance against its base.

Per-dataset, largest moves in each direction:

| dataset | base | TwIL-LM3 | Δ |
|---|---:|---:|---:|
| LogicBench BQA | 0.647 | 0.717 | +0.070 |
| DROP | 0.700 | 0.747 | +0.047 |
| CommonsenseQA | 0.707 | 0.737 | +0.030 |
| StrategyQA | 0.633 | 0.650 | +0.017 |
| MMLU-Redux | 0.663 | 0.667 | +0.003 |
| GSM8K | 0.883 | 0.873 | −0.010 |
| MATH-500 | 0.700 | 0.690 | −0.010 |
| IFEval (strict) | 0.677 | 0.643 | −0.033 |

Every regression is within 0.033, and the gains on logical-reasoning transfer tasks
(LogicBench +0.070, DROP +0.047) are larger than any loss. IFEval is the one place worth
noting — instruction-following degrades slightly, which is a common cost of verifier-driven RL.

### Comparison against other open models

All arms below were run through the same harness, prompts and decoding settings described under
[Evaluation protocol](#evaluation-protocol). Throughput rows are reported because in-domain score
alone is misleading for a 3B model: `ans/s` is defined throughout as `tok/s ÷ mean generation
length`, so it measures completed answers rather than raw decode rate.

#### Track A — in-domain formal logic

| lane / metric | TwIL-LM3 | SmolLM3-3B base | Llama-3.2-3B | LFM2-2.6B | LFM2.5-8B-A1B | Qwen3-8B |
|---|---:|---:|---:|---:|---:|---:|
| lean_formalize token_f1 | **0.5869** | 0.4347 | 0.3690 | 0.1321 | 0.4655 | 0.4022 |
| rule_induction derivation | 0.3192 | 0.1029 | 0.0825 | 0.0615 | 0.1936 | **0.3680** |
| entailment_label accuracy | 0.5750 | 0.3750 | 0.3300 | 0.4700 | 0.5400 | **0.5800** |
| mcq_answer accuracy | **0.1100** | 0.0000 | 0.0000 | 0.0150 | 0.0750 | 0.0000 |
| semantic_parse token_f1 | **0.4416** | 0.4149 | 0.3102 | 0.3665 | 0.3778 | 0.4257 |
| lean_critic accuracy | 0.6600 | 0.6500 | 0.5300 | 0.5900 | 0.5500 | **0.7950** |
| lean_formalize exact_match | 0.0050 | 0.0050 | 0.0000 | 0.0000 | 0.0000 | 0.0050 |
| fol_translation exact_match | 0.0000 | 0.0050 | 0.0000 | 0.0000 | 0.0000 | 0.0000 |
| semantic_parse exact_match | 0.0000 | 0.0050 | 0.0000 | 0.0000 | 0.0000 | 0.0000 |
| procedural accuracy | 0.0300 | 0.0050 | 0.0000 | 0.0300 | 0.0350 | **0.0850** |
| procedural loose_match | 0.1100 | 0.1050 | 0.1050 | 0.1150 | 0.1400 | **0.1800** |
| mcq_answer loose_match | 0.4450 | 0.5000 | 0.4150 | 0.5000 | 0.4550 | **0.7450** |
| lm_corpus perplexity ↓ | 2.8972 | 3.1818 | 2.8478 | 4.3815 | 4.9472 | **2.5440** |
| math_corpus perplexity ↓ | **3.8229** | 4.0685 | 4.7531 | 6.7472 | 8.3323 | 4.0083 |
| **macro gate** | 0.4218 | 0.3466 † | 0.2925 | 0.3473 | 0.3757 | **0.5336** |
| **strict-7** | 0.1971 | 0.1493 | 0.1229 | 0.1579 | 0.1714 | **0.2093** |
| tok/s | 15880 | 15564 | 16160 | 25000 | 22000 | not measured |
| mean gen length | **564** | 999 | 696 | 2296 | 1830 | 2094 |
| **ans/s** | **28.1** | 15.6 | 23.2 | 10.9 | 12.0 | not measured |

† The base column here comes from the external-comparison run rather than the paired run used
for the Δ table above, hence 0.3466 against 0.3356 — run-to-run variation of the same
checkpoint. The paired run is the correct basis for the improvement claim.

`strict-7` is the mean of seven lanes scored under strict metrics only (`fol_translation`,
`entailment_label`, `mcq_answer`, `semantic_parse` and `lean_formalize` exact match,
`lean_critic` and `procedural` accuracy), with no loose-match credit anywhere.

Qwen3-8B takes the macro gate at roughly 2.7x the parameter count, driven by the classification
lanes — `lean_critic` 0.7950 and loose MCQ 0.7450. TwIL-LM3 holds the two lanes this pipeline
targets most directly, `lean_formalize` token-F1 (0.5869 against 0.4022) and strict MCQ accuracy
(0.1100, the only non-trivial value in that row), and it is the most efficient arm in the table
by a wide margin: 28.1 answers/sec, from generations averaging 564 tokens where every other arm
except Llama runs past 690.

#### Track B — held-out benchmarks

| dataset | TwIL-LM3 | SmolLM3-3B base | Llama-3.2-3B | LFM2-2.6B | LFM2.5-8B-A1B | Qwen3-8B | gpt-oss-120b ‡ |
|---|---:|---:|---:|---:|---:|---:|---:|
| gsm8k | 0.8733 | 0.8833 | 0.8300 | 0.8767 | 0.9133 | 0.9567 | **0.9767** |
| svamp | 0.8500 | 0.8567 | 0.8200 | 0.9000 | 0.9133 | **0.9400** | **0.9400** |
| gsm_symbolic | 0.7567 | 0.7633 | 0.8067 | **0.9767** | 0.9267 | 0.8133 | 0.8467 |
| arc_cot | 0.8467 | 0.8400 | 0.7967 | 0.8667 | 0.9033 | 0.9633 | **0.9667** |
| logicbench | 0.7167 | 0.6467 | 0.5733 | 0.6267 | 0.7200 | **0.8567** | 0.8533 |
| strategyqa | 0.6500 | 0.6333 | 0.6533 | 0.6433 | 0.6667 | 0.7400 | **0.7867** |
| drop | 0.7467 | 0.7000 | 0.6733 | 0.6900 | 0.6633 | **0.8833** | 0.8500 |
| csqa | 0.7367 | 0.7067 | 0.7500 | 0.7433 | 0.7700 | **0.8633** | 0.8367 |
| musr | 0.4957 | 0.4997 | 0.4932 | 0.4867 | 0.5703 | 0.6301 | **0.6852** |
| mmlu_redux | 0.6667 | 0.6633 | 0.6000 | 0.7133 | 0.8367 | 0.8500 | **0.9467** |
| ifeval | 0.6433 | 0.6767 | 0.7167 | 0.7300 | **0.8900** | 0.8400 | 0.7900 |
| rudas_ood | 0.0365 | 0.0209 | **0.0733** | 0.0017 | 0.0061 | 0.0468 | 0.0000 § |
| bbh_logic | 0.6633 | 0.6667 | 0.5333 | 0.5713 | 0.7700 | 0.6367 | **0.9980** |
| math500 | 0.6900 | 0.7000 | 0.4233 | 0.7133 | 0.7800 | 0.6100 | **0.8433** |
| **macro (10 CoT datasets)** | 0.7339 | 0.7193 | 0.6997 | 0.7523 | 0.7884 | 0.8493 | **0.8689** |
| **macro (all 14)** | 0.6694 | 0.6612 | 0.6245 | 0.6814 | 0.7378 | 0.7591 | **0.8086** |
| tok/s | 15880 | 15564 | 16160 | 25000 | 22000 | not measured | 3374 |
| mean gen length | **482** | 626 | 510 | ≈796 | ≈1327 | ≈1931 | 801 |
| **ans/s** | **32.9** | 24.9 | 31.7 | ≈31.4 | ≈16.6 | not measured | 4.2 |

‡ MXFP4 weights, tensor-parallel 2 — quantized and multi-GPU, so not directly comparable to the
single-GPU BF16 rows. § 74% of its `rudas_ood` generations hit the length cap, so that cell is a
truncation artefact rather than a measured score; excluding the row, its 13-dataset macro is
0.8708.

Lengths marked ≈ are derived from stored generations using each model's characters-per-token
ratio rather than re-tokenized directly; the method reproduces the three directly measured
lengths to within 3.5%.

The honest summary of this table is that TwIL-LM3 does not lead it. Larger models score higher,
in order of size, and the 120B leads nine of fourteen rows. Two things are worth extracting
anyway. First, TwIL-LM3 improves on its own base while sitting mid-table (0.7339 against 0.7193
on the 10-dataset macro), which is the point of the WiSE-FT stage — in-domain gains without
transfer collapse. Second, it produces the shortest generations of any arm here at 482 tokens
and consequently the most answers per second at 32.9, roughly eight times the 120B's rate.

## Usage

```python
import torch
from transformers import AutoModelForCausalLM, AutoTokenizer

model_id = "webAI-Official/TwIL-LM3"
tok = AutoTokenizer.from_pretrained(model_id)
model = AutoModelForCausalLM.from_pretrained(
    model_id, torch_dtype=torch.bfloat16, device_map="auto"
)

messages = [{"role": "user", "content":
             "Does 'All dogs are mammals. Rex is a dog.' entail 'Rex is a mammal'? "
             "Answer entailment, contradiction, or neutral."}]
inputs = tok.apply_chat_template(
    messages, add_generation_prompt=True,
    return_tensors="pt", return_dict=True,
).to(model.device)

out = model.generate(**inputs, max_new_tokens=2048, do_sample=False)
print(tok.decode(out[0][inputs["input_ids"].shape[-1]:], skip_special_tokens=True))
```

`return_dict=True` matters on transformers 5.x, where `apply_chat_template` returns a
`BatchEncoding` rather than a bare tensor; the above works on both 4.x and 5.x.

The reported numbers use **greedy decoding** (`do_sample=False`) and a **2048-token** generation
budget. Note that the shipped `generation_config.json` inherits SmolLM3's sampling defaults
(`do_sample=true`, `temperature=0.6`, `top_p=0.95`), so `do_sample=False` must be passed
explicitly to reproduce the evaluation. The model opens a `<think>...</think>` reasoning block
before answering, so a short generation budget truncates reasoning and scores far worse.

### GGUF / llama.cpp

Quantized GGUF builds ship in this repository alongside the safetensors weights. The `smollm3`
architecture is supported by llama.cpp, and the chat template, `<|im_end|>` EOS and BOS are
carried into the GGUF metadata, so chat mode works without extra flags.

| file | quant | size | bits/weight | notes |
|---|---|---:|---:|---|
| `TwIL-LM3-Q4_K_M.gguf` | Q4_K_M | 1.78 GiB | 4.96 | recommended default; runs on CPU or 4 GB of VRAM |
| `TwIL-LM3-Q8_0.gguf` | Q8_0 | 3.05 GiB | 8.50 | near-lossless, for quality-sensitive use |

```bash
llama-cli -m TwIL-LM3-Q4_K_M.gguf -cnv --temp 0 -n 2048
```

Two things matter for reproducing the scores above under llama.cpp. Pass `--temp 0`, because the
evaluation is greedy while the packaged sampling defaults are not. And leave the generation
budget large — 2048 tokens or more — since the model emits a `<think>` block before answering
and a short budget truncates it, which costs far more accuracy than the quantization does.

Q8_0 was produced directly by `convert_hf_to_gguf.py` from the released bf16 weights; Q4_K_M was
produced from an F16 conversion with `llama-quantize`, without an importance matrix. Both builds
were smoke-tested for load and generation on CPU. The published Track A and Track B numbers were
measured on the **bf16** weights through vLLM, not on these GGUF builds, so expect small
deviations at Q4_K_M that have not been quantified here.

## How it was built

Four stages on top of the base model:

1. **LoRA supervised fine-tuning** on a synthetic formal-logic corpus covering the Track A
   objectives (first-order-logic translation, entailment labelling, semantic parsing, Lean
   formalisation and critique, procedural reasoning, rule induction).
2. **Checkpoint fusion** — parameter-space averaging of intermediate SFT checkpoints selected
   by a diversity probe, rather than taking the final checkpoint.
3. **WiSE-FT interpolation** toward the pretrained base, `W = (1 − λ)·W_base + λ·W_finetuned`
   with **λ = 0.25** — i.e. only a quarter of the fine-tuned delta is retained. λ was chosen by
   constrained optimisation: maximise in-domain score subject to minimal degradation on held-out
   benchmarks. This conservative λ is the direct reason held-out capability survives.
4. **MGPO** — entropy-weighted GRPO reinforcement learning against a programmatic verifier, with
   partial credit for loose matches and token-F1 so that all-fail prompt groups still produce
   gradient. Published checkpoint is **step 2071**.

A sibling arm that skipped stage 3's conservative interpolation scores considerably higher
in-domain (macro gate 0.515) but gives back roughly twelve points of held-out capability. This
release is the balanced point of that trade; the other was not published.

## Limitations and caveats

**Truncation.** At a 2048-token budget, 4.4% of Track A generations hit the cap — better than
the base's 17.4%, but still above the 2% threshold our protocol requires to mark a comparison
`rankable`. The Track A macro gate should therefore be read as indicative rather than exact.
Because a truncated response scores zero regardless of reasoning quality, both numbers are
pessimistic, and the base substantially more so — meaning the true Track A gap is probably
narrower than +0.086.

**Scope.** Tuned for formal logic. The Track B suite does not cover code generation or tool use
(HumanEval, LiveCodeBench and BFCL were not run for this model or its base), so this release
makes no claim about those.

**Not a chat model.** It was optimised against automatic verifiers on logic tasks. It has had no
safety tuning beyond whatever the base model carries, and no instruction-following alignment
work — IFEval regressed slightly.

**Failed consolidation stage.** A post-RL self-distillation round (SDFT) was attempted and made
both tracks worse at every budget tried (−18% Track A at one epoch on this family). It is not
part of this model. See the accompanying `SDFT_RESULT.md` in the project repository.

## Evaluation protocol

- Track A: `n = 200` per objective, greedy (`temperature = 0`), `max_new_tokens = 2048`, one
  retry at 4096 for truncated rows, `max_seq_len = 8192`, seed 42.
- Track B: 300 examples per task, greedy, `max_gen_toks = 4096`, `max_model_len = 8192`,
  `repetition_penalty = 1.0`, chat template applied, vLLM backend.
- Both tracks use the same protocol for the model and its base, in a paired run over identical
  sampled rows.

`repetition_penalty = 1.0` is load-bearing. A 1.1 penalty produced apparent 20-point swings on
Track B that were pure decoding artefact; the decoding kwargs are hashed into the protocol
identity so a mismatched runner fails loudly instead of quietly producing a different number.

## Relationship to TwIL-LM

[`webAI-Official/TwIL-LM`](https://huggingface.co/webAI-Official/TwIL-LM) is the 1.7B member of
this family, built from SmolLM2 by the same pipeline. It reaches a higher in-domain score
relative to its own base but gives back held-out capability; this model is the one that improves
both. Unlike TwIL-LM's `main` branch, which ships a PEFT LoRA adapter, this repository ships a
full merged model loaded directly with `AutoModelForCausalLM`.

## License and attribution

Released under the **webAI Non-Commercial License ver. 1.0** — see `LICENSE.md` in this
repository.

The base model, [`HuggingFaceTB/SmolLM3-3B`](https://huggingface.co/HuggingFaceTB/SmolLM3-3B),
is Apache 2.0; its licence text is retained as `apache-2.0-LICENSE.txt` and all credit for the
base model goes to the HuggingFaceTB team. Apache 2.0 permits distributing derivative works
under different terms provided attribution is preserved, which is what the pair of licence files
in this repository does.