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

webAI has put out TwIL-LM, a two-model family built for formal logic rather than general-purpose chatter. The pair comes in 1.7B and 3B parameter versions, both aimed at autoformalization: taking English statements and turning them into first-order logic, then checking whether a conclusion actually follows from the premises.

The bigger model, TwIL-LM3, starts from SmolLM3-3B and goes through a four-step training recipe: supervised fine-tuning on synthetic logic data, checkpoint fusion, WiSE-FT interpolation back toward the base model at λ = 0.25, and then MGPO against a programmatic verifier. webAI says that last interpolation matters a lot. Only a quarter of the fine-tuned delta is kept, and a sibling version that skipped it did better in-domain but gave back around twelve points of held-out capability.

This is also a local-first release. The 1.7B version ships as a 1.06 GB quantized build, while the 3B model is offered as a 1.78 GiB Q4_K_M GGUF that can run on CPU or with 4 GB of VRAM. webAI is framing that as useful for places where data cannot leave the device, with use cases that include compliance, RegTech, finance, healthcare, law, contract operations, and formal-methods research.

On its own scoreboard, TwIL-LM3 is not the biggest model in the room, and webAI does not pretend otherwise. The company says it trails gpt-oss-120b on the six-lane average, 0.4488 to 0.5192, but it moves fast: 482-token generations on Track B and 32.9 answers per second, versus 4.2 for the 120B model. It also improves on held-out transfer, which is the part that usually gets crushed when a model gets too specialized.

The smaller 1.7B model follows a similar pattern. Its macro-primary score rises to 0.361 from 0.185 for the base model, while some broader benchmarks improve and others slip. Both checkpoints are under webAI’s Non-Commercial License ver. 1.0, so anyone wanting revenue-generating deployment needs a separate agreement.