Update TwIL-LM3: weights, tokenizer and model card

README.md

@@ -28,9 +28,10 @@ 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).
+(+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.
 
-<!-- ![TwIL-LM3 formal and general reasoning benchmarks against gpt-oss-120b, Qwen3-8B, LFM2-2.6B and Llama-3.2-3B](benchmarks.jpg) -->
+![TwIL-LM3 formal and general reasoning benchmarks against gpt-oss-120b, Qwen3-8B, LFM2-2.6B and Llama-3.2-3B](benchmarks.jpg)
 
 ## Results
 
@@ -63,6 +64,8 @@ delimiter-aware answer extractors rather than read from harness metrics.
 | 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:
 
@@ -90,40 +93,55 @@ 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 |
-|---|---:|---:|---:|---:|---:|
-| lean_formalize token_f1 | **0.5869** | 0.4347 | 0.3690 | 0.1321 | 0.4655 |
-| rule_induction derivation | **0.3192** | 0.1029 | 0.0825 | 0.0615 | 0.1936 |
-| entailment_label accuracy | **0.5750** | 0.3750 | 0.3300 | 0.4700 | 0.5400 |
-| mcq_answer accuracy | **0.1100** | 0.0000 | 0.0000 | 0.0150 | 0.0750 |
-| semantic_parse token_f1 | **0.4416** | 0.4149 | 0.3102 | 0.3665 | 0.3778 |
-| lean_critic accuracy | **0.6600** | 0.6500 | 0.5300 | 0.5900 | 0.5500 |
-| lean_formalize exact_match | 0.0050 | 0.0050 | 0.0000 | 0.0000 | 0.0000 |
-| fol_translation exact_match | 0.0000 | 0.0050 | 0.0000 | 0.0000 | 0.0000 |
-| semantic_parse exact_match | 0.0000 | 0.0050 | 0.0000 | 0.0000 | 0.0000 |
-| procedural accuracy | 0.0300 | 0.0050 | 0.0000 | 0.0300 | **0.0350** |
-| procedural loose_match | 0.1100 | 0.1050 | 0.1050 | 0.1150 | **0.1400** |
-| mcq_answer loose_match | 0.4450 | 0.5000 | 0.4150 | 0.5000 | 0.4550 |
-| lm_corpus perplexity ↓ | 2.8972 | 3.1818 | **2.8478** | 4.3815 | 4.9472 |
-| math_corpus perplexity ↓ | **3.8229** | 4.0685 | 4.7531 | 6.7472 | 8.3323 |
-| **macro gate** | **0.4218** | 0.3466 † | 0.2925 | 0.3473 | 0.3757 |
-| **strict-7** | **0.1971** | 0.1493 | 0.1229 | 0.1579 | 0.1714 |
-| tok/s | 15880 | 15564 | 16160 | 25000 | 22000 |
-| mean gen length | **564** | 999 | 696 | 2296 | 1830 |
-| **ans/s** | **28.1** | 15.6 | 23.2 | 10.9 | 12.0 |
-
+| lane / metric | TwIL-LM3 | TwIL-LM3* | SmolLM3-3B base | Llama-3.2-3B | LFM2-2.6B | LFM2.5-8B-A1B |
+|---|---:|---:|---:|---:|---:|---:|
+| lean_formalize token_f1 | 0.5869 | **0.6456** | 0.4347 | 0.3690 | 0.1321 | 0.4655 |
+| rule_induction derivation | 0.3192 | **0.9644** | 0.1029 | 0.0825 | 0.0615 | 0.1936 |
+| entailment_label accuracy | 0.5750 | **0.6867** | 0.3750 | 0.3300 | 0.4700 | 0.5400 |
+| mcq_answer accuracy | 0.1100 | **0.5200** | 0.0000 | 0.0000 | 0.0150 | 0.0750 |
+| semantic_parse token_f1 | 0.4416 | **0.8762** | 0.4149 | 0.3102 | 0.3665 | 0.3778 |
+| lean_critic accuracy | **0.6600** | 0.5200 | 0.6500 | 0.5300 | 0.5900 | 0.5500 |
+| lean_formalize exact_match | 0.0050 | — | 0.0050 | 0.0000 | 0.0000 | 0.0000 |
+| fol_translation exact_match | 0.0000 | — | 0.0050 | 0.0000 | 0.0000 | 0.0000 |
+| semantic_parse exact_match | 0.0000 | — | 0.0050 | 0.0000 | 0.0000 | 0.0000 |
+| procedural accuracy | 0.0300 | — | 0.0050 | 0.0000 | 0.0300 | **0.0350** |
+| procedural loose_match | 0.1100 | — | 0.1050 | 0.1050 | 0.1150 | **0.1400** |
+| mcq_answer loose_match | 0.4450 | — | 0.5000 | 0.4150 | 0.5000 | 0.4550 |
+| lm_corpus perplexity ↓ | 2.8972 | 3.1284 | 3.1818 | **2.8478** | 4.3815 | 4.9472 |
+| math_corpus perplexity ↓ | 3.8229 | **3.5245** | 4.0685 | 4.7531 | 6.7472 | 8.3323 |
+| **macro gate** | 0.4218 | **0.5896** | 0.3466 † | 0.2925 | 0.3473 | 0.3757 |
+| **strict-7** | 0.1971 | **0.3290** | 0.1493 | 0.1229 | 0.1579 | 0.1714 |
+| macro_primary | 0.4475 | **0.4958** | 0.4075 | 0.3450 | 0.4188 | 0.4213 |
+| tok/s | 15880 | — | 15564 | 16160 | 25000 | 22000 |
+| mean gen length | **564** | — | 999 | 696 | 2296 | 1830 |
+| **ans/s** | **28.1** | — | 15.6 | 23.2 | 10.9 | 12.0 |
+
+\* **TwIL-LM3\*** is our latest version of TwIL-LM3. **The weights will be released soon** — the
+files in this repository are the current TwIL-LM3 release, not this one. Lanes marked — are not
+yet reported for it.
+
+† 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.
 
-TwIL-LM3 leads both headline metrics here and wins every lane the pipeline targets directly:
-`lean_formalize` token-F1 0.5869 against 0.4655 for the nearest arm, `rule_induction` 0.3192
-against 0.1936, and strict MCQ accuracy 0.1100, the only non-trivial value in that row. Its
-closest competitor on the macro gate is LFM2.5-8B-A1B at 0.3757, roughly 2.8x its size. What it
-gives up: `procedural` under both scorings, loose MCQ where the base and LFM2-2.6B reach 0.5000
-against its 0.4450, `lm_corpus` perplexity where Llama-3.2-3B is marginally lower, and the three
-exact-match rows that sit at or near zero for every arm.
+Among the released models, TwIL-LM3 leads both headline metrics and wins every lane the pipeline
+targets directly: `lean_formalize` token-F1 0.5869 against 0.4655 for the nearest arm,
+`rule_induction` 0.3192 against 0.1936, and strict MCQ accuracy 0.1100, the only non-trivial
+value in that row. Its closest competitor on the macro gate is LFM2.5-8B-A1B at 0.3757, roughly
+2.8x its size. What it gives up: `procedural` under both scorings, loose MCQ where the base and
+LFM2-2.6B reach 0.5000 against its 0.4450, `lm_corpus` perplexity where Llama-3.2-3B is
+marginally lower, and the three exact-match rows that sit at or near zero for every arm.
+
+The unreleased TwIL-LM3\* moves the gate to 0.5896 and strict-7 to 0.3290, roughly +0.17 and
++0.13 over the current release. The gains are concentrated in the two lanes where TwIL-LM3 is
+weakest in absolute terms rather than relative ones — `rule_induction` 0.3192 → 0.9644 and
+`semantic_parse` token-F1 0.4416 → 0.8762 — plus strict MCQ accuracy 0.1100 → 0.5200. It gives
+back `lean_critic` (0.6600 → 0.5200) and a little `lm_corpus` perplexity, so it is not uniformly
+better.
 
 It is also 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. The Liquid
@@ -163,7 +181,9 @@ Lengths marked ≈ are derived from stored generations using each model's charac
 ratio rather than re-tokenized directly; the method reproduces the three directly measured
 lengths to within 3.5%.
 
-First, TwIL-LM3 improves on its own base while sitting mid-table (0.7339 against 0.7193
+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.
@@ -260,7 +280,10 @@ release is the balanced point of that trade; the other was not published.
 
 **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`. 
+`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