README.md

---
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) 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

```python
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`](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.