Релиз семейого моделей TwIL-LM от webAI

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

Новинки оптимизированы для запуска на локальном оборудовании. Квантованная сборка младшей модификации занимает всего 1,06 гигабайта, в то время как вариант TwIL-LM3 распространяется в формате Q4_K_M GGUF объемом 1,78 гигабайта. В официальном анонсе разработчики делают акцент на том, что их модель превосходит gpt-oss-120b в четырех из пяти категорий формальных рассуждений. Тем не менее, практическое развертывание имеет ограничения: на данный момент модели доступны исключительно для некоммерческого применения в соответствии с лицензией webAI Non-Commercial License версии 1.0. Для внедрения в коммерческие продукты, приносящие доход, требуется заключение отдельного соглашения с компанией независимо от масштаба организации.

Технические характеристики и сферы применения

Модель TwIL-LM3 в формате Q4_K_M GGUF требует для работы процессор или всего 4 гигабайта видеопамяти при весе в 1,78 гигабайта, а 1,7-миллиардная версия обходится 1,06 гигабайта. Подобные показатели открывают возможности для использования в различных отраслях, включая комплаенс и RegTech, финансовый сектор, здравоохранение и фармацевтику, юридическую сферу и управление контрактами, а также фундаментальные исследования в области формальных методов. Локальное выполнение особенно актуально для сценариев, где конфиденциальные данные не должны покидать устройство пользователя.

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

Архитектура и методика обучения TwIL-LM3

Процесс создания TwIL-LM3 состоял из четырех последовательных этапов поверх базовой модели. Сначала проводилось контролируемое дообучение методом LoRA на синтетическом корпусе данных по формальной логике. Затем выполнялось объединение контрольных точек посредством усреднения промежуточных весов SFT в пространстве параметров. На третьем этапе применялась интерполяция WiSE-FT обратно к предобученной базе с коэффициентом λ = 0.25. Завершающим шагом стало использование алгоритма MGPO — взвешенного по энтропии метода GRPO, реализованного с привлечением программного верификатора. Опубликованная версия соответствует контрольной точке на шаге 2071.

Выбранный коэффициент интерполяции играет критическую роль: в итоговой модели сохраняется лишь четверть дельты, полученной при дообучении. Параллельная ветка обучения без этапа интерполяции демонстрировала лучшие результаты в рамках домена (макро-гейт 0.515), но теряла около двенадцати пунктов на отложенных тестах общих возможностей, из-за чего компания не стала публиковать этот вариант.

Показатели производительности и эффективности

В официальных материалах приводятся следующие результаты: 96,4 балла в индукции правил, 87,6 в семантическом парсинге, 64,6 в формализации Lean, 52,0 в ответах с точным форматированием и 68,7 в разметке логического следования. Тестирование проводилось в рамках двух направлений. На треке A (формальная логика внутри домена) TwIL-LM3 набирает 0,4488 по усредненному показателю шести направлений и 0,4218 по макро-гейту, который выступал в качестве целевой метрики при обучении. Модель опережает все решения вплоть до LFM2.5-8B-A1B включительно по всем шести объективным критериям, демонстрируя 0,4218 против 0,3757 при использовании лишь трети от объема параметров соперника.

Тем не менее, модель уступает крупнейшим системам. Решение Qwen3-8B превосходит ее по макро-гейту со счетом 0,5336 против 0,4218, хотя большая часть этого преимущества обеспечивается за счет нечетких совпадений, тогда как на строгом тесте strict-7 показатели составляют 0,2093 и 0,1971 соответственно. Модель gpt-oss-120b выигрывает по среднему значению шести направлений со счетом 0,5192 против 0,4488.

Главным бесспорным преимуществом TwIL-LM3 является вычислительная эффективность. Модель генерирует самые короткие ответы среди всех участников (в среднем 482 токена на треке B), обеспечивая скорость обработки 32,9 ответа в секунду по сравнению с 4,2 ответа у 120-миллиардной модели.

Оценка переноса знаний на отложенных наборах данных

При тестировании на отложенных данных TwIL-LM3 демонстрирует рост внутридоменных результатов на 26% относительно базовых значений (макро-гейт увеличивается с 0,336 до 0,422), одновременно прибавляя 0,022 на отложенном базовом наборе. В описании модели подчеркивается, что это единственное решение в проекте, показавшее улучшение на обоих треках. Оценка на LogicBench возрастает с 0,6467 до 0,7167, тогда как на GSM8K наблюдается незначительное снижение с 0,8833 до 0,8733, а на IFEval показатель уменьшается с 0,6767 до 0,6433.

Младшая модель с 1,7 миллиарда параметров демонстрирует иной баланс характеристик. Ее показатель макро-приоритета составляет 0,361 по сравнению с 0,185 у неадаптированной базы. Результаты вне обучающего распределения носят смешанный характер: показатели LogicBench BQA улучшаются с 0,563 до 0,590, в то время как точность на GSM8K падает с 0,413 до 0,380, а на ARC-C с цепочкой рассуждений снижается с 0,587 до 0,463.

Источник: marktechpost.com