README.md

---
language:
  - en
library_name: transformers
pipeline_tag: text-generation
base_model: ibm-granite/granite-4.2-3b
license: other
license_name: webai-non-commercial-license-ver.-1.0
license_link: https://huggingface.co/webAI-Official/TwIL-LM3-Pro/blob/main/LICENSE.md
tags:
  - granite
  - granite-4.2
  - formal-logic
  - reasoning
  - lora
  - model-merging
  - wise-ft
  - reinforcement-learning
  - grpo
  - gguf
---

# TwIL-LM3-Pro

A 3.66B reasoning model for **formal logic** tasks, built from
[`ibm-granite/granite-4.2-3b`](https://huggingface.co/ibm-granite/granite-4.2-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 **+28% relative** over its base model
(macro gate 0.431 → 0.554) **while holding held-out benchmark performance** — the 10-dataset
macro is level with the base (0.7942 → 0.7901) and the 14-dataset macro improves slightly
(0.7332 → 0.7425). On the same harness and sampled rows it reaches the highest Track A macro
gate, strict-7 and six-lane average of any arm in the tables below for which each can be
computed, including Qwen3-8B, Qwen3.5-4B, VibeThinker-3B and gpt-oss-120b (the 120B has no gate or strict-7
value).

![TwIL-LM3-Pro formal and general reasoning benchmarks against VibeThinker-3B, VibeThinker-webAI-trained, Qwen3.5-4B, Qwen3-8B, gpt-oss-120b, LFM2.5-8B-A1B and TwIL-LM3](benchmarks.png)

*VibeThinker-webAI-trained is the public VibeThinker-3B after the same post-training pipeline (SLERP, d = 0.5, t = 0.5); see [Against the tuned VibeThinker-3B](#against-the-tuned-vibethinker-3b). It has no strict-7 or six-lane-average value, so those bars show n/a.*

## Highlights

* **Large in-domain gain on the same harness.** Macro gate 0.4313 → 0.5539 (+0.123) and strict-7
  0.1821 → 0.2879 against its own base, measured on identical sampled rows. Both models are
  heavily truncated at this budget (see [Limitations](#limitations-and-caveats)), and the base
  more so, so the size of the gap is indicative rather than exact.
* **Top of the Track A summary rows at 3.66B.** Macro gate 0.5539 against Qwen3-8B's 0.5336
  (2.2x the parameters) and TwIL-LM3's 0.4218; strict-7 0.2879 against 0.2093 and 0.1971;
  six-lane average 0.5389 against gpt-oss-120b's 0.5192. The gate lead over Qwen3-8B is 0.020 —
  smaller than the sampling noise at n = 200 per lane — so read that one as parity, not a win.
* **Strongest strict MCQ, and close to the best language-model fit.** `mcq_answer` strict accuracy
  0.4100 (next best 0.1700), `lean_critic` 0.7950 (tied with Qwen3-8B and its own base), the
  lowest `lm_corpus` perplexity of any arm (2.3130) and a `math_corpus` perplexity of 3.6983 that
  only Qwen3.5-4B beats (3.5926). Perplexity is per token, so it is only loosely comparable across
  tokenizers.
* **Holds general capability.** Track B 10-dataset macro 0.7901 and 14-dataset macro 0.7425 —
  ahead of LFM2.5-8B-A1B (0.7884 / 0.7378) at less than half its parameter count, and behind
  Qwen3-8B (0.8493 / 0.7591) and gpt-oss-120b (0.8689 / 0.8086). It gains on BBH-logic
  (0.9013 → 0.9540), MATH-500 (0.6567 → 0.7467) and MuSR (0.5922 → 0.6409), and gives back
  GSM-Symbolic (0.8900 → 0.8267) and ARC (0.8933 → 0.8600).
* **Against VibeThinker-3B, a reasoning model of similar size.** TwIL-LM3-Pro leads it on all
  six Track A lanes — macro gate 0.5539 against 0.4118, strict-7 0.2879 against 0.2021 — but not
  on Track B, where VibeThinker-3B is ahead on the 10-dataset macro (0.8097 against 0.7901) and
  TwIL-LM3-Pro is ahead on the 14-dataset macro (0.7425 against 0.7262). That 14-dataset lead
  comes entirely from BBH-logic (0.9540 against 0.6107); without that row TwIL-LM3-Pro trails.
* **The pipeline is not tied to one model.** The same recipe was run on five base models. On
  VibeThinker-3B it lifts the Track A macro gate from 0.374 to 0.508 (SLERP, the
  *VibeThinker-webAI-trained* column) while the Track B 10-dataset macro moves from 0.815 to 0.802 — see
  [One pipeline, several models](#one-pipeline-several-models).
* **Structured formal output.** Tuned for the objects rather than the prose: FOL translation,
  entailment labels, semantic parses, Lean statements and Lean proof critique.
* **Runs anywhere.** 3.66B parameters in bf16 (6.82 GiB), with a Q4\_K\_M GGUF at 2.09 GiB for
  CPU or 4 GB of VRAM.

It is **not the most efficient**: it reasons at length. Track A generations average 1,902 tokens,
against 564 for TwIL-LM3, and 24.2% of them hit the length cap. Its raw decode rate is high
(21,169 tok/s †) but the long answers bring it to about 11 completed
answers per second †, against 28.1 for TwIL-LM3 and 4.5 for Qwen3-8B. It is also not a general
assistant — there is no safety or preference tuning here beyond what Granite 4.2 carries. See
[Limitations](#limitations-and-caveats).

## Model Details

| Property                  | Value                                                                                          |
| ------------------------- | ---------------------------------------------------------------------------------------------- |
| Model ID                  | `webAI-Official/TwIL-LM3-Pro`                                                              |
| Base model                | [`ibm-granite/granite-4.2-3b`](https://huggingface.co/ibm-granite/granite-4.2-3b)              |
| Total parameters          | 3.66B (3,659,737,600)                                                                          |
| Architecture              | Granite decoder-only dense transformer (`GraniteForCausalLM`); 40 layers, hidden size 2560, 40 attention heads / 8 KV heads |
| Input / output            | Text / text                                                                                    |
| Language                  | English                                                                                        |
| Tokenizer vocabulary size | 100,352                                                                                        |
| Context window            | 131,072 tokens                                                                                 |
| Checkpoint precision      | bfloat16 (6.82 GiB), plus Q4\_K\_M / Q5\_K\_M / Q6\_K / Q8\_0 / F16 GGUF builds              |
| Post-training             | LoRA SFT → checkpoint fusion → WiSE-FT (α = 0.15) → MGPO reinforcement learning (β = 0.02, step 2580) |
| Reasoning format          | Emits a `<think>…</think>` block before the answer (default chat template)                     |
| Evaluated decoding        | Greedy, 2048 new tokens (one retry at 4096), `max_seq_len` 8192                                |
| Specialisation            | Formal logic: FOL translation, entailment, semantic parsing, Lean formalisation and critique   |
| License                   | webAI Non-Commercial License ver. 1.0                                                          |

The base model's 131,072-token context is carried through unchanged, but every score on this card
was measured inside an 8,192-token window; longer contexts are inherited rather than validated
here.

## Results

### Track A — in-domain formal logic

TwIL-LM3-Pro, its base and VibeThinker-3B were run through the same harness, prompts, decoding
settings and sampled rows described under [Evaluation protocol](#evaluation-protocol), and the
other peer columns are the values already published for TwIL-LM3 on its card, produced by that
same harness (see [Comparability](#limitations-and-caveats)). Throughput rows come from a
dedicated decode-throughput protocol: `ans/s` is defined throughout as
`tok/s ÷ mean generation length`, so it measures completed answers rather than raw decode rate.
Cells marked † need the engine note below.

| lane / metric | TwIL-LM3-Pro | Granite-4.2-3B base | VibeThinker-3B | VibeThinker-webAI-trained ★ | Qwen3.5-4B | TwIL-LM3 | Llama-3.2-3B | LFM2-2.6B | LFM2.5-8B-A1B | Qwen3-8B | gpt-oss-120b ‡ |
|---|---:|---:|---:|---:|---:|---:|---:|---:|---:|---:|---:|
| lean_formalize token_f1 | 0.5092 | 0.2943 | 0.2087 | 0.527 | 0.4996 | 0.5869 | 0.3690 | 0.1321 | 0.4655 | 0.4022 | **0.6306** |
| rule_induction derivation | 0.4195 | 0.2267 | 0.2038 | 0.227 | 0.5078 | 0.3192 | 0.0825 | 0.0615 | 0.1936 | 0.3680 | **0.6518** |
| entailment_label accuracy | 0.6700 | 0.3000 | 0.5500 | 0.685 | 0.2400 | 0.5750 | 0.3300 | 0.4700 | 0.5400 | 0.5800 | **0.7750** |
| mcq_answer accuracy | **0.4100** | 0.1200 | 0.1700 | — | 0.0000 | 0.1100 | 0.0000 | 0.0150 | 0.0750 | 0.0000 | 0.0700 |
| semantic_parse token_f1 | 0.4295 | 0.3910 | 0.2422 | 0.392 | 0.3826 | **0.4416** | 0.3102 | 0.3665 | 0.3778 | 0.4257 | 0.4331 |
| lean_critic accuracy | **0.7950** | **0.7950** | 0.6000 | 0.685 | 0.5400 | 0.6600 | 0.5300 | 0.5900 | 0.5500 | **0.7950** | 0.5550 |
| lm_corpus perplexity ↓ | **2.3130** | 2.6334 | 16.9253 | 7.350 | 2.3916 | 2.8972 | 2.8478 | 4.3815 | 4.9472 | 2.5440 | 912.23 § |
| math_corpus perplexity ↓ | 3.6983 | 4.4864 | 27.0318 | 7.000 | **3.5926** | 3.8229 | 4.7531 | 6.7472 | 8.3323 | 4.0083 | 1045.63 § |
| average, 6 lanes | **0.5389** | 0.3545 | 0.3291 | — | 0.3617 | 0.4488 | 0.2703 | 0.2725 | 0.3670 | 0.4285 | 0.5192 |
| **macro gate** | **0.5539** | 0.4313 | 0.4118 | 0.508 | 0.4466 | 0.4218 | 0.2925 | 0.3473 | 0.3757 | 0.5336 | — |
| **strict-7** | **0.2879** | 0.1821 | 0.2021 | — | 0.1121 | 0.1971 | 0.1229 | 0.1579 | 0.1714 | 0.2093 | — |
| macro_primary | **0.5875** | 0.4825 | 0.4637 | 0.579 | 0.4313 | 0.4475 | 0.3450 | 0.4188 | 0.4213 | 0.5750 | — |
| tok/s | 21169 † | 21916 † | 28010 † | ≈28010 ★ † | 11097 † | 15880 | 16160 | 25230 | 22480 | 9420 | 3374 |
| mean gen length | 1902 | 2951 | 2688 | — | 2486 | **564** | 696 | 2296 | 1830 | 2094 | 1005 |
| **ans/s** | 11.1 † | 7.4 † | 10.4 † | — | 4.5 † | **28.1** | 23.2 | 10.9 | 12.0 | 4.5 | 3.4 |

‡ **gpt-oss-120b** runs MXFP4 weights at tensor-parallel 2 — quantized and multi-GPU, so its
throughput rows are not directly comparable to the single-GPU BF16 arms. Its `procedural` lane
and the loose-match scorings were not collected, so the three summary rows below the six-lane
average cannot be computed for it; that is what the — cells mean, not a zero.

§ The 120B's perplexities are three orders of magnitude off every other arm because its response
format and tokenizer make the corpus lanes score a different quantity. The number is reported
for completeness but is not a comparable measurement, and is excluded from the bolding.

★ **VibeThinker-webAI-trained** is the public VibeThinker-3B after the same post-training pipeline as
TwIL-LM3-Pro, in its SLERP (d = 0.5, t = 0.5) configuration; it is not a checkpoint in this
repository, and [the section below](#against-the-tuned-vibethinker-3b) explains how it differs
from the base model. Its figures are taken from the internal family comparison tables, to three
decimals, not from the per-lane reports behind the other columns, so its column is indicative
rather than strictly paired with them. `macro gate` and `macro_primary` are the family tables'
"macro primary (rule)" and "primary" columns, which have the same definitions as above. The
family tables score `mcq_answer` with loose-match credit (0.695), so the strict MCQ row, the
six-lane average and strict-7 — which all need strict scoring — are left as —. Its perplexities
come from that separate run; the family table records the untuned VibeThinker-3B at 18.70 and
21.80 there, against 16.93 and 27.03 in the columns above, so read them within their own source.
Its `tok/s` is an **estimate, not a measurement**: merging changes weights but not architecture,
parameter count or tokenizer, and the throughput protocol fixes the output at 512 generated tokens
with EOS ignored, so the decode rate does not depend on what the weights say. It is therefore set
equal to the 28,010 tok/s measured for the base VibeThinker-3B in the same session (a ≈ and both
marks in the cell). Mean generation length, and so `ans/s`, does depend on the weights and was not
measured, so those rows stay —.

† **Throughput for TwIL-LM3-Pro, its base and VibeThinker-3B** was measured with the same
dedicated protocol and prompt file as the peer columns (128 prompts × 512 generated tokens, EOS
ignored, greedy, `gpu_memory_utilization` 0.45, idle GPU), run on a single H200 with vLLM
0.19.1 in a later session, whereas the other columns are figures recorded earlier on vLLM 0.11.2. Engine effects
are architecture-dependent: in the same session TwIL-LM3 re-measured at 15,248 tok/s
against its published 15,880 (−4%), while VibeThinker-3B measured
28,010 against a published 18,116 (+55%). The †
cells are therefore comparable with each other, and only approximately with the older columns.
The Qwen3.5-4B figure comes from the earlier throughput sweep, which ran the Qwen3.5 models on the
newer engine (vLLM 0.19.1) according to its driver script, so it belongs with the † cells.
TwIL-LM3-Pro's two runs gave 20,454 and 21,884 tok/s (the first paid for cold
kernel caches) and the table shows their mean. `mean gen length` is measured directly under the
shared evaluation protocol and is comparable across every column.

**`average, 6 lanes`** is the plain mean of the six objective rows above it, each at whatever
scoring that row reports (Lean F1, rule derivation, entailment, MCQ strict, semantic F1, critic).
It is a coarser summary than the three that follow — it mixes token-F1 with accuracy — but it is
the only summary row every arm here can be compared on, including the 120B.

The next three rows aggregate more carefully. None of them include the perplexity lanes or the
token-F1 scorings, which are not on a common 0–1 accuracy scale.

**`macro gate`** is the headline metric and the one the training pipeline gates on. It is the
equal-weight mean of five objectives: the four bounded classification lanes (`entailment_label`,
`mcq_answer`, `procedural`, `lean_critic`) plus `rule_induction`, scored by its continuous
derivation score. In the gate, `mcq_answer` and `procedural` are credited as
`max(exact_match, loose_match)`: for free-text answer lanes, a response that is correct but
differently formatted is a formatting artefact rather than a reasoning failure. This affects the
aggregate only — the per-lane rows above stay strict. (TwIL-LM3-Pro's loose-match MCQ is
0.6500 against the 0.4100 strict figure shown in the lane row.)

**`macro_primary`** is the same mean over the four classification lanes alone, without
`rule_induction`.

**`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. It is deliberately
harsh — exact match on generative lanes is near zero for every arm — so it is useful for ranking
models against each other but not as an absolute capability measure.

TwIL-LM3-Pro leads all four summary rows that every arm with a computable value can be
compared on. The clearest margins are over the arms at its own scale and above: 0.5539 against
0.3757 on the gate for LFM2.5-8B-A1B, and 0.2879 against 0.1971 on strict-7 for TwIL-LM3. Against
Qwen3-8B the gate gap is only 0.020, but strict-7 is 0.2879 against 0.2093 — a difference that
does not depend on loose-match credit — and TwIL-LM3-Pro leads on MCQ (strict 0.4100 against
0.0000), rule induction (0.4195 against 0.3680) and both perplexity lanes.

VibeThinker-3B — WeiboAI's 3B reasoning model, with 37.1% of its Track A generations truncated
— trails TwIL-LM3-Pro on every objective lane and every summary row: macro gate 0.4118 against
0.5539, strict-7 0.2021 against 0.2879, six-lane average 0.3291 against 0.5389. The gap is widest
on Lean formalisation (0.2087 against 0.5092) and narrowest on entailment (0.5500 against 0.6700).
Its corpus perplexities (16.93 and 27.03) are not comparable with the Granite-tokenizer models',
because perplexity is per token and its vocabulary is 151,936 against 100,352.

Qwen3.5-4B, a 4B reasoning model, sits between
the small models and TwIL-LM3-Pro: macro gate 0.4466 against 0.5539, strict-7 0.1121 against
0.2879. It is ahead of TwIL-LM3-Pro on two rows only, `rule_induction` (0.5078 against 0.4195,
second in the table after gpt-oss-120b) and `math_corpus` perplexity (3.5926 against 3.6983), and
far behind on entailment (0.2400 against 0.6700) and strict MCQ (0.0000 against 0.4100).

It does not lead every lane. gpt-oss-120b is clearly stronger on `rule_induction` (0.6518),
entailment (0.7750) and Lean formalisation (0.6306), and TwIL-LM3 remains ahead on Lean
formalisation (0.5869 against 0.5092) and semantic parsing (0.4416 against 0.4295). The two weak
spots in absolute terms are `procedural` (strict 0.1200, loose 0.2350) and FOL translation
(exact match 0.0100).

### Track B — held-out benchmarks

| dataset | TwIL-LM3-Pro | Granite-4.2-3B base | VibeThinker-3B | VibeThinker-webAI-trained ★ | Qwen3.5-4B | TwIL-LM3 | Llama-3.2-3B | LFM2-2.6B | LFM2.5-8B-A1B | Qwen3-8B | gpt-oss-120b ‡ |
|---|---:|---:|---:|---:|---:|---:|---:|---:|---:|---:|---:|
| gsm8k | 0.9433 | 0.9533 | 0.9600 | 0.930 | 0.8633 | 0.8733 | 0.8300 | 0.8767 | 0.9133 | 0.9567 | **0.9767** |
| svamp | 0.9500 | 0.9200 | 0.9367 | **0.953** | 0.8867 | 0.8500 | 0.8200 | 0.9000 | 0.9133 | 0.9400 | 0.9400 |
| gsm_symbolic | 0.8267 | 0.8900 | 0.8167 | 0.883 | 0.7767 | 0.7567 | 0.8067 | **0.9767** | 0.9267 | 0.8133 | 0.8467 |
| arc_cot | 0.8600 | 0.8933 | 0.9033 | 0.877 | 0.9267 | 0.8467 | 0.7967 | 0.8667 | 0.9033 | 0.9633 | **0.9667** |
| logicbench | 0.7933 | 0.7733 | **0.8600** | 0.850 | 0.7200 | 0.7167 | 0.5733 | 0.6267 | 0.7200 | 0.8567 | 0.8533 |
| strategyqa | 0.5967 | 0.6267 | 0.6467 | 0.647 | 0.6967 | 0.6500 | 0.6533 | 0.6433 | 0.6667 | 0.7400 | **0.7867** |
| drop | 0.7367 | 0.7467 | 0.8467 | 0.790 | 0.6233 | 0.7467 | 0.6733 | 0.6900 | 0.6633 | **0.8833** | 0.8500 |
| csqa | 0.7667 | 0.7733 | 0.7367 | 0.687 | 0.7767 | 0.7367 | 0.7500 | 0.7433 | 0.7700 | **0.8633** | 0.8367 |
| musr | 0.6409 | 0.5922 | 0.5799 | 0.588 | 0.5696 | 0.4957 | 0.4932 | 0.4867 | 0.5703 | 0.6301 | **0.6852** |
| mmlu_redux | 0.7867 | 0.7733 | 0.8100 | 0.813 | 0.8433 | 0.6667 | 0.6000 | 0.7133 | 0.8367 | 0.8500 | **0.9467** |
| ifeval | 0.7500 | 0.7633 | 0.6633 | 0.557 | 0.2400 ¶¶¶ | 0.6433 | 0.7167 | 0.7300 | **0.8900** | 0.8400 | 0.7900 |
| rudas_ood | 0.0437 ¶¶ | 0.0012 | 0.0056 | 0.000 | 0.0084 ¶¶¶ | 0.0365 | **0.0733** | 0.0017 | 0.0061 | 0.0468 | 0.0000 ¶ |
| bbh_logic | 0.9540 | 0.9013 | 0.6107 | 0.829 | 0.9647 | 0.6633 | 0.5333 | 0.5713 | 0.7700 | 0.6367 | **0.9980** |
| math500 | 0.7467 | 0.6567 | 0.7900 | 0.790 | 0.3600 ¶¶¶ | 0.6900 | 0.4233 | 0.7133 | 0.7800 | 0.6100 | **0.8433** |
| **macro (10 CoT datasets)** | 0.7901 | 0.7942 | 0.8097 | 0.802 | 0.7683 | 0.7339 | 0.6997 | 0.7523 | 0.7884 | 0.8493 | **0.8689** |
| **macro (all 14)** | 0.7425 | 0.7332 | 0.7262 | 0.728 | 0.6611 | 0.6694 | 0.6245 | 0.6814 | 0.7378 | 0.7591 | **0.8086** |
| tok/s | 21169 † | 21916 † | 28010 † | ≈28010 ★ † | 11097 † | 15880 | 16160 | 25230 | 22480 | 9420 | 3374 |
| mean gen length | ≈792 | ≈1282 | ≈1789 | — | ≈2787 | **482** | 510 | ≈796 | ≈1327 | ≈1931 | 801 |
| **ans/s** | 26.7 † | 17.1 † | ≈15.7 † | — | ≈4.0 † | **32.9** | 31.7 | ≈31.7 | ≈16.9 | 4.9 | 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. ¶¶ 93.7% of TwIL-LM3-Pro's `rudas_ood` generations also hit the length cap, so its
cell is likewise a truncation artefact rather than a measurement of the model's ability.
¶¶¶ Qwen3.5-4B hits the length cap on 67.3% of IFEval, 59.0% of MATH-500 and 99.3% of `rudas_ood`
generations, so those three cells are truncation artefacts too.

Lengths marked ≈ are derived from stored generations rather than read from the run. For
TwIL-LM3-Pro, its base and VibeThinker-3B they were re-tokenized directly with each model's
own tokenizer and
averaged over the 14 datasets (MuSR counted once); the same method reproduces TwIL-LM3's measured
482 to within 1%. The peer lengths marked ≈ use each model's characters-per-token ratio and are
carried over from the TwIL-LM3 card. † `tok/s` is the same throughput figure as in Track A (see
the engine note under that table) and `ans/s` divides it by the mean generation length shown. The
VibeThinker-3B Track B rows come from the same external-baseline run and vLLM 0.11.2 engine as
the other external peers.

The honest summary of this table is that TwIL-LM3-Pro does not lead it. Larger models score
higher, and gpt-oss-120b leads seven of the fourteen dataset rows. Three things are worth
extracting anyway. First, it holds its own base on the held-out suite (10-dataset macro 0.7901
against 0.7942, a difference well inside the sampling noise at n = 300 per dataset) while gaining
in-domain, which is the point of the WiSE-FT stage. Second, the 14-dataset macro rises 0.0093
over the base, driven by BBH-logic, MATH-500 and MuSR. Third, it edges LFM2.5-8B-A1B on both
macros at less than half the parameters and leads every untuned arm on SVAMP (0.9500; the
tuned VibeThinker-3B is at 0.953, one example out of 300 higher).

VibeThinker-3B is the stronger held-out model on the 10-dataset macro (0.8097 against 0.7901). It
is ahead of TwIL-LM3-Pro on seven datasets — GSM8K, ARC, LogicBench, StrategyQA, DROP,
MMLU-Redux and MATH-500 — and behind on the other seven: SVAMP, GSM-Symbolic, CSQA, MuSR, IFEval,
BBH-logic and `rudas_ood`. TwIL-LM3-Pro's 0.0163 lead on the 14-dataset macro comes entirely
from BBH-logic (0.9540 against 0.6107): on the other thirteen datasets it averages 0.7263 against
VibeThinker-3B's 0.7350. VibeThinker-3B also writes much longer answers on Track B (about 1,789
tokens against 792).

Track B here was run with the chat template's thinking mode **disabled** for TwIL-LM3-Pro and
its base (the prompt ends in an empty `<think></think>`), as it was for TwIL-LM3, whereas Track A
uses the default thinking mode. The Track B numbers therefore describe non-reasoning behaviour;
they are not a measure of what a thinking-mode generation would score. Some Track B cells are also
truncation-limited: MATH-500 hits the cap on 14.0% of rows, and SVAMP, GSM-Symbolic and
MuSR-team sit slightly above the 2% cap-hit threshold (3.0%, 3.0% and 2.8%).

### Against the tuned VibeThinker-3B

The tables above use the public VibeThinker-3B checkpoint. The same post-training pipeline was also
applied to it, and two of its tuned configurations are the closest same-scale comparisons to
TwIL-LM3-Pro: WiSE-FT (λ = 0.50), and the SLERP merge (d = 0.5, t = 0.5) that appears in the
tables and plot as **VibeThinker-webAI-trained**. These values come from the family comparison tables
rather than from a per-lane raw report, so they are shown as a summary only:

| model | macro gate | macro_primary | B10 | B14 | Track A truncation |
|---|---:|---:|---:|---:|---:|
| TwIL-LM3-Pro | **0.554** | **0.588** | 0.790 | **0.743** | 24.2% |
| VibeThinker-webAI-trained (SLERP, d = 0.5, t = 0.5) | 0.508 | 0.579 | **0.802** | 0.728 | — |
| VibeThinker-3B, WiSE-FT λ = 0.50 | 0.541 | **0.588** | **0.802** | 0.728 ◊ | 14.3% |

◊ There is no B14 row for the λ = 0.50 configuration; the figure is the one recorded for the SLERP
configuration in the row above. Truncation was not recorded for the SLERP configuration.

Against VibeThinker-webAI-trained, TwIL-LM3-Pro is ahead on Track A (macro gate 0.554 against 0.508,
`macro_primary` 0.588 against 0.579) and on the 14-dataset macro (0.743 against 0.728), and behind
on the 10-dataset macro (0.790 against 0.802). Against the WiSE-FT λ = 0.50 configuration the two
are effectively tied on Track A (gate 0.554 against 0.541, `macro_primary` equal at 0.588, both
within sampling noise at n = 200), and the tuned VibeThinker-3B is ahead on the 10-dataset macro
with a lower truncation rate. TwIL-LM3-Pro's edge is the 14-dataset macro, a gap that cannot be
broken down per dataset from the summary values.

#### How VibeThinker-webAI-trained differs from the base VibeThinker-3B

**Base VibeThinker-3B** is WeiboAI's public checkpoint, unmodified, and is what the untuned columns
in the tables above measure. **VibeThinker-webAI-trained** starts from those same weights and changes
them in two ways:

* **Formal-logic post-training.** A rank-64 LoRA is trained on the same synthetic formal-logic
  corpus and Track A objectives used for TwIL-LM3-Pro (FOL translation, entailment, semantic
  parsing, Lean formalisation and critique, procedural reasoning, rule induction), with multipath
  distillation supplying the reasoning traces.
* **Merging back toward the base.** The tuned weights are not used raw. They are merged into the
  pretrained VibeThinker-3B weights with a DARE-SLERP merge (d = 0.5, t = 0.5, the configuration
  labels used in the family tables), the same conservative interpolation step that protects
  held-out capability in TwIL-LM3-Pro.

The family tables record no reinforcement-learning (MGPO) run for VibeThinker-3B, so
VibeThinker-webAI-trained reflects the supervised and merging stages only, whereas TwIL-LM3-Pro also has
the MGPO stage. It is a reference point for the pipeline, not a checkpoint shipped in this
repository.

What that changes, on the family tables (one source, so the comparison is like for like):

| metric | VibeThinker-3B (base) | VibeThinker-webAI-trained | change |
|---|---:|---:|---:|
| macro gate | 0.374 | 0.508 | +0.134 |
| macro_primary | 0.444 | 0.579 | +0.135 |
| entailment | 0.480 | 0.685 | +0.205 |
| rule induction | 0.094 | 0.227 | +0.133 |
| lean_critic | 0.580 | 0.685 | +0.105 |
| `lm_corpus` perplexity ↓ | 18.70 | 7.35 | 2.5x lower |
| `math_corpus` perplexity ↓ | 21.80 | 7.00 | 3.1x lower |
| Track B, 10-dataset macro | 0.815 | 0.802 | −0.013 |
| Track B, 14-dataset macro | 0.729 | 0.728 | −0.001 |

The in-domain gain is large and the held-out change is inside sampling noise at n = 300 per
dataset, which is the same trade the pipeline makes on Granite 4.2. Two per-dataset shifts are
worth knowing: BBH-logic rises from 0.609 to 0.829, and IFEval falls from 0.660 to 0.557. Read the
base column of this table against the family source only; the lane tables above record the same
weights at a gate of 0.4118 from a separate run.

### Checkpoint selection

MGPO checkpoints were compared on both tracks, and step 2580 was published because it has the
best (or tied-best) held-out score rather than the best in-domain gate:

| checkpoint | macro gate | macro_primary | B10 | B14 |
|---|---:|---:|---:|---:|
| WiSE-FT α = 0.15 (RL initialiser) | 0.531 | 0.583 | — | — |
| MGPO step 1200 | **0.569** | **0.598** | 0.7819 | 0.7362 |
| MGPO step 2000 | 0.557 | 0.581 | 0.7882 | 0.7425 |
| MGPO step 2200 | 0.567 | 0.583 | 0.7865 | 0.7406 |
| **MGPO step 2580 (published)** | 0.554 | 0.588 | **0.7901** | **0.7425** |

Track A gate here uses the same definition as the tables above (rule induction included).
Step 1200 leads the gate by 0.015 and `macro_primary` by 0.010, but step 2580 has the highest
10-dataset macro and ties step 2000 on the 14-dataset macro (0.7425 for both at four decimals),
and the differences between the later checkpoints on Track A are within sampling noise at
n = 200. The checkpoint-selection probe recorded for this release (100 prompts each from FOL
translation, entailment and math MCQ, eight sampled completions per prompt at
`temperature = 0.8`, `top_p = 0.95`) gave macro Pass@1 0.4071 and macro Pass@8 0.5567. That probe
is a selection tool, not a benchmark claim.

## Usage

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

model_id = "webAI-Official/TwIL-LM3-Pro"
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. Use a
Transformers release with Granite 4.2 support.

The reported numbers use **greedy decoding** (`do_sample=False`) and a **2048-token** generation
budget. Note that the shipped `generation_config.json` enables sampling (`do_sample=true`,
`temperature=1.0`, `top_p=0.95`), so `do_sample=False` must be passed explicitly to reproduce the
evaluation. By default the chat template opens a `<think>` block, so the model reasons before it
answers and a short generation budget truncates that reasoning and scores far worse. The template
also accepts `enable_thinking=False` (empty think block, lower latency and lower quality on
reasoning-heavy tasks) and `reasoning_effort="low"` through `chat_template_kwargs`.

### GGUF / llama.cpp

Quantized GGUF builds ship in this repository alongside the safetensors weights. The Granite
architecture is supported by llama.cpp; the model uses a ChatML-style template with `<|im_end|>`
as EOS, so run it in conversation mode (`-cnv`).

| file | quant | size | bits/weight | notes |
|---|---|---:|---:|---|
| `TwIL-LM3-Pro-Q4_K_M.gguf` | Q4_K_M | 2.09 GiB | 4.91 | recommended default; runs on CPU or 4 GB of VRAM |
| `TwIL-LM3-Pro-Q5_K_M.gguf` | Q5_K_M | 2.43 GiB | 5.71 | a little more headroom than Q4_K_M |
| `TwIL-LM3-Pro-Q6_K.gguf` | Q6_K | 2.80 GiB | 6.57 | close to Q8_0 quality at about three-quarters the size |
| `TwIL-LM3-Pro-Q8_0.gguf` | Q8_0 | 3.63 GiB | 8.51 | near-lossless, for quality-sensitive use |
| `TwIL-LM3-Pro-F16.gguf` | F16 | 6.82 GiB | 16.01 | unquantized, for requantization or reference runs |

```bash
llama-cli -hf webAI-Official/TwIL-LM3-Pro:Q4_K_M -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.

F16 and Q8_0 were produced directly by `convert_hf_to_gguf.py` from the released bf16 weights; the
K-quants (Q4_K_M, Q5_K_M, Q6_K) were quantized from the F16 build with `llama-quantize`, without
an importance matrix. F16 is not bit-identical to the released weights: bf16 and f16 carry the
same 16 bits but trade exponent range against mantissa precision, so the conversion is a
narrowing one, in practice negligible for inference.

The published Track A and Track B numbers were measured on the **bf16** weights through vLLM, not
on any of these GGUF builds, so expect small deviations — most likely at Q4_K_M — that have not
been quantified here.

## How it was built

Five 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. **Multipath Distillation** to generate different reasoning traces from a given input prompt. 
3. **Checkpoint fusion** — parameter-space averaging of intermediate SFT checkpoints, rather
   than taking the final checkpoint.
4. **WiSE-FT interpolation** along with **TIES** and **DARE-SLERP** merging toward the pretrained base. This conservative
   interpolation is the direct reason held-out capability survives.
5. **MGPO + Contrastive step loss** — 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. Group size 16, learning rate 5e-6, sampling temperature 1.0, top-p 0.95,
   γ = 3.0. The run was resumed at step 800 with β = 0.02 and trained through step 2580, and the
   published checkpoint is **step 2580**. This release is the merged policy, not a LoRA adapter.

## One pipeline, several models

The recipe above is not specific to Granite 4.2. Each stage takes a base checkpoint, the shared
formal-logic corpus and the programmatic verifier as inputs and hands the next stage a checkpoint
of the same shape, so pointing the pipeline at a different base model does not change its
structure. In the internal family comparison, the same rank-64 LoRA stage and the same merge
families (WiSE-FT, DARE, SLERP) were run on five bases that differ in vocabulary, pretraining and
size: an earlier Granite, SmolLM3, the TwIL base, VibeThinker-3B (151,936-token vocabulary) and
Granite 4.2 (100,352). The MGPO stage was run on the two Granite bases.

The one setting that is chosen per model is the merge coefficient, picked by a sweep over held-out
performance: the best WiSE-FT weight is 0.15 for SmolLM3, 0.20 for Granite and the TwIL base, and
0.50 for VibeThinker-3B, which needs to keep far more of the tuned weights than the others do.

| base model | Track A macro gate (base → tuned) | Track B 10-dataset macro (base → tuned) |
|---|---:|---:|
| Granite | 0.309 → 0.454 | 0.777 → 0.786 |
| SmolLM3 | 0.344 → 0.446 | 0.723 → 0.736 |
| TwIL base | 0.423 → 0.435 | 0.729 → 0.716 |
| VibeThinker-3B | 0.374 → 0.541 | 0.810 → 0.802 |
| Granite 4.2 (this model)| 0.4313 → 0.5539 | 0.7942 → 0.7901 |

Track A improves on every base, from +0.012 to +0.167, and the Track B change stays within ±0.013,
inside sampling noise at n = 300 per dataset. The first four rows are from the family comparison
tables and the last from the paired run described under [Results](#results), so the base gates
are only comparable within a row. Reinforcement learning was applied only to the Granite bases
here, so the other rows show what the supervised and merging stages achieve without it.

## Limitations and caveats


**Verbose by construction.** Track A generations average 1,902 tokens and Track B generations
about 792, so cost per answer is substantially higher than the TwIL-LM family (564 and 482 tokens)
even though quality per answer is higher on Track A.

**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. The weak absolute areas inside the specialisation are FOL translation
(exact match 0.0100), `procedural` (strict 0.1200) and semantic parsing exact match (0.0000);
`rule_induction` parses only 56.5% of outputs.

**Comparability.** For Track A, TwIL-LM3-Pro, its base, VibeThinker-3B, Qwen3.5-4B, Qwen3-8B, LFM2-2.6B,
LFM2.5-8B-A1B and Llama-3.2-3B were checked to share the same sampled-row manifest and dataset
hash, seed and decoding; the TwIL-LM3 and gpt-oss-120b values are carried over from the TwIL-LM3
card, which describes the same harness. For Track B, the arms checked (including VibeThinker-3B
and Qwen3.5-4B, on all 18 tasks) share the same sampled rows and decoding, but the serving engine differs between
arms (vLLM 0.19.1 for TwIL-LM3-Pro, its base, Qwen3.5-4B, Qwen3-8B and LFM2.5-8B-A1B; vLLM 0.11.2 for
TwIL-LM3, Llama-3.2-3B and VibeThinker-3B), and the engine version is part of the protocol hash.
The VibeThinker-webAI-trained column (★) comes from the internal family comparison tables and is not
covered by the manifest checks described here. Throughput has its own, separate engine caveat (see the † note under the Track A table). With
n = 200 per lane on Track A and n = 300 per dataset on Track B, differences of two to three points
are within sampling noise.

## 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, default (thinking-enabled)
  chat template.
- Track B: 300 examples per task, greedy, `max_gen_toks = 4096`, `max_model_len = 8192`,
  `repetition_penalty = 1.0`, chat template applied with thinking disabled, vLLM backend.
- Both tracks use the same protocol for the model and its base, in a paired run over identical
  sampled rows.
- Throughput: 128 prompts drawn from a fixed Track A prompt file, 512 generated tokens each with
  EOS ignored, greedy, vLLM `gpu_memory_utilization` 0.45, `max_model_len` 4096, on an otherwise
  idle GPU (a single H200 for the TwIL-LM3-Pro, base and VibeThinker-3B runs); the reported rate is generated tokens over decode time, excluding engine start-up and
  compilation.

`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

TwIL-LM3-Pro applies the same post-training pipeline as the
[TwIL-LM3](https://huggingface.co/webAI-Official/TwIL-LM3) and TwIL-LM family — LoRA SFT,
checkpoint fusion, WiSE-FT and MGPO — to a different base, IBM's Granite 4.2 3B, instead of
SmolLM3 or SmolLM2 with some additional mechanisms. Compared with TwIL-LM3 it is a stronger in-domain model (macro gate 0.5539
against 0.4218) and a stronger held-out one (10-dataset macro 0.7901 against 0.7339), at the
price of much longer generations and a much higher truncation rate. Like the TwIL-LM models, it
ships as a full merged model on `main`, 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, [`ibm-granite/granite-4.2-3b`](https://huggingface.co/ibm-granite/granite-4.2-3b),
is Copyright IBM Corporation and is distributed under the Apache License 2.0; its licence text is
retained as `apache-2.0-LICENSE.txt` and all credit for the base model goes to IBM. 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.