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

webAI has introduced TwIL-LM, a collection of language models designed to convert natural language into first-order logic and verify the validity of logical arguments. Available in 1.7B and 3B parameter sizes, these tools are optimized to run on consumer-grade hardware or CPUs. This release aims to simplify autoformalization tasks, though the models are currently restricted to non-commercial use.