webAIは、ローカルハードウェアでの自動形式化を対象とした1.7Bおよび3Bパラメータの形式論理推論器2モデルからなる「TwIL-LM」をリリースした。これらのモデルは英語を一階述語論理に変換し、結論の有効性を検証するものであり、3Bバリアントはドメイン内形式論理タスクにおいてマクロゲートスコア0.4218を達成している。

  • TwIL-LM3 (3B) は SmolLM3-3B のマージファインチューンであり、1.7Bモデルは SmolLM2-1.7B-Instruct に対する PEFT LoRA アダプターである。
  • 両モデルはそれぞれ1.06 GBおよび1.78 GiBの量子化ビルドでローカル実行可能であり、VRAMは4 GBのみを必要とする。
  • トレーニングにはLoRA教師ありファインチューニング、チェックポイント融合、λ = 0.25におけるWiSE-FT補間、およびプログラム検証器に対するMGPOが含まれる。
  • TwIL-LM3はLFM2.5-8B-A1Bまでの全アームにおいて6つの客観的レーンで首位だが、gpt-oss-120bには6レーンの平均（0.4488対0.5192）で劣っている。
  • 3Bモデルは482トークンの最短生成を実現し、gpt-oss-120bの4.2に対して秒間32.9件の回答を生成する。

このリリースにより、コンプライアンスや法務運用などデータに敏感な環境でのローカル実行が可能になり、ドメイン内パフォーマンスとホールドアウト能力の保持のバランスを提供する。