TwIL-LM2

A 1.7B reasoning model for formal logic tasks, built from HuggingFaceTB/SmolLM2-1.7B-Instruct through LoRA supervised fine-tuning, checkpoint fusion, WiSE-FT weight interpolation, and entropy-weighted GRPO reinforcement learning.

It raises in-domain formal-logic performance by +49% relative over its base model (macro gate 0.263 → 0.393), and on the strict, no-partial-credit reading of Track A it is the strongest model we have measured at any size — ahead of Qwen3-8B and of a 26B Gemma-4 MoE.

Its larger sibling, TwIL-LM3 (3B, from SmolLM3), trades a smaller in-domain gain for strictly better held-out retention. If you care about not regressing on general benchmarks, prefer that one.

Highlights

• Best strict-7 score of any model we have evaluated — 0.2386, against 0.2093 for Qwen3-8B and 0.2050 for Gemma-4-26B-A4B-it. Strict-7 gives no loose-match or partial credit anywhere, so it rewards emitting the exactly-requested form rather than merely reasoning near it.
• Structured-output accuracy is where the gain lands. Semantic parsing token-F1 0.8428 and Lean formalisation token-F1 0.6199 are both the highest in the comparison table below, by margins of roughly 0.39 and 0.21 over the next model.
• Rule induction nearly quadruples and entailment more than doubles over the base model (0.135 → 0.514 derivation score, 0.245 → 0.585 accuracy).
• Formatted answering becomes possible at all. Strict MCQ accuracy moves 0.000 → 0.160, where every other model in the comparison table scores 0.020 or below — including both 8B-and-larger arms, which answer the question correctly but almost never in the requested form.
• Lowest perplexity in the table on both held-out corpora (2.2981 language, 3.0390 maths), including against models up to fifteen times its size.
• Short answers. Track A generations average 460 tokens against the base model's 719, at 14,963 tok/s decode on one H100 — roughly 32 completed answers per second.
• Runs anywhere. 1.7B parameters in bf16, with Q4_K_M GGUF at 0.98 GiB for CPU or 2 GB of VRAM.

Two things this model is not: it is not a general assistant (see Limitations), and it does not preserve held-out benchmark performance — it gives back about a point of Track B macro relative to its base, which is the trade TwIL-LM3 was built to avoid.

Model Details

Property	Value
Model ID	webAI-Official/TwIL-LM (weights on main)
Base model	HuggingFaceTB/SmolLM2-1.7B-Instruct
Total parameters	1.71B
Architecture	Llama-style decoder-only transformer; 24 layers, hidden size 2048
Input / output	Text / text
Language	English
Tokenizer vocabulary size	49,152
Context window	8,192 tokens
Checkpoint precision	bfloat16 (3.19 GiB), plus Q4_K_M / Q5_K_M / Q8_0 / F16 GGUF builds
Post-training	LoRA SFT → checkpoint fusion → WiSE-FT (λ = 0.75) → MGPO reinforcement learning (step 1680)
Reasoning format	Emits a <think>…</think> block before the answer
Evaluated decoding	Greedy, 2048 new tokens, 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 8,192-token context is carried through unchanged; nothing in this pipeline extends or reduces it, and every reported score was measured inside that window.

Results

Track A — in-domain formal logic

Every arm below ran through the same harness, prompts and decoding settings described under Evaluation protocol — 200 prompts per objective, greedy, 2048 new tokens.

lane / metric	TwIL-LM2	SmolLM2-1.7B base	LFM2.5-1.2B-Thinking	LFM2-2.6B	Granite-4.1-3B	Llama-3.2-3B	Qwen3-8B	Gemma-4-26B-A4B-it
parameters	1.7B	1.7B	1.2B	2.6B	3B	3B	8B	26B (4B active)
lean_formalize token_f1	0.6199	0.1087	0.1890	0.1321	0.2652	0.3690	0.4022	0.4107
rule_induction derivation	0.5136	0.1350	0.0837	0.0615	0.2476	0.0825	0.3680	0.7319
entailment_label accuracy	0.5850	0.2450	0.4700	0.4700	0.4900	0.3300	0.5800	0.6200
mcq_answer accuracy	0.1600	0.0000	0.0000	0.0150	0.0100	0.0000	0.0000	0.0200
semantic_parse token_f1	0.8428	0.2155	0.4439	0.3665	0.1953	0.3102	0.4257	0.4567
lean_critic accuracy	0.5250	0.4950	0.5450	0.5900	0.5150	0.5300	0.7950	0.7500
lm_corpus perplexity ↓	2.2981	2.5845	5.0065	4.3815	2.4736	2.8478	2.5440	16.1145
math_corpus perplexity ↓	3.0390	3.2670	7.7402	6.7472	4.1162	4.7531	4.0083	59.7838
average, 6 lanes	0.5410	0.1999	0.2886	0.2725	0.2872	0.2703	0.4285	0.4982
strict-7	0.2386	0.1071	0.1450	0.1579	0.1507	0.1229	0.2093	0.2050
macro gate	0.3927	0.2590 †	0.3067	0.3473	0.3435	0.2925	0.5336	0.6344
macro_primary	0.3625	0.2900	0.3625	0.4188	0.3675	0.3450	0.5750	0.6100
mean generation length ↓	460	719	2464	2296	246	696	2094	1183

