Что такое MathForm-8B? Тихий релиз автоформализации OpenBMB превращает математику в Lean 4.

openbmb/MathForm-8B — это новая модель автоформализации от OpenBMB, которая переводит математические утверждения, сформулированные на естественном языке, в Lean 4. Она вышла практически без анонса: веса, датасет и статья появились на Hugging Face и arXiv в один и тот же день, 2026-08-14, под общим заголовком «MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement». За этим тихим запуском скрывается необычный результат — модель с 8B параметров сообщает о средних показателях Pass@8 88,06% при синтаксической проверке и 72,37% при более строгой проверке согласованности на шести бенчмарках, и, по утверждению статьи, она превосходит несколько специализированных автоформализаторов с 32B параметров. Это материал о том, что известно на данный момент: всё, что ниже помечено как «из репозитория», взято напрямую из карточки модели, карточки датасета и статьи, а всё, что ещё не было подтверждено независимо, помечено соответствующим образом.

Основные выводы

• MathForm-8B — это модель автоформализации на 8B параметров с лицензией Apache-2.0: она читает неформальную математическую задачу и записывает утверждение теоремы на Lean 4 с именованным заголовком, готовое к последующему доказательству.

• Она дообучена на основе Qwen3-8B на FormalVerse — проверенном наборе данных Lean 4 из ~367 000 примеров, созданном OpenBMB с помощью извлечения знаний и проверяемого компилятором уточнения, — а затем обучена с подкреплением с использованием компиляции Lean и обратной связи по семантической согласованности.

• Заявленные вендором показатели (не воспроизведены): средний Pass@8 — 88,06% при проверке синтаксиса, 72,37% при проверке согласованности, что превосходит специализированные автоформализаторы от 7B до 32B в таблице самой статьи.

• Это не анонсировано, не доступно в крупном платном API на запуске и ещё не прошло независимое бенчмаркирование — три пробела, которые важны для производственного внедрения.

• Сервинг развертывается самостоятельно: Transformers, vLLM или SGLang — все предоставляют OpenAI-совместимый endpoint.

Что на самом деле содержит релиз

Три артефакта появились в течение нескольких минут друг за другом 2026-08-14, что выглядит как скоординированный, но неанонсированный релиз:

• Репозиторий модели openbmb/MathForm-8B — 8B каузальная языковая модель в BF16 с чат-шаблоном, четырьмя шардами safetensors, лицензия Apache 2.0.

Репозиторий набора данных, openbmb/FormalVerse — набор данных для автоформализации на Lean 4, содержащий примерно 367 000 проверенных примеров, также под лицензией Apache 2.0.

• Статья arXiv 2608.14221 — 25 страниц, описывающих конвейер построения данных, рецепт обучения и оценку на шести бенчмарках.

Ссылка на код на GitHub в README на момент написания всё ещё является заглушкой, поэтому конвейер оценки и скрипты Pass@k обещаны, но ещё не опубликованы. В README говорится, что проверки компиляции требуют запущенного Kimina Lean Server и что в экспериментах используется Lean 4.21.0.

Страница репозитория выше — это вся публичная часть релиза на данный момент: карточка модели, четыре шарда safetensors, шаблон чата и README, который одновременно является единственной документацией. На момент написания этого текста анонсирующего поста в блоге не существует.

Что делает MathForm-8B — и почему это узкая задача

Автоформализация — это шаг перед доказательством теорем: получив математическую задачу на простом английском («Докажите, что для любого вещественного числа x, x² неотрицательно»), модель должна создать формально корректное утверждение на Lean 4 — импорты, типы и заголовок теоремы — которое затем может атаковать человек или программа доказательства. Это совершенно другой навык, чем занятие математикой, потому что модель должна сопоставлять понятия естественного языка с точной иерархией определений и типов в Mathlib. Утверждение, которое проходит проверку типов, но незаметно ослабляет исходное («(2^5) ∣ (13^4 − 11^4)» вместо полного утверждения о делимости), — это классический режим отказа, и именно поэтому в статье различают проверку синтаксиса (компилируется ли оно) и проверку согласованности (является ли оно семантически тем же утверждением).

Карточка модели показывает предполагаемый способ использования: вы передаёте ей промпт с неформальной постановкой задачи и желаемым именем теоремы, и она возвращает утверждение на Lean 4 с code>theorem my_favorite_theorem : ... := by sorry/code> — code>sorry/code> оставляет доказательственное обязательство открытым. Такое разделение труда важно: MathForm-8B — формализатор, а не доказыватель. Команды, создающие инструменты для Lean, используют его для преобразования банков задач в форму, проверяемую машиной.

Как оно было обучено

Методика из статьи состоит из двух этапов. Сначала OpenBMB создал FormalVerse с помощью конвейера, который (1) извлекает релевантные определения и существующие формализации из Mathlib перед генерацией, (2) генерирует кандидатные утверждения, (3) уточняет их на основе диагностики компилятора Lean и обратной связи по семантической согласованности и (4) сохраняет только образцы, прошедшие обе проверки. Этот проверенный корпус затем используется для контролируемой тонкой настройки, после чего применяется обучение с подкреплением с сигналами вознаграждения от компиляции Lean и семантической согласованности.

