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 Q4_K_M GGUF for the 3B. webAI’s 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 Q4_K_M GGUF is 1.78 GiB and runs on CPU or 4 GB of VRAM. The 1.7B Q4_K_M is 1.06 GB. Industries: compliance and RegTech, financial services, health...
