Из открытых лидербордов. Сравнивайте результаты одного теста при одинаковых условиях — отсутствие оценки не значит, что модель хуже.
В подключённых источниках результатов для этой модели пока нет.
Что умеет модель
Описание составлено по карточке модели и метаданным Hugging Face
Gobble-Prover-1.7B — языковая модель, опубликованная анонимно для рецензирования. Она дообучена на базе AI-MO/Kimina-Prover-Distill-1.7B методом supervised fine-tuning с последующим GRPO и предназначена для генерации доказательств на Lean 4 по утверждениям с несколькими вариантами ответа. Модель построена на плотной архитектуре Qwen3, содержит 1,7 млрд параметров и принимает контекст длиной до 40 960 токенов.
Модель подходит для формализации и поиска доказательств в интерактивных сценариях математического доказательства. Сгенерированные доказательства необходимо проверять в Lean 4; сама генерация не гарантирует корректности. Репозиторий содержит веса в формате safetensors, конфигурацию модели и токенизатор. Указанная лицензия — Apache 2.0.
Сценарии применения
генерация доказательств Lean 4 по математическому утверждению
поиск доказательства среди нескольких вариантов ответа
подготовка кандидатов доказательств для проверки в Lean 4
Ограничения
Сгенерированные доказательства необходимо проверять в Lean 4; их корректность не гарантируется. Назначение модели ограничено задачей генерации доказательств Lean 4.
Для каких профессий подходит3
Разделы каталога профессий, в задачах которых используется эта модель
Gobble-Prover-1.7B is fine-tuned from
AI-MO/Kimina-Prover-Distill-1.7B
using supervised fine-tuning followed by GRPO. It generates Lean 4 proofs
for statements with multiple candidate answers.
This repository contains the model weights, model configuration, and tokenizer.
Generated proofs must be checked with Lean.
The base model was developed by Project Numina and Kimi teams and is
released under the Apache 2.0 license. See the linked base model card
for upstream information.
Как запустить
На своей GPU в ailist. Цена — по текущим предложениям провайдеров