webAI Releases TwIL-LM: A 1.7B and 3B Formal-Logic Model Family for Autoformalization on Local Hardware

webAI has released TwIL-LM, a two-model family of formal-logic reasoners designed for autoformalization, translating English into first-order logic and checking whether a conclusion follows from its premises.

Model Family Overview

• TwIL-LM3 (3B parameters): A merged fine-tune of SmolLM3-3B. Runs locally with a 1.78 GiB Q4_K_M GGUF build.
• 1.7B Member: A PEFT LoRA adapter for SmolLM2-1.7B-Instruct. Runs locally with a 1.06 GB quantized build.
• Licensing: Both checkpoints ship under the webAI Non-Commercial License ver. 1.0. Revenue-generating deployment requires a separate agreement with webAI.

Training Pipeline

The base model undergoes four stages:

1. LoRA supervised fine-tuning on a synthetic formal-logic corpus.
2. Checkpoint fusion, averaging intermediate SFT checkpoints in parameter space.
3. WiSE-FT interpolation back toward the pretrained base at λ = 0.25. This step retained only a quarter of the fine-tuned delta, balancing in-domain performance with held-out generalization.
4. MGPO, an entropy-weighted GRPO stage run against a programmatic verifier.

Performance and Benchmarks

• Formal Reasoning: TwIL-LM3 surpassed gpt-oss-120b on four of five formal-reasoning lanes.
• Track A (In-domain formal logic):
  • TwIL-LM3 scored 0.4488 on the six-lane average and 0.4218 on the macro gate.
  • It leads LFM2.5-8B-A1B on all six objective lanes (0.4218 vs 0.3757) with a third of the parameters.
  • It does not lead the two largest arms (Qwen3-8B and gpt-oss-120b) in aggregate metrics. Under strict-7, Qwen3-8B scored 0.2093 and TwIL-LM3 scored 0.1971.
• Efficiency: TwIL-LM3 produced the shortest generations (482 tokens on Track B) and the most answers per second (32.9) compared to gpt-oss-120b's 4.2.
• Overall Improvement: TwIL-LM3 improved its in-domain macro gate by +26% relative (0.336 to 0.422) and gained +0.022 on the held-out core average, making it the only arm in the project to gain on both tracks.
  • LogicBench improved to 0.7167 from 0.6467.
  • GSM8K slipped slightly to 0.8733 from 0.8833.
  • IFEval regressed to 0.6433 from 0.6767.
• Specific Scores: webAI's announcement lists 96.4 on rule induction, 87.6 on semantic parsing, 64.6 on Lean formalization, 52.0 on exact-format answering, and 68.7 on entailment labeling.