† The base column comes from the external-comparison run rather than the paired base-vs-TwIL run, hence 0.2590 against the 0.2630 quoted in the summary at the top of this card — run-to-run variation of the same checkpoint. The paired run is the correct basis for the improvement claim.

average, 6 lanes is the plain mean of the six objective rows above it, each at whatever scoring that row reports. It mixes token-F1 with accuracy, so it is coarse, but it is the broadest summary every arm can be compared on.

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

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. Exact match on generative lanes is near zero for every model, so it is a harsh scale — useful for ranking models against each other rather than as an absolute capability measure.

macro gate is the metric the training pipeline gates on: the equal-weight mean of the four bounded classification lanes (entailment_label, mcq_answer, procedural, lean_critic) plus rule_induction, scored by its continuous derivation score. Rule induction is included specifically so a fine-tune cannot pass the gate while quietly regressing inductive reasoning. 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.

macro_primary is the same mean over the four classification lanes alone, without rule_induction. It is kept for comparability with earlier reports, and it is the one summary where TwIL-LM2 looks unremarkable: it excludes all three lanes this model is strongest on (semantic_parse, lean_formalize, rule_induction) and it credits loose matches, which is where the larger models recover most of their score.

Read against models at its own scale, TwIL-LM2 wins outright. It beats its own base on all six objective lanes and all four summary rows, and it beats every 1–3B arm here on strict-7 by at least 0.08.

The more interesting comparison is upward. On strict-7 it leads the entire table — 0.2386 against 0.2093 for Qwen3-8B (4.7x the parameters) and 0.2050 for Gemma-4-26B-A4B-it — and it holds the best six-lane average at 0.5410 against Gemma's 0.4982. It also has the lowest perplexity in the table on both corpora.

It does not lead the macro gate, where Gemma-4-26B-A4B-it reaches 0.6344 and Qwen3-8B 0.5336 against 0.3927. Most of that gap is partial credit rather than capability: the gate credits mcq_answer and procedural at max(exact_match, loose_match), and both larger models answer those lanes correctly while almost never producing the requested form — Qwen3-8B's strict MCQ accuracy is 0.0000 against TwIL-LM2's 0.1600. Gemma also genuinely leads rule induction (0.7319) and entailment (0.6200), which no amount of scoring convention explains away.

So the honest reading is a split one. If what you need is a model that emits exactly the demanded formal object — a parse, a Lean statement, a bare label — this is the strongest option in the table and by some distance the smallest. If what you need is a model that gets the answer approximately right in free text, the 8B and 26B arms are better.

Track B — held-out benchmarks

Nothing in this suite was trained on. All arms are scored by the same aggregation over 300 randomly sampled, model-identical examples per dataset.

dataset	TwIL-LM2	SmolLM2-1.7B base	LFM2.5-1.2B-Thinking	LFM2-2.6B	Granite-4.1-3B	Llama-3.2-3B	Qwen3-8B	Gemma-4-26B-A4B-it
gsm8k	0.4633	0.4800	0.8400	0.8767	0.9100	0.8300	0.9567	0.9733
svamp	0.3833	0.4867	0.9167	0.9000	0.9000	0.8200	0.9367	0.9500
gsm_symbolic	0.2600	0.2200	0.6867	0.9767	0.9533	0.8067	0.8133	0.9967
arc_cot	0.5200	0.5100	0.8300	0.8667	0.8633	0.7967	0.9633	0.9767
logicbench	0.5400	0.5067	0.6700	0.6267	0.7367	0.5733	0.8567	0.8667
strategyqa	0.5900	0.6000	0.5933	0.6433	0.6333	0.6533	0.7400	0.7700
drop	0.4367	0.4233	0.6667	0.6900	0.7600	0.6733	0.8833	0.7933
csqa	0.4333	0.3967	0.6100	0.7433	0.7633	0.7500	0.8633	0.8633
musr	0.3131	0.4223	0.5227	0.4867	0.5669	0.4932	0.6301	0.6369
mmlu_redux	0.3933	0.4100	0.6400	0.7133	0.6800	0.6000	0.8500	0.9633
ifeval	0.4300	0.4700	0.8233	0.7300	0.7967	0.7167	0.8400	0.8733
rudas_ood	0.0289	0.0128	0.0089	0.0017	0.0355	0.0733	0.0468	0.1547
bbh_logic	0.2373	0.2447	0.5327	0.5713	0.7727	0.5333	0.6367	0.9940
math500	0.2100	0.1900	0.6867	0.7133	0.6067	0.4233	0.6100	0.9000
macro (10 CoT datasets)	0.4333	0.4456	0.6976	0.7523	0.7767	0.6997	0.8493	0.8790
macro (all 14)	0.3742	0.3838	0.6448	0.6814	0.7127	0.6245	0.7591	0.8366

