TwIL-LM3-Pro

A 3.66B reasoning model for formal logic tasks, built from 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).

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. 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), 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.
• 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.

Model Details

Property	Value
Model ID	webAI-Official/TwIL-LM3-Pro
Base model	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, and the other peer columns are the values already published for TwIL-LM3 on its card, produced by that same harness (see Comparability). 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 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

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

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	best tuned configuration	Track A macro gate (base → tuned)	Track B 10-dataset macro (base → tuned)
Granite	WiSE-FT λ = 0.20	0.309 → 0.454	0.777 → 0.786
SmolLM3	WiSE-FT λ = 0.15	0.344 → 0.446	0.723 → 0.736
TwIL base	WiSE-FT λ = 0.20	0.423 → 0.435	0.729 → 0.716
VibeThinker-3B	WiSE-FT λ = 0.50	0.374 → 0.541	0.815 → 0.802
Granite 4.2 (this model)	MGPO β = 0.02, step 2580	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, 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 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, 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.