webAI выкатила TwIL-LM3-Pro — компактную штуку на 3,66B параметров, заточенную строго под формальную логику. Сделана поверх IBM Granite 4.2 3B, а дальше её дообучали под конкретику: проверить, вытекает ли вывод из заданных предпосылок, перегнать текст в формальную логику, semantic parsing, а ещё формализовать и раскритиковать доказательства в Lean.

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

Q4 GGUF тянет всего на 2,09 GiB, хватит около 4 GB VRAM, запуск — через llama.cpp, и данные никуда не уезжают. Это не болталка на все случаи жизни, а узкая reasoning-модель под конкретный класс задач. Лицензия — non-commercial. TwIL-LM3-Pro на Hugging Face

👉 About Python