README.md

metadata

language:
  - en
library_name: transformers
pipeline_tag: text-generation
base_model: HuggingFaceTB/SmolLM3-3B
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
  - smollm3
  - twil-lm

TwIL-LM3

A 3B reasoning model for formal logic tasks, built from HuggingFaceTB/SmolLM3-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 +26% relative over its base model (macro gate 0.336 → 0.422) and improves held-out benchmark performance at the same time (+0.022 core average). It is the only arm in this project that gains on both tracks, which is why it is the recommended release of the pair.

Results

Track A — in-domain formal logic

The macro gate is the mean of five objective scores: entailment labelling, multiple-choice answering, procedural reasoning, Lean proof critique, and rule induction (scored by its continuous derivation score). MCQ and procedural are credited as max(exact_match, loose_match). n = 200 prompts per objective, greedy decoding, 2048 max new tokens.

objective	SmolLM3-3B	TwIL-LM3	Δ
rule_induction	0.103	0.319	+0.216
entailment_label	0.335	0.575	+0.240
lean_critic	0.630	0.660	+0.030
procedural	0.105	0.110	+0.005
mcq_answer	0.505	0.445	−0.060
macro gate	0.3356	0.4218	+0.0862

Four of five objectives improve. MCQ answering regressed by six points, and that loss is averaged into the macro above rather than excluded.

Track B — held-out benchmarks

Nothing in this suite was trained on. Scores are re-derived from saved generations with delimiter-aware answer extractors rather than read from harness metrics.

	SmolLM3-3B	TwIL-LM3	Δ
core average	0.790	0.812	+0.022
suite average (14 datasets)	0.661	0.669	+0.008

This model passes the per-capability floor: no core or held-out transfer metric drops by more than the 0.02 tolerance against its base.

Per-dataset, largest moves in each direction:

dataset	base	TwIL-LM3	Δ
LogicBench BQA	0.647	0.717	+0.070
DROP	0.700	0.747	+0.047
CommonsenseQA	0.707	0.737	+0.030
StrategyQA	0.633	0.650	+0.017
MMLU-Redux	0.663	0.667	+0.003
GSM8K	0.883	0.873	−0.010
MATH-500	0.700	0.690	−0.010
IFEval (strict)	0.677	0.643	−0.033

Every regression is within 0.033, and the gains on logical-reasoning transfer tasks (LogicBench +0.070, DROP +0.047) are larger than any loss. IFEval is the one place worth noting — instruction-following degrades slightly, which is a common cost of verifier-driven RL.

Comparison against other open models

All arms below were run through the same harness, prompts and decoding settings described under Evaluation protocol. Throughput rows are reported because in-domain score alone is misleading for a 3B model: ans/s is defined throughout as tok/s ÷ mean generation length, so it measures completed answers rather than raw decode rate.

Track A — in-domain formal logic

lane / metric	TwIL-LM3	SmolLM3-3B base	Llama-3.2-3B	LFM2-2.6B	LFM2.5-8B-A1B	Qwen3-8B
lean_formalize token_f1	0.5869	0.4347	0.3690	0.1321	0.4655	0.4022
rule_induction derivation	0.3192	0.1029	0.0825	0.0615	0.1936	0.3680
entailment_label accuracy	0.5750	0.3750	0.3300	0.4700	0.5400	0.5800
mcq_answer accuracy	0.1100	0.0000	0.0000	0.0150	0.0750	0.0000
semantic_parse token_f1	0.4416	0.4149	0.3102	0.3665	0.3778	0.4257
lean_critic accuracy	0.6600	0.6500	0.5300	0.5900	0.5500	0.7950
lean_formalize exact_match	0.0050	0.0050	0.0000	0.0000	0.0000	0.0050
fol_translation exact_match	0.0000	0.0050	0.0000	0.0000	0.0000	0.0000
semantic_parse exact_match	0.0000	0.0050	0.0000	0.0000	0.0000	0.0000
procedural accuracy	0.0300	0.0050	0.0000	0.0300	0.0350	0.0850
procedural loose_match	0.1100	0.1050	0.1050	0.1150	0.1400	0.1800
mcq_answer loose_match	0.4450	0.5000	0.4150	0.5000	0.4550	0.7450
lm_corpus perplexity ↓	2.8972	3.1818	2.8478	4.3815	4.9472	2.5440
math_corpus perplexity ↓	3.8229	4.0685	4.7531	6.7472	8.3323	4.0083
macro gate	0.4218	0.3466 †	0.2925	0.3473	0.3757	0.5336
strict-7	0.1971	0.1493	0.1229	0.1579	0.1714	0.2093
tok/s	15880	15564	16160	25000	22000	not measured
mean gen length	564	999	696	2296	1830	2094
ans/s	28.1	15.6	23.2	10.9	12.0	not measured

† The base column here comes from the external-comparison run rather than the paired run used for the Δ table above, hence 0.3466 against 0.3356 — run-to-run variation of the same checkpoint. The paired run is the correct basis for the improvement claim.

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.

Qwen3-8B takes the macro gate at roughly 2.7x the parameter count, driven by the classification lanes — lean_critic 0.7950 and loose MCQ 0.7450. TwIL-LM3 holds the two lanes this pipeline targets most directly, lean_formalize token-F1 (0.5869 against 0.4022) and strict MCQ accuracy (0.1100, the only non-trivial value in that row), and it is the most efficient arm in the table by a wide margin: 28.1 answers/sec, from generations averaging 564 tokens where every other arm except Llama runs past 690.

