---
language:
- en
library_name: transformers
pipeline_tag: text-generation
base_model: HuggingFaceTB/SmolLM2-1.7B-Instruct
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
- smollm2
- twil-lm
---
# TwIL-LM2
A 1.7B reasoning model for **formal logic** tasks, built from
[`HuggingFaceTB/SmolLM2-1.7B-Instruct`](https://huggingface.co/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**](https://huggingface.co/webAI-Official/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](#limitations-and-caveats)), 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`](https://huggingface.co/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 `…` 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](#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
```python
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 `...` 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 |
```bash
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
`` 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**](https://huggingface.co/webAI-Official/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`](https://huggingface.co/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.