webAI 发布 TwIL-LM：1.7B 和 3B 形式逻辑模型家族，可在本地硬件上运行

webAI 发布了 TwIL-LM：https://huggingface.co/webAI-Official/TwIL-LM，这是一个参数为 1.7B 和 3B 的形式逻辑推理器双模型系列：https://www.webai.com/blog/webai-releases-twil-lm-a-family-of-formal-logic-models-that-outreason-a-120b-model-and-run-on-an-iphone。3B 成员 TwIL-LM3：https://huggingface.co/webAI-Official/TwIL-LM3，是 SmolLM3-3B：https://huggingface.co/HuggingFaceTB/SmolLM3-3B 的合并微调版本；1.7B 成员是 SmolLM2-1.7B-Instruct：https://huggingface.co/HuggingFaceTB/SmolLM2-1.7B-Instruct 的 PEFT LoRA 适配器。两者都针对自动形式化：https://arxiv.org/abs/2205.12615，旨在将英文翻译成一阶逻辑并检查结论是否从前提中得出。两者均可本地运行，1.7B 的量化版本为 1.06 GB，3B 的 Q4_K_M GGUF 为 1.78 GiB。webAI 的公告：https://www.webai.com/blog/webai-releases-twil-lm-a-family-of-formal-logic-models-that-outreason-a-120b-model-and-run-on-an-iphone 以在五条形式推理赛道中的四条击败 gpt-oss-120b 为发布重点。

部分。现阶段仅限非商业用途。

两个检查点均在 webAI 非商业许可 ver. 1.0 下发布：https://huggingface.co/webAI-Official/TwIL-LM3。产生收入的部署需与 webAI 签订单独协议。

四个阶段位于基础模型之上。首先在合成形式逻辑语料库上进行 LoRA 监督微调。检查点融合，在参数空间中平均中间 SFT 检查点。WiSE-FT 插值回到预训练基础模型，λ = 0.25。然后是 MGPO，即加权熵 GRPO：https://arxiv.org/abs/2402.03300 阶段，在程序化验证器上运行。公开的检查点为第 2071 步。

该 λ 值至关重要：仅保留微调增量的四分之一。跳过插值的兄弟分支在领域内得分更高，宏门控 0.515，但牺牲了大约十二点的外部能力。webAI 并未发布该分支。

webAI 的公告列出性能：规则归纳 96.4，语义解析 87.6，Lean 形式化 64.6，精确格式回答 52.0，蕴含标注 68.7。

它报告了两条赛道。在赛道A，即领域内形式逻辑方面，TwIL-LM3在六条 lanes 的平均得分为 0.4488，宏门控（训练流程依赖的指标）得分为 0.4218。它在所有六条客观 lanes 上超过了包括 LFM2.5-8B-A1B 在内的每个模型，0.4218 对比 0.3757，仅使用了约三分之一的参数。它并未领先两个最大模型。Qwen3-8B：https://huggingface.co/Qwen/Qwen3-8B 的宏门控得分达到 0.5336 对比 0.4218，但大部分属于宽松匹配分；在严格-7 条件下，两者得分分别为 0.2093 和 0.1971。gpt-oss-120b：https://huggingface.co/openai/gpt-oss-120b 的六条 lanes 平均分从 0.4488 提升至 0.5192。

效率方面模型卡说明明确。TwIL-LM3 生成的文本最短，在赛道B上为 482 个 token，因此每秒回答数最多，为 32.9，而 120B 仅为 4.2。

TwIL-LM3 在领域内相对提升 +26%，宏门控由 0.336 提升至 0.422，同时在保留核心平均分上也增加 +0.022。模型卡称它是项目中唯一在两条赛道上都有提升的模型。LogicBench 从 0.6467 提升至 0.7167。GSM8K 轻微下滑至 0.8733（原为 0.8833），IFEval 回退至 0.6433（原为 0.6767）。

1.7B 模型属于不同的权衡。其宏主指标得分为 0.361，而未经适配的基线为 0.185。分布外的结果表现参差：LogicBench BQA 提升至 0.590（原 0.563），而 GSM8K 下滑至 0.380（原 0.413），ARC-C 思维链下滑至 0.463（原 0.587）。

需要与我们合作推广你的 GitHub 仓库、Hugging Face 页面、产品发布或网络研讨会等？请联系我们：https://forms.gle/wbash1wF6efRj8G58

Asif Razzaq 是 Marktechpost Media Inc. 的首席执行官。作为一位有远见的企业家和工程师，Asif 致力于利用人工智能的潜力造福社会。他最近的努力是推出人工智能媒体平台 Marktechpost，该平台以深入报道机器学习和深度学习新闻而著称，既技术上可靠又便于广泛受众理解。该平台每月访问量超过 200 万，显示了其在受众中的受欢迎程度。

