webAI发布TwIL-LM：面向本地硬件的自动形式化逻辑模型家族

近日，webAI发布了名为TwIL-LM的形式逻辑推理模型系列，包括1.7B和3B参数的两个版本。其中，3B版本基于SmolLM3-3B进行微调；而1.7B版本则是在SmolLM2-1.7B-Instruct基础上添加了PEFT LoRA适配器。这两个模型均致力于将自然语言翻译成一阶逻辑，并检查结论是否从前提中得出，可以在本地硬件上运行，无需依赖云端资源。webAI表示，TwIL-LM在形式推理任务中的表现优于gpt-oss-120b。目前，该系列模型仅限于非商业用途，适用于合规和监管科技、金融服务、医疗保健与制药、法律合同操作以及形式方法研究等行业。