Track B — held-out benchmarks

dataset	TwIL-LM3	SmolLM3-3B base	Llama-3.2-3B	LFM2-2.6B	LFM2.5-8B-A1B	Qwen3-8B	gpt-oss-120b ‡
gsm8k	0.8733	0.8833	0.8300	0.8767	0.9133	0.9567	0.9767
svamp	0.8500	0.8567	0.8200	0.9000	0.9133	0.9400	0.9400
gsm_symbolic	0.7567	0.7633	0.8067	0.9767	0.9267	0.8133	0.8467
arc_cot	0.8467	0.8400	0.7967	0.8667	0.9033	0.9633	0.9667
logicbench	0.7167	0.6467	0.5733	0.6267	0.7200	0.8567	0.8533
strategyqa	0.6500	0.6333	0.6533	0.6433	0.6667	0.7400	0.7867
drop	0.7467	0.7000	0.6733	0.6900	0.6633	0.8833	0.8500
csqa	0.7367	0.7067	0.7500	0.7433	0.7700	0.8633	0.8367
musr	0.4957	0.4997	0.4932	0.4867	0.5703	0.6301	0.6852
mmlu_redux	0.6667	0.6633	0.6000	0.7133	0.8367	0.8500	0.9467
ifeval	0.6433	0.6767	0.7167	0.7300	0.8900	0.8400	0.7900
rudas_ood	0.0365	0.0209	0.0733	0.0017	0.0061	0.0468	0.0000 §
bbh_logic	0.6633	0.6667	0.5333	0.5713	0.7700	0.6367	0.9980
math500	0.6900	0.7000	0.4233	0.7133	0.7800	0.6100	0.8433
macro (10 CoT datasets)	0.7339	0.7193	0.6997	0.7523	0.7884	0.8493	0.8689
macro (all 14)	0.6694	0.6612	0.6245	0.6814	0.7378	0.7591	0.8086
tok/s	15880	15564	16160	25000	22000	not measured	3374
mean gen length	482	626	510	≈796	≈1327	≈1931	801
ans/s	32.9	24.9	31.7	≈31.4	≈16.6	not measured	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.

Lengths marked ≈ are derived from stored generations using each model's characters-per-token ratio rather than re-tokenized directly; the method reproduces the three directly measured lengths to within 3.5%.

The honest summary of this table is that TwIL-LM3 does not lead it. Larger models score higher, in order of size, and the 120B leads nine of fourteen rows. Two things are worth extracting anyway. First, TwIL-LM3 improves on its own base while sitting mid-table (0.7339 against 0.7193 on the 10-dataset macro), which is the point of the WiSE-FT stage — in-domain gains without transfer collapse. Second, it produces the shortest generations of any arm here at 482 tokens and consequently the most answers per second at 32.9, roughly eight times the 120B's rate.

Usage

import torch
from transformers import AutoModelForCausalLM, AutoTokenizer

model_id = "webAI-Official/TwIL-LM3"
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. Note that the shipped generation_config.json inherits SmolLM3's sampling defaults (do_sample=true, temperature=0.6, top_p=0.95), so do_sample=False must be passed explicitly to reproduce the evaluation. The model opens a <think>...</think> reasoning block before answering, so a short generation budget truncates reasoning and scores far worse.

GGUF / llama.cpp

Quantized GGUF builds ship in this repository alongside the safetensors weights. The smollm3 architecture is 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-LM3-Q4_K_M.gguf	Q4_K_M	1.78 GiB	4.96	recommended default; runs on CPU or 4 GB of VRAM
TwIL-LM3-Q8_0.gguf	Q8_0	3.05 GiB	8.50	near-lossless, for quality-sensitive use

llama-cli -m TwIL-LM3-Q4_K_M.gguf -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.

Q8_0 was produced directly by convert_hf_to_gguf.py from the released bf16 weights; Q4_K_M was produced from an F16 conversion with llama-quantize, without an importance matrix. Both builds were smoke-tested for load and generation on CPU. The published Track A and Track B numbers were measured on the bf16 weights through vLLM, not on these GGUF builds, so expect small deviations 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.25 — i.e. only a quarter of the fine-tuned delta is retained. λ was chosen by constrained optimisation: maximise in-domain score subject to minimal degradation on held-out benchmarks. This conservative λ is the direct reason held-out capability survives.
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 2071.

A sibling arm that skipped stage 3's conservative interpolation scores considerably higher in-domain (macro gate 0.515) but gives back roughly twelve points of held-out capability. This release is the balanced point of that trade; the other was not published.

Limitations and caveats

Truncation. At a 2048-token budget, 4.4% of Track A generations hit the cap — better than the base's 17.4%, but still above the 2% threshold our protocol requires to mark a comparison rankable. The Track A macro gate should therefore be read as indicative rather than exact. Because a truncated response scores zero regardless of reasoning quality, both numbers are pessimistic, and the base substantially more so — meaning the true Track A gap is probably narrower than +0.086.

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 regressed slightly.

Failed consolidation stage. A post-RL self-distillation round (SDFT) was attempted and made both tracks worse at every budget tried (−18% Track A at one epoch on this family). 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.

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

webAI-Official/TwIL-LM is the 1.7B member of this family, built from SmolLM2 by the same pipeline. It reaches a higher in-domain score relative to its own base but gives back held-out capability; this model is the one that improves both. Unlike TwIL-LM's main branch, which ships a PEFT LoRA adapter, this repository ships a full merged model 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, HuggingFaceTB/SmolLM3-3B, 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.