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 at 1.7B and 3B parameters. The 3B member, TwIL-LM3, is a merged fine-tune of SmolLM3-3B; the 1.7B member is a PEFT LoRA adapter for SmolLM2-1.7B-Instruct. Both target autoformalization: translating English into first-order logic and checking whether a conclusion follows from its premises. Both run locally, with a 1.06 GB quantized build for the 1.7B and a 1.78 GiB GGUF for the 3B. webAIs announcement frames the release around beating gpt-oss-120b on four of five formal-reasoning lanes. Is it deployable? Partially. Non-commercial use only, as of now. Both checkpoints ship under the webAI Non-Commercial License ver. 1.0. Revenue-generating deployment requires a separate agreement with webAI. Company level: any size....
webAI has released TwIL-LM, a two-model family of formal-logic reasoners at 1.7B and 3B parameters. The 3B member, TwIL-LM3, is a merged fine-tune of SmolLM3-3B; the 1.7B member is a PEFT LoRA adapter for SmolLM2-1.7B-Instruct. Both target autoformalization: translating English into first-order logic and checking whether a conclusion follows from its premises. Both run locally, with a 1.06 GB quantized build for the 1.7B and a 1.78 GiB GGUF for the 3B. webAIs announcement frames the release around beating gpt-oss-120b on four of five formal-reasoning lanes. Is it deployable? Partially. Non-commercial use only, as of now. Both checkpoints ship under the webAI Non-Commercial License ver. 1.0. Revenue-generating deployment requires a separate agreement with webAI. Company level: any size. The 3B GGUF is 1.78 GiB and runs on CPU or 4 GB of VRAM. The 1.7B is 1.06 GB. Industries: compliance and RegTech, financial services, healthcare and pharma, legal and contract operations, formal-methods research. webAI positions local execution for environments where data cannot leave the device. Applications: first-order logic (FOL) translation, entailment classification over premise sets, natural language to structured query, Lean formalization drafting and critique, and a verifier layer that checks a larger models output. How TwIL-LM3 was built? Four stages sit on top of the base model. LoRA supervised fine-tuning on a synthetic formal-logic corpus. Checkpoint fusion, averaging intermediate SFT checkpoints in parameter space. WiSE-FT interpolation back toward the pretrained base at λ = 0.25. Then MGPO, an entropy-weighted GRPO stage run against a programmatic verifier. The published checkpoint is step 2071. That λ is load-bearing: only a quarter of the fine-tuned delta is retained. A sibling arm that skipped the interpolation scored higher in-domain, at macro gate 0.515, but gave back roughly twelve points of held-out capability. webAI did not publish that arm. Performance webAI's