Ember-1 против MathForm-8B: две модели, созданные путём сужения заимствованной базы.

Ember-1 и MathForm-8B разделяют стратегию, которую ни одна из лабораторий не афиширует как таковую: обе представляют собой сужения модели, обученной кем-то другим. Ember-1 — специализированная производная Kimi K3 от Moonshot AI, опубликованная 23 сентября 2026 года и переобученная так, что достигает точности K3 примерно на 40% меньшем количестве токенов. MathForm-8B — это 8B-модель автоформализации от OpenBMB, тихо выпущенная 14 августа 2026 года как Apache-2.0-файнтюн Qwen3-8B от Alibaba, которая превращает неформальную математику в формулировки теорем Lean 4, проверяемые компилятором. Одно сужение устранило бесполезные размышления и сохранило общие способности нетронутыми. Другое устранило почти все общие способности и взамен приобрело проверяемость. Сопоставление их вместе — самый чистый способ увидеть, во что на самом деле обходится специализация, потому что эти две модели потратили свои бюджеты на обучение на противоположных сторонах этого баланса.

Два вида сужения

Вмешательство Fireworks Research носит поведенческий характер. Ember-1 сохраняет архитектуру Kimi K3 и её широту — математика, программирование, следование инструкциям, беседа, поиск, использование инструментов и разработка программного обеспечения — все присутствуют в обучающей смеси — и меняет только то, как долго модель размышляет перед ответом. Сообщается, что длина рассуждений сократилась на 35–50% без потери точности на семи бенчмарках и двух клиентских производственных A/B-тестах, при этом одна производственная задача по программированию сократила вывод с 49,3K до 29,9K токенов, а её оценка осталась на уровне 0,753 против 0,751. Каждая цифра заявлена производителем и не воспроизведена.

Вмешательство OpenBMB носит договорный характер. MathForm-8B берёт Qwen3-8B и направляет весь бюджет обучения на одну форму вывода: утверждение на Lean 4 с заголовком imports и именованной теоремой. Конвейер представляет собой дообучение с учителем на FormalVerse — корпусе примерно из 367 000 проверенных примеров Lean 4, который OpenBMB создала и выпустила вместе с моделью, — после чего следует обучение с подкреплением, где в качестве сигнала вознаграждения используются компиляция Lean и обратная связь о семантической согласованности. Модель не решает доказательства. Она пишет утверждение, которое завершит доказывающий, а сама статья описывает оценку на шести бенчмарках как суть упражнения.

От чего отказался каждый из них

Ember-1 на бумаге уступила очень мало — в этом и заключается всё заявление. В её опубликованной таблице показана победа на Terminal Bench 2.1 с 82,0% против 80,9% у Kimi K3 Max и на DeepSWE 1.1 с 75,2% против 66,4%, а также минимальные проигрыши на SWE-bench Verified — 92,2% против 93,2% — и на SWE-Interact — 20,0% против 21,3%. Это цифры вендора на выбранных вендором наборах, но картина остаётся неизменной: модель не столько утратила способности, сколько перенаправила то, куда она вкладывает усилия. Однако экономия токенов варьируется от 51,9% на Terminal Bench до 5,9% на τ-2 Bench Airline, так что «около 40%» — это среднее по очень широкому разбросу.

MathForm-8B растеряла большую часть того, чем известна Qwen3-8B. Она не ведёт общий диалог, не охватывает 119 языков и диалектов, на которых обучалась Qwen3-8B, и не принимает изображения или аудио. Её бюджет генерации рассчитан на вывод Lean, а не на продолжительные смешанные рассуждения. Сохранила она разрешительную лицензию и компактность: четыре шарда safetensors в BF16, работающие под Transformers, vLLM или SGLang через OpenAI-совместимый эндпоинт, с путём компиляции, который предполагает Kimina Lean Server на Lean 4.21.0.

Цифры измеряют разные вещи, и весь смысл именно в разрыве.

Ключевой показатель Ember-1 — это процент задач, правильно выполненных агентом, — Terminal Bench 2.1, 89 образцов, 82,0%. Ключевые показатели MathForm-8B — это средние оценки Pass@8 по шести бенчмаркам автоформализации: 88,06% при проверке синтаксиса и 72,37% при более строгой проверке согласованности. Они находятся не на одной оси. Один измеряет, выполнил ли агент работу в терминале; другой измеряет, разбирается ли сгенерированное утверждение теоремы и означает ли оно то же самое, что и неформальная задача, из которой оно получено.

Разброс 88,06 против 72,37 внутри собственных результатов MathForm — это более поучительное число. Разрыв между «это компилируется» и «это компилируется и говорит то, что я имел в виду» составляет примерно шестнадцать пунктов, и именно этот режим отказа делает автоформализацию трудной: утверждение, которое проходит проверку типов, но при этом незаметно ослабляет исходное утверждение, хуже очевидной ошибки, потому что ничто на последующих этапах этого не выявляет. На самых сложных наборах проверка согласованности падает до 63% на FATE-H и 37% на FATE-X, тогда как лёгкие наборы вроде FormalIMATH держатся на уровне 95,06%, а ProverBench — 94,83%. Это честный взгляд специалиста на то, где специалист слаб, и это полезнее, чем одно среднее значение.

