webAI выпустила TwIL-LM: компактные модели для формальной логики, работающие локально

Компания webAI выпустила TwIL-LM — семейство из двух моделей формально-логического вывода на 1,7 млрд и 3 млрд параметров. Старшая модель TwIL-LM3 получена слиянием донастроек SmolLM3-3B, а младшая — PEFT LoRA-адаптер для SmolLM2-1.7B-Instruct. Обе нацелены на автоформализацию: перевод естественного языка в логику первого порядка и проверку, следует ли вывод из посылок.

Модели полностью локальны: квантизованная версия 1.7B занимает 1,06 ГБ, 3B в формате Q4_K_M GGUF — 1,78 ГБ и работает на CPU или 4 ГБ видеопамяти. webAI заявляет, что TwIL-LM3 превосходит gpt-oss-120b по четырём из пяти направлений формального вывода. Однако модель доступна только для некоммерческого использования (лицензия webAI Non-Commercial License v1.0); для коммерческого развёртывания требуется отдельное соглашение.

TwIL-LM3 строилась в четыре этапа: LoRA-дообучение на синтетическом корпусе, слияние чекпоинтов, интерполяция WiSE-FT (λ=0.25) и этап MGPO с программным верификатором. Интересно, что вариант без интерполяции показал более высокие результаты на обучающей выборке, но потерял около 12 пунктов на удержанных данных — поэтому webAI опубликовала именно интерполированную версию.

Области применения: комплаенс и RegTech, финансовые услуги, здравоохранение, юридические и контрактные операции, формальные методы. Модели подходят для сред, где данные нельзя передавать за пределы устройства. Возможности: перевод в логику первого порядка, классификация логического следования, преобразование естественного языка в структурированные запросы, помощь в формализации Lean и верификация выходов более крупных моделей.