webAI releases formal logic reasoning models

webAI published TwIL-LM, a family of formal-logic reasoning models at 1.7B and 3B parameters designed for autoformalization tasks. The models translate English statements into first-order logic and verify logical conclusions, running locally on consumer hardware with quantized builds under 2GB. Company benchmarks show the 3B variant outperforms larger models on four of five formal reasoning benchmarks, though deployment requires a non-commercial license or separate commercial agreement.