webAI выпустила TwIL-LM3-Pro - компактную модель на 3,66B параметров специально для формальной логики.

Модель построена на базе IBM Granite 4.2 3B и дообучена для задач вроде:

- проверки, следует ли вывод из заданных предпосылок
- перевода текста в формальную логику
- semantic parsing
- формализации и критики доказательств в Lean

По тестам webAI, TwIL-LM3-Pro примерно на уровне Qwen3-8B по главному composite-метрику формальной логики, при этом параметров у неё меньше чем вдвое. Также она обходит публичный VibeThinker-3B по всем шести заявленным formal-задачам.

- 3,66B параметров
- Q4 GGUF весит всего 2,09 GiB
- достаточно около 4 GB VRAM
- можно запускать через llama.cpp
- данные остаются локально

Это не универсальный чат-бот, а узкоспециализированная reasoning-модель. Лицензия — non-commercial.

https://huggingface.co/webAI-Official/TwIL-LM3-Pro