webAI Launches TwIL-LM Models for Local Formal Reasoning

Formal-logic models translate human language into machine-checkable representations, such as first-order logic, that can be tested by symbolic solvers or proof systems. Autoformalization could make mathematical proof, software verification and reliable reasoning for AI agents more accessible. Running such models on local hardware also matters for organizations seeking lower latency and tighter control over computing costs, sensitive data and privacy requirements.

webAI released the TwIL-LM family on Aug. 10, 2026, offering models with 1.7 billion and 3 billion parameters for natural-language-to-FOL conversion, entailment classification and reasoning verification. The company said the 3B model beat OpenAI’s gpt-oss-120b on four of five formal-reasoning benchmarks despite using roughly 40 times fewer parameters, while delivering 2.6 times faster inference and running efficiently on consumer devices.