Карточка набора данных даёт конкретное представление о данных: каждая запись сопоставляет неформальное утверждение с проверенным формальным и помечена источником (например, AceReason-Math) и тематической меткой (теория чисел и т. д.). Поскольку каждый пример прошёл реальную проверку компилятором до попадания в обучающую выборку, модель учится на заведомо корректных утверждениях, а не на сыром выводе модели.

Таблица бенчмарков, честно промаркированная

Все числа в этом разделе заявлены поставщиком в статье (arXiv 2608.14221) и не были независимо воспроизведены. Pass@8 означает, что модель получает восемь попыток на каждую задачу, и результат засчитывается, если хотя бы одна из них успешна; это более щадящая метрика, чем pass@1, и её следует понимать как «как часто модель может выдать корректное утверждение при заданном бюджете».

• MathForm-8B средние показатели — Проверка синтаксиса 88.06%, Проверка согласованности 72.37%.

По бенчмаркам, SC, затем CC: FormalIMATH 100.00 / 95.06, ProverBench 100.00 / 94.83, CombiBench 93.00 / 47.00, FATE-M 99.33 / 97.33, FATE-H 82.00 / 63.00, FATE-X 54.00 / 37.00.

Тяжелые наборы — честные: FATE-H CC 63% и FATE-X CC 37% показывают потолок модели на самых сложных подмножествах, тогда как на более легких FormalIMATH и ProverBench CC превышает 95%.

• Лучшие базовые модели 8B, перечисленные в статье, — ReForm-8B 81.76 / 66.21, Goedel-Formalizer-V2-8B 78.24 / 60.08 — и лучшие базовые модели 32B — ReForm-32B 81.61 / 68.41, Goedel-Formalizer-V2-32B 78.28 / 63.74, StepFun-Formalizer-32B 63.65 / 44.47 — все уступают MathForm-8B с показателями 88.06 / 72.37.

• Контрольная точка только с SFT (до этапа RL) показывает 84.38 / 66.53, так что проход с обучением с подкреплением даёт в среднем примерно +3.7 SC и +5.8 CC, причём наибольший прирост наблюдается на сложных наборах.

Наиболее сильные утверждения, которым стоит не доверять: показатели SC 100.00 на FormalIMATH и ProverBench (100% компиляции на простых наборах — это красный флаг, указывающий на то, что эти наборы сошлись), а также сравнение с 32B-моделями, которые не перезапускались в идентичных условиях. Числа проверки согласованности на FATE-H и FATE-X — это показатели, которые с наибольшей вероятностью переживут независимое тестирование.

Что не подтверждено

• Независимой оценки не существует. На момент написания ни одна третья сторона не прогоняла MathForm-8B через публичный тестовый стенд, а код для оценки так и не был выпущен.

• Никакого анонса о предоставлении сервиса. OpenBMB не опубликовал ни блога о запуске, ни страницы с ценами, ни API-эндпоинта. Формулировка «тихо выпущено» буквальна.

• Веса вознаграждений RL, бюджет обучения и аппаратное обеспечение не указаны в карточке модели; они есть только в статье.

• Не проверялось, распространяется ли модель 8B на Lean 4.21.1+ или на импорты, не относящиеся к Mathlib.

Как это запустить

На сегодняшний день самостоятельный хостинг — единственный путь. В README описаны три пути, все с OpenAI-совместимым чат-эндпоинтом по адресу code>localhost:8000/v1/chat/completions/code>:

• Transformers — code>AutoModelForCausalLM.from_pretrained("openbmb/MathForm-8B", torch_dtype=torch.bfloat16)/code>, затем генерируйте с помощью чат-шаблона.

• vLLM — code>vllm serve openbmb/MathForm-8B --served-model-name MathForm-8B --dtype bfloat16 --max-model-len 16384/code>.

• SGLang — code>python -m sglang.launch_server --model-path openbmb/MathForm-8B --served-model-name MathForm-8B --dtype bfloat16 --context-length 16384/code>.

В README рекомендуется температура 0.6, top_p 0.95 и до 16384 новых токенов — формальные утверждения получаются длинными, так что щедрое окно генерации — это фактическое системное требование, которое следует учесть.

Почему часть «8B превосходит 32B» важна

Если цифры подтвердятся, MathForm-8B — самый веский аргумент на данный момент в пользу того, что узкое место автоформализации — это качество данных и верификация, а не количество параметров. Собственная таблица в статье показывает, что специализированные модели на 32B (ReForm-32B, Goedel-Formalizer-V2-32B, StepFun-Formalizer-32B) уступают модели на 8B, обученной на корпусе, проверенном компилятором. Для команд, которые сейчас используют формализатор на 32B, это существенное изменение стоимости: модель на 8B в BF16 помещается на одном GPU, чего большинство моделей на 32B не могут, и она работает быстрее на токен.

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

Что посмотреть дальше

Три вещи превратили бы этот «интересный репозиторий» в «заслуживающий доверия инструмент»: фактическое появление кода оценки на GitHub; первый независимый прогон FATE-H и FATE-X с pass@1 вместо pass@8; и любое объявление OpenBMB о добавлении хостируемого маршрута или статьи v2 с результатами абляции. Пока не появится хотя бы одно из этих событий, относитесь к анонсируемым показателям как к ориентировочным — главное — архитектура и идея обучающих данных, а не точный процент.