Контраст, измерение за измерением

• Базовая модель — Ember-1: Kimi K3. MathForm-8B: Qwen3-8B.

• Что изменило обучение — Ember-1: как долго модель рассуждает, при неизменных возможностях. MathForm-8B: что модель выдаёт, в значительной мере пожертвовав обобщающей способностью.

• Параметры — Ember-1: не раскрыты. MathForm-8B: ~8B, плотная, BF16.

• Контракт вывода — Ember-1: обычный текст и вызовы инструментов, качество уровня K3. MathForm-8B: утверждение на Lean 4 с заголовком и именованной теоремой.

• Лицензия и веса — Ember-1: не опубликованы; исследовательский предпросмотр через собственную платформу поставщика. MathForm-8B: Apache 2.0, и веса, и набор данных доступны для скачивания.

• Заявленный главный результат — Ember-1: 82,0 % на Terminal Bench 2.1 при на 51,9 % меньшем количестве токенов. MathForm-8B: 88,06 % среднего Pass@8 при проверке синтаксиса, 72,37 % при проверке согласованности.

• Независимая проверка — ни для одного; оба заявлены вендором и не воспроизведены.

Строка о лицензии решает больше, чем результаты тестов

При всей разнице в цифрах практическое различие между этими двумя релизами — в способе распространения. MathForm-8B — это файл. OpenBMB опубликовала веса, датасет FormalVerse и статью в один и тот же день, под лицензией Apache 2.0, без анонса и без хостингового API — карточка модели и есть запуск. Вы можете скачать её сегодня днём и запустить на одной GPU, и никто уже не сможет этого отнять. Ember-1 — это сервис. Весов нет, цена не опубликована, а окно доступа описано как двухнедельный бессерверный период, продолжение которого зависит от спроса. Сегодня вы можете обратиться к ней, а в ноябре уже не можете быть уверены, что сможете.

Это различие также определяет, для чего можно использовать каждую модель. Компонент формализации должен находиться внутри контролируемого вами пайплайна, привязанного к версии, с инструментарием Lean на той же машине — именно поэтому чекпоинт Apache-2.0 без ограничений доступа — подходящая форма для задачи MathForm-8B, и поэтому отсутствие ссылки на код GitHub в его README (на момент написания всё ещё заглушка) — более досадный пробел, чем любое число из бенчмарков. Модель, для которой критична стоимость рассуждений, должна находиться за API, где оптимизируется именно счёт за токены и где поставщики конкурируют по цене и задержке. Форма Ember-1 тоже подходит для своей задачи; это просто означает, что зависимость здесь коммерческая, а не техническая.

Там, где конвейер использовал бы оба

Эти две модели дополняют друг друга, а не конкурируют, и композицию легко описать: специалист по формализации преобразует задачу в проверяемое утверждение, а reasoning-модель работает с этим утверждением или с окружающей инженерией. Ни одной из них нет на OrcaRouter — MathForm-8B доступна только при самостоятельном размещении, а Ember-1 находится в собственном превью вендора — но сама эта композиция и есть тот паттерн, для которого существует наш DSL маршрутизации. Объединение нескольких моделей в один вызов — именно так конвейер получает и специалиста, и универсала, не поддерживая два пути интеграции и два контракта, а слияние моделей идёт на шаг дальше, позволяя панели моделей отвечать сообща, когда отказ одной-единственной модели обходится слишком дорого.

Для стека формализации в частности аргумент в пользу композиции сильнее, чем обычно. Видимый режим отказа — это утверждение, которое компилируется и означает немного другое, а самая дешёвая защита от тихой ошибки — вторая модель, читающая ту же задачу, — и это решение о маршрутизации, а не об обучении.

Какая покупка выгоднее?

Если вам нужна машинно-проверяемая математика, MathForm-8B — единственная из двух, которая её вообще выдаёт, а его главная цена — это универсальность, которую для этой задачи вы всё равно не собирались использовать. Скачайте его, предусмотрите бюджет на сервер Lean и постройте собственную систему оценки — статья OpenBMB не расскажет вам, как он показывает себя на вашем распределении.

Если вам нужна универсальная модель рассуждений с меньшими затратами на токены, Ember-1 предназначена для вас, и правильный следующий шаг — прогнать теневой трафик через то, что вы используете сегодня, а не сравнивать бенчмарки. Её риск — доступность, а не возможности, и этот риск можно хеджировать, сохранив слой маршрутизации между вашим приложением и моделью.

Неудобный вывод для тех, кто надеется, что один из них решит вопрос, состоит в том, что ни один из них не был независимо оценён. MathForm-8B находится в открытом доступе уже шесть недель, и ни одна третья сторона не опубликовала воспроизведение; Ember-1 находится в открытом доступе всего день. Оба предлагают вам выступить в роли оценщика — это обычное условие выбора специализированной модели в 2026 году.

Что они действительно доказывают, так это то, что стратегия сужения работает в обоих направлениях. Передовую модель можно сделать дешевле, не сделав её хуже, а небольшую базовую модель можно сделать строгой, направив её обучение на компилятор. Интересен не вопрос о том, какой из этих двух подходов победит, а вопрос о том, как долго каждый из них ещё будет необходим после того, как применяемые в них методы станут обычной практикой.