webAI’s 3B logic model runs locally at 32.9 answers per second

webAI has released TwIL-LM, a two-model family designed to translate English into first-order logic and test whether conclusions follow from stated premises. The models are available for local execution, with a 1.7B-parameter version and a 3B version aimed at users who cannot send sensitive data to a cloud service.

The release is notable less for raw benchmark leadership than for its size and operating requirements. The 3B model, TwIL-LM3, uses a merged fine-tune of SmolLM3-3B. The 1.7B model is a PEFT LoRA adapter for SmolLM2-1.7B-Instruct. webAI says the family can beat gpt-oss-120b on four of five formal-reasoning lanes in its announcement, although the detailed results show the 3B model trailing that 120B system on the overall six-lane average.

×

Local models for formal logic

The quantized builds are small enough for local hardware:

• TwIL-LM 1.7B: 1.06 GB in Q4_K_M format
• TwIL-LM3 3B: 1.78 GiB in Q4_K_M GGUF format, running on a CPU or with 4 GB of VRAM

The intended uses include first-order-logic translation, entailment classification, natural-language-to-structured-query conversion, Lean formalization drafting and critique, and a verifier layer for checking the output of a larger model. webAI specifically positions local execution for compliance, legal, financial, healthcare and formal-methods workflows where data may not leave the device.

Both checkpoints are released under the webAI Non-Commercial License 1.0. Organizations of any size can use them without a commercial license for non-revenue-generating work, but revenue-generating deployment requires a separate agreement with webAI.

How TwIL-LM3 was trained

TwIL-LM3 was built through four stages rather than a single fine-tuning pass:

• LoRA supervised fine-tuning on a synthetic formal-logic corpus.
• Checkpoint fusion, averaging intermediate supervised-fine-tuning checkpoints in parameter space.
• WiSE-FT interpolation toward the pretrained base, retaining only 25% of the fine-tuned delta with λ = 0.25.
• MGPO, an entropy-weighted GRPO stage trained against a programmatic verifier.

The published checkpoint is step 2071. That interpolation is central to webAI’s claim that the model transfers beyond its training distribution. A sibling model that skipped it reached a higher in-domain macro-gate score of 0.515, but lost roughly 12 points of held-out capability; webAI did not publish that sibling checkpoint.

Benchmark results and the unresolved commercial question

On the listed formal-logic tasks, webAI reports scores of 96.4 for rule induction, 87.6 for semantic parsing, 64.6 for Lean formalization, 52.0 for exact-format answering and 68.7 for entailment labeling.

On Track A, TwIL-LM3 records a 0.4488 six-lane average and a 0.4218 macro gate. That beats every tested arm through LFM2.5-8B-A1B on the objective lanes, despite using a third as many parameters. It does not beat the largest models: Qwen3-8B scores 0.5336 on the gate versus 0.4218, while gpt-oss-120b posts 0.5192 on the six-lane average versus 0.4488. Under the stricter strict-7 measure, Qwen3-8B scores 0.2093 and TwIL-LM3 scores 0.1971.

The efficiency results are stronger. On Track B, TwIL-LM3 generates an average of 482 tokens, the shortest output among the tested systems, and reaches 32.9 answers per second compared with 4.2 for gpt-oss-120b.

The model also shows a more favorable held-out tradeoff than its in-domain score alone suggests. Its macro gate rises from 0.336 to 0.422, a 26% relative improvement, while the held-out core average increases by 0.022. LogicBench improves from 0.6467 to 0.7167, although GSM8K slips from 0.8833 to 0.8733 and IFEval falls from 0.6767 to 0.6433.

The smaller model is less consistent: its macro-primary score reaches 0.361, compared with 0.185 for the unadapted base, but out-of-distribution LogicBench BQA rises only from 0.563 to 0.590 while GSM8K drops from 0.413 to 0.380 and ARC-C chain-of-thought declines from 0.587 to 0.463.

The reporting does not include independent benchmark verification, methodology beyond the model-card details, or commercial pricing and agreement terms. That leaves the practical business case unsettled even though the local hardware requirements are clear.

Our read is that TwIL-LM3 is a meaningful efficiency release, not a replacement for the largest reasoning models on aggregate accuracy. Its strongest case is constrained, privacy-sensitive formal-logic work where 32.9 answers per second on a 3B model matters more than beating gpt-oss-120b’s overall score. The non-commercial license sharply limits who can turn that efficiency into a product, so the commercial agreement—not the parameter count—will determine whether this becomes useful beyond research and internal verification.