README.md

metadata

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 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) while holding held-out general capability roughly flat.

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.

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	SmolLM2-1.7B-Instruct	TwIL-LM2	Δ
entailment_label	0.245	0.585	+0.340
rule_induction	0.135	0.514	+0.379
lean_critic	0.490	0.525	+0.035
mcq_answer	0.290	0.270	−0.020
procedural	0.155	0.070	−0.085
macro gate	0.2630	0.3927	+0.1297

The gain is concentrated in entailment labelling and rule induction. MCQ answering and procedural reasoning regressed, and that is not hidden by the macro — it is averaged into the number above.

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.

	SmolLM2-1.7B-Instruct	TwIL-LM2	Δ
core average	0.499	0.508	+0.009
suite average (14 datasets)	0.384	0.374	−0.010

Per-dataset, largest moves in each direction:

dataset	base	TwIL-LM2	Δ
GSM-Symbolic	0.220	0.260	+0.040
CommonsenseQA	0.397	0.433	+0.037
LogicBench BQA	0.507	0.540	+0.033
MATH-500	0.190	0.210	+0.020
IFEval (strict)	0.470	0.430	−0.040
SVAMP	0.487	0.383	−0.103
MuSR	0.422	0.313	−0.109

This model does not pass a no-regression bar on held-out tasks. MuSR and SVAMP lose about ten points each. The suite average is slightly negative. The honest summary is that in-domain logic improves substantially and general capability is approximately preserved on average, with real losses on multi-step narrative and word-problem reasoning.

Usage

import torch
from transformers import AutoModelForCausalLM, AutoTokenizer

model_id = "webAI-Official/TwIL-LM"
tok = AutoTokenizer.from_pretrained(model_id, revision="TwIL-LM2")
model = AutoModelForCausalLM.from_pretrained(
    model_id, revision="TwIL-LM2", 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 model was trained and evaluated with greedy decoding (do_sample=False) and a 2048-token generation budget. It usually opens a <think>...</think> reasoning block before answering, so give it room — the reported numbers assume at least 2048 new tokens, and a shorter budget truncates reasoning and scores far worse.

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. λ was chosen by constrained optimisation: maximise in-domain score subject to minimal degradation on held-out benchmarks.
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

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.

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.

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 the main branch

The main branch of this repository holds the original TwIL-LM release: a PEFT LoRA adapter (plus GGUF builds) for the supervised fine-tuning stage only. This branch holds a full merged model from a later point in the pipeline — after fusion, WiSE-FT interpolation and MGPO reinforcement learning — so it is loaded directly with AutoModelForCausalLM, with no adapter and no base checkpoint required.

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

License and attribution

Released under the webAI Non-Commercial License ver. 1.0 — see LICENSE.md in this repository. This matches the licensing of the main branch.

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.