webAI TwIL-LM: 1.7B and 3B Formal-Logic Models for Local Hardware

webAI has released TwIL-LM, a two-model family targeting autoformalization — translating natural-language statements into first-order logic and classifying whether a conclusion follows from a given premise set. The family consists of TwIL-LM3, a merged fine-tune of SmolLM3-3B at 3 billion parameters, and a 1.7B PEFT LoRA adapter for SmolLM2-1.7B-Instruct. Both ship under the webAI Non-Commercial License ver. 1.0; revenue-generating deployment requires a separate agreement with webAI. For practitioners interested in small language models with constrained hardware budgets, the hardware floor is genuinely low: the 3B Q4_K_M GGUF weighs 1.78 GiB and runs on CPU or 4 GB of VRAM, while the 1.7B Q4_K_M quantized build is 1.06 GB.

Training Pipeline

TwIL-LM3 is produced through four stages stacked on SmolLM3-3B. Stage 1 is LoRA supervised fine-tuning on a synthetic formal-logic corpus spanning FOL translation, entailment labeling, semantic parsing, Lean formalization and critique, and rule induction. Stage 2 averages intermediate SFT checkpoints in parameter space — a checkpoint fusion step selected by a diversity probe. Stage 3 applies WiSE-FT interpolation back toward the pretrained base at λ = 0.25, retaining only a quarter of the fine-tuned weight delta: W = (1 − λ)·W_base + λ·W_finetuned. Stage 4 runs MGPO, an entropy-weighted GRPO reinforcement-learning pass against a programmatic verifier that awards partial credit via token-F1, ensuring all-fail prompt groups still contribute gradient. The published checkpoint is step 2071.

The λ = 0.25 choice is load-bearing. A sibling training arm that skipped WiSE-FT interpolation scored higher in-domain — macro gate 0.515 — but surrendered roughly twelve points of held-out capability. webAI did not release that arm. The published model gains on both tracks simultaneously: +26% relative improvement in-domain (macro gate 0.336 → 0.422) while posting a +0.022 gain on the held-out core average.

Benchmark Performance and the Shipping-vs-Announced Gap

webAI's announcement cites five scores: 96.4 on rule induction, 87.6 on semantic parsing, 64.6 on Lean formalization, 52.0 on exact-format MCQ answering, and 68.7 on entailment labeling. Those figures belong to TwIL-LM3*, an unreleased checkpoint. The shipping model scores differently across the same six-lane Track A suite.

The shipping checkpoint trails gpt-oss-120b on the six-lane average, 0.4488 to 0.5192. It outperforms every evaluated arm up to and including LFM2.5-8B-A1B on the macro gate metric (0.4218 vs. 0.3757 at a third of the parameters). Against Qwen3-8B the gate score is 0.4218 to 0.5336, but under strict-7 evaluation the two converge to 0.1971 and 0.2093 respectively, indicating Qwen3-8B's lead is largely loose-match credit. Out-of-domain, LogicBench rises to 0.7167 from 0.6467, GSM8K slips to 0.8733 from 0.8833, and IFEval regresses to 0.6433 from 0.6767.

Throughput

Track B throughput is where TwIL-LM3 separates from the 120B comparison without ambiguity. The model generates a mean of 482 tokens per answer — the shortest of any arm evaluated — and delivers 32.9 answers per second at 15,880 tokens per second. gpt-oss-120b, run at MXFP4 on tensor-parallel 2 and therefore not directly comparable, produces 4.2 answers per second at 3,374 tokens per second with a mean generation length of 801 tokens. webAI's blog characterises the throughput differential as 2.6×; the Track B table implies roughly 8× under the measured conditions.

The 1.7B model trades absolute score for adapter flexibility. Its macro-primary score reaches 0.361 against 0.185 for the unadapted SmolLM2-1.7B-Instruct base. Out-of-distribution results are mixed: LogicBench BQA improves to 0.590 from 0.563, while GSM8K falls to 0.380 from 0.413 and ARC-C chain-of-thought drops to 0.463 from 0.587.

The release positions TwIL-LM as a verifier layer for larger-model pipelines — checking a 70B or 120B model's formal-logic output rather than replacing it — a pattern gaining traction as agentic data science workflows increasingly demand cheap, local verification passes before expensive upstream calls. The open question is the gap between the shipping checkpoint and the unreleased TwIL-LM3*: a rule-induction score of 96.44 versus 31.92 is not a rounding difference, and whether those weights ship under the same license will determine whether the headline benchmark claims translate into practical adoption.