TwIL-LM3-Pro from webAI, a 3.66B formal logic model built on Granite 4.2 3B

webAI has released TwIL-LM3-Pro, a 3.66B parameter model specialized for formal logic tasks such as entailment checking, rule induction, and Lean proof critique. Built on IBM Granite 4.2 3B, the model was post-trained using LoRA SFT, checkpoint merging, and RL against a programmatic verifier.

Performance Benchmarks

The model demonstrates strong performance relative to its size, effectively tying with models more than twice its parameter count on logic tasks:

• Logic Composite: 55.4 (vs. 43.1 for Granite base, 42.2 for original TwIL-LM3, and 53.4 for Qwen3-8B).
• Strict Multiple Choice Logic: 41% (vs. 17% for the next best model).
• BBH Logic: 95.4%.

While it matches Qwen3-8B on logic, it trails in general benchmarks (79.0 vs. 84.9 for Qwen3-8B) and loses to gpt-oss-120b on specific tasks like rule induction and Lean formalization.

Inference and Deployment

A key advantage is its efficiency on CPU-only hardware. Benchmarks show ~10.5 tokens/second on a CPU-only Xeon with 15 GiB RAM, which is 98x faster than Qwen3.8-27B on the same hardware. The model requires a long thinking budget (~1,900 tokens/answer), with a quarter of answers hitting the length cap.

• Availability: Supported in Ollama, LM Studio, and llama.cpp.
• Size: Q4_K_M GGUF is 2.09 GiB; Q5/Q6/Q8 up to 3.63 GiB.
• Requirements: Runs on CPU or 4 GB VRAM. Recommended temperature is 0 with a 2048+ token budget.