webAI has released TwIL-LM：https://huggingface.co/webAI-Official/TwIL-LM, a two-model family of formal-logic reasoners at 1.7B and 3B parameters：https://www.webai.com/blog/webai-releases-twil-lm-a-family-of-formal-logic-models-that-outreason-a-120b-model-and-run-on-an-iphone. The 3B member, TwIL-LM3：https://huggingface.co/webAI-Official/TwIL-LM3, is a merged fine-tune of SmolLM3-3B：https://huggingface.co/HuggingFaceTB/SmolLM3-3B; the 1.7B member is a PEFT LoRA adapter for SmolLM2-1.7B-Instruct：https://huggingface.co/HuggingFaceTB/SmolLM2-1.7B-Instruct. Both target autoformalization：https://arxiv.org/abs/2205.12615: translating English into first-order logic and checking whether a conclusion follows from its premises. Both run locally, with a 1.06 GB quantized build for the 1.7B and a 1.78 GiB Q4_K_M GGUF for the 3B. webAI’s announcement：https://www.webai.com/blog/webai-releases-twil-lm-a-family-of-formal-logic-models-that-outreason-a-120b-model-and-run-on-an-iphone frames the release around beating gpt-oss-120b on four of five formal-reasoning lanes.

Partially . Non-commercial use only, as of now.

Both checkpoints ship under the webAI Non-Commercial License ver. 1.0：https://huggingface.co/webAI-Official/TwIL-LM3. Revenue-generating deployment requires a separate agreement with webAI.

Four stages sit on top of the base model. LoRA supervised fine-tuning on a synthetic formal-logic corpus. Checkpoint fusion, averaging intermediate SFT checkpoints in parameter space. WiSE-FT interpolation back toward the pretrained base at λ = 0.25 . Then MGPO, an entropy-weighted GRPO：https://arxiv.org/abs/2402.03300 stage run against a programmatic verifier. The published checkpoint is step 2071.

That λ is load-bearing: only a quarter of the fine-tuned delta is retained. A sibling arm that skipped the interpolation scored higher in-domain, at macro gate 0.515, but gave back roughly twelve points of held-out capability. webAI did not publish that arm.

webAI's announcement lists 96.4 on rule induction, 87.6 on semantic parsing, 64.6 on Lean formalization, 52.0 on exact-format answering, and 68.7 on entailment labeling.

It reports two tracks. On Track A, in-domain formal logic, TwIL-LM3 scores 0.4488 on the six-lane average and 0.4218 on the macro gate, the metric the training pipeline gates on. It leads every arm up to and including LFM2.5-8B-A1B on all six objective lanes, at 0.4218 against 0.3757 with a third of the parameters. It does not lead the two largest arms. Qwen3-8B：https://huggingface.co/Qwen/Qwen3-8B takes the gate 0.5336 to 0.4218, but most of that is loose-match credit; under strict-7 the two sit at 0.2093 and 0.1971. gpt-oss-120b：https://huggingface.co/openai/gpt-oss-120b takes the six-lane average 0.5192 to 0.4488.

Efficiency is where the model card is unambiguous. TwIL-LM3 produces the shortest generations of any arm, 482 tokens on Track B, and consequently the most answers per second at 32.9 against the 120B's 4.2.

TwIL-LM3 improves in-domain by +26% relative, macro gate 0.336 to 0.422, while also gaining +0.022 on the held-out core average. The model card calls it the only arm in the project that gains on both tracks. LogicBench moves to 0.7167 from 0.6467. GSM8K slips slightly to 0.8733 from 0.8833, and IFEval regresses to 0.6433 from 0.6767.

The 1.7B is a different trade. Its macro-primary score is 0.361 against 0.185 for the unadapted base. Out-of-distribution results are mixed: LogicBench BQA improves to 0.590 from 0.563, while GSM8K falls to 0.380 from 0.413 and ARC-C chain-of-thought falls to 0.463 from 0.587.

Need to partner with us for promoting your GitHub Repo OR Hugging Face Page OR Product Release OR Webinar etc.? Connect with us ：https://forms.gle/wbash1wF6efRj8G58

Asif Razzaq is the CEO of Marktechpost Media Inc.. As a visionary entrepreneur and engineer, Asif is committed to harnessing the potential of Artificial Intelligence for social good. His most recent endeavor is the launch of an Artificial Intelligence Media Platform, Marktechpost, which stands out for its in-depth coverage of machine learning and deep learning news that is both technically sound and easily understandable by a wide audience. The platform boasts of over 2 million monthly views, illustrating its popularity among audiences.