The 10-dataset macro covers the chain-of-thought reasoning and QA sets (gsm8k, svamp, gsm_symbolic, arc_cot, logicbench, strategyqa, drop, csqa, musr, mmlu_redux); the 14-dataset macro adds ifeval, rudas_ood, bbh_logic and math500.

TwIL-LM2 is last in this table, and slightly below its own base. The 10-dataset macro moves 0.4456 → 0.4333 and the 14-dataset macro 0.3838 → 0.3742, so roughly one point is given back on both. Every other arm is larger, and the ordering is close to a size ordering, so the only like-for-like comparison here is against SmolLM2-1.7B — and that comparison is mildly negative.

Per dataset, the moves against the base go in both directions:

dataset	base	TwIL-LM2	Δ
gsm_symbolic	0.2200	0.2600	+0.040
csqa	0.3967	0.4333	+0.037
logicbench	0.5067	0.5400	+0.033
math500	0.1900	0.2100	+0.020
ifeval	0.4700	0.4300	−0.040
svamp	0.4867	0.3833	−0.103
musr	0.4223	0.3131	−0.109

The pattern is coherent: the sets that reward committing to a discrete, checkable answer improve (symbolic arithmetic, commonsense MCQ, propositional logic), and the sets that reward open-ended multi-step narrative reasoning lose (MuSR, SVAMP word problems). Instruction following also regresses, which is expected of a model tuned against verifiers rather than preferences. This model does not pass a no-regression bar on held-out tasks.

Usage

import torch
from transformers import AutoModelForCausalLM, AutoTokenizer

model_id = "webAI-Official/TwIL-LM"
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. The shipped generation_config.json carries no sampling defaults, so greedy is what you get unless you ask for otherwise. The model opens a <think>...</think> reasoning block before answering, so give it room — a short budget truncates the reasoning and scores far worse.

GGUF / llama.cpp

Quantized GGUF builds ship alongside the safetensors weights. The llama architecture is fully 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-LM2-Q4_K_M.gguf	Q4_K_M	0.98 GiB	4.93	recommended default; runs on CPU or 2 GB of VRAM
TwIL-LM2-Q5_K_M.gguf	Q5_K_M	1.14 GiB	5.73	a little more headroom than Q4_K_M
TwIL-LM2-Q8_0.gguf	Q8_0	1.70 GiB	8.51	near-lossless, for quality-sensitive use
TwIL-LM2-F16.gguf	F16	3.19 GiB	16.01	unquantized, for requantization or reference runs

llama-cli -m TwIL-LM2-Q4_K_M.gguf -cnv --temp 0 -n 2048

Pass --temp 0 and leave the generation budget at 2048 tokens or more: the model emits a <think> block before answering, and truncating it costs far more accuracy than the quantization does.

F16 was produced directly by convert_hf_to_gguf.py from the released bf16 weights; the K-quants were quantized from the F16 build with llama-quantize, without an importance matrix. Note that 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

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.75 — three quarters of the fine-tuned delta is retained. λ was chosen by constrained optimisation: maximise in-domain score subject to minimal degradation on held-out benchmarks. TwIL-LM3 keeps only a quarter of its delta, and that difference is most of why it holds Track B where this model does not.
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 1680.

Limitations and caveats

Held-out regression. The 10-dataset Track B macro moves 0.4456 → 0.4333 against the base. An earlier revision of this card quoted a narrower five-dataset "core average" that showed a small gain; the canonical 10- and 14-dataset macros in the table above are the numbers to use, and both are slightly negative.

Truncation. At a 2048-token budget, 6.9% of Track A generations hit the cap, down from 11.7% for the base. Our protocol marks a comparison rankable only below 2% truncation, so both the base and this model are formally not rankable on Track A and the macro gate should be read as indicative rather than exact. A truncated response scores zero regardless of whether its reasoning was sound, so both numbers are pessimistic — the base more so, meaning the true gap is probably narrower than +0.130.

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 in fact regressed.

Failed consolidation stage. A post-RL self-distillation round (SDFT) was attempted to recover held-out capability and made both tracks worse at every budget tried. 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. The comparison arms are scored on the same sampled rows as well.

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.

Track B is sampled at 300 examples per dataset for compute reasons. Absolute scores can shift on the full sets, but the comparative ordering across models is stable.

Relationship to prior releases

The main branch of this repository holds TwIL-LM2: a full merged model from a later point in the pipeline — after fusion, WiSE-FT interpolation and MGPO reinforcement learning — so it loads directly with AutoModelForCausalLM, with no adapter and no base checkpoint required. It is also mirrored on the TwIL-LM2 branch.

The original TwIL-LM (v1) release — a PEFT LoRA adapter for the supervised fine-tuning stage only — is archived on the TwIL-LM1 branch and matching tag. Load it with revision="TwIL-LM1".

The two are scored on different protocols and their headline numbers are not directly comparable: v1 reports a macro-primary average, while this card reports the five-component macro gate and the seven-lane strict mean described above.

TwIL-LM3 is the 3B member of the family, built from SmolLM3 by the same pipeline. It gains less in-domain than this model but improves its held-out scores at the same time, which this model does not.

License and attribution

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

The base model, HuggingFaceTB/SmolLM2-1.7B-Instruct, 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.