webAI推出TwIL-LM：用于本地自动形式化的形式逻辑模型系列

webAI发布了TwIL-LM，这是一个双模型家族的形式逻辑推理器，参数规模分别为1.7B和3B。其中3B成员TwIL-LM3是SmolLM3-3B的合并微调版本；1.7B成员是SmolLM2-1.7B-Instruct的PEFT LoRA适配器。两者都针对自动形式化：将英语翻译成一阶逻辑，并检查结论是否由其前提推出。两者均可本地运行，1.7B模型提供1.06 GB的量化版本，3B模型提供1.78 GiB的Q4_K_M GGUF格式。webAI的公告强调该发布在五项形式推理赛道中有四项超过了gpt-oss-120b。部署受到部分限制，因为两个检查点均以webAI非商业许可1.0版发布；产生收入的部署需要单独协议。这些模型面向多个行业，包括合规与监管科技、金融服务、医疗保健与制药、法律与合同运营，以及形式化方法研究。应用包括一阶逻辑（FOL）翻译、蕴涵分类、自然语言转结构化查询、Lean形式化草稿与评论，以及验证器层。TwIL-LM3的构建分为四个阶段：LoRA监督微调、检查点融合、WiSE-FT插值（λ=0.25）回预训练基础模型，以及针对程序化验证器运行的熵加权GRPO阶段（MGPO）。发布的检查点为第2071步。TwIL-LM3在规则归纳上得分96.4，语义解析87.6，Lean形式化64.6，精确格式回答52.0，蕴涵标注68.7。在Track A上，六赛道平均得分为0.4488，宏观门控得分为0.4218，领先除两个最大模型（Qwen3-8B和gpt-oss-120b）外的所有模型。效率是关键优势：TwIL-LM3生成的文本最短（482个标记），每秒回答数最多（32.9对4.2，后者为120B模型）。TwIL-LM3在领域内相对提升26%，同时在保留的领域外核心平均分上获得+0.022的提升，是唯一在两个轨道上均有提升的模型。1.7B模型提供了不同的权衡，但领域外结果参差不齐。关键要点：TwIL-LM3和TwIL-LM适用于非商业许可下的形式逻辑；TwIL-LM3在六赛道平均分上落后于gpt-oss-120b；其真正的优势在于效率；WiSE-FT（λ=0.25）是领域内提升不损害领域外表现的原因。