webAI has released TwIL-LM, a two-model family of formal-logic reasoners with 1.7B and 3B parameters designed for autoformalization on local hardware. The models translate English into first-order logic and check conclusion validity, with the 3B variant achieving a macro gate score of 0.4218 on in-domain formal logic tasks.

  • TwIL-LM3 (3B) is a merged fine-tune of SmolLM3-3B, while the 1.7B model is a PEFT LoRA adapter for SmolLM2-1.7B-Instruct.
  • Both models run locally with quantized builds of 1.06 GB and 1.78 GiB respectively, requiring only 4 GB of VRAM.
  • Training involved LoRA supervised fine-tuning, checkpoint fusion, WiSE-FT interpolation at λ = 0.25, and MGPO against a programmatic verifier.
  • TwIL-LM3 leads all arms up to LFM2.5-8B-A1B on six objective lanes but trails gpt-oss-120b on the six-lane average (0.4488 vs 0.5192).
  • The 3B model produces the shortest generations at 482 tokens, yielding 32.9 answers per second compared to gpt-oss-120b's 4.2.

The release enables local execution for data-sensitive environments like compliance and legal operations, offering a balance between in-domain performance and held-out capability retention.