/ Модель
Каталог

Характеристики

Контекст
32 768 токенов
Параметры
7,6 млрд
Размер весов
16,4 ГБ
Лицензия
Своя лицензия
Архитектура
qwen3 · dense
Базовая модель
Qwen3-8B-Base
Библиотека
transformers
Опубликована
3 сен 2026

Ссылки

Hugging Face

qwen3-sft-feedback-with-proof-repair-rl

formalmathatepfl
Генерация текстаТекст → текст3 профессии

Дообученная Qwen3 на 7,6 млрд параметров для генерации текста, ориентированная на формальные математические доказательства и их исправление.

867скачиваний за 30 дней0лайковвеса обновлены3 сен 2026

Бенчмарки

Как модель справилась с задачами пользователей ailist и что о ней публикуют открытые лидерборды

Тесты пользователейпока нет

Никто ещё не опубликовал тест этой модели. Соберите бенчмарк из своих задач — результат появится здесь.

  1. Добавьте модель в бенчмарк

    Вместе с другими моделями категории «Текст» — сравнение идёт внутри одной категории.

  2. Опишите свои задачи

    Напишите запросы, при необходимости приложите файлы и эталонные ответы.

  3. Запустите и опубликуйте

    Модели ответят на каждую задачу, судья оценит ответы. Опубликованный результат появится на этой странице.

Открыть конструктор бенчмарка

Публичные оценки

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

В подключённых источниках результатов для этой модели пока нет.

Что умеет модель

Описание составлено по карточке модели и метаданным Hugging Face

Это дообученная модель Qwen3 для генерации текста и диалогового взаимодействия, опубликованная пользователем formalmathatepfl. Она создана на основе Qwen/Qwen3-8B-Base и дополнительно обучена на наборе lean_selfdistill_r1_train; название и данные карточки указывают на настройку для работы с формальными математическими доказательствами и их исправлением.

Модель имеет плотную авторегрессионную архитектуру Qwen3ForCausalLM, содержит 7,6 млрд параметров и поддерживает контекст до 32 768 токенов. Репозиторий содержит веса в формате Safetensors. Карточка не приводит результаты оценки качества и конкретные инструкции по применению. Лицензия указана как other, поэтому условия использования следует сверить с лицензией репозитория и базовой модели.

Сценарии применения

  • генерация формальных математических доказательств
  • исправление ошибок в формальных доказательствах
  • диалоговая помощь при работе с Lean
  • продолжение текста в задачах формальной математики

Ограничения

В карточке нет описания оценки качества и подробных рекомендаций по применению. Лицензия обозначена как other, поэтому условия использования нужно уточнить в репозитории.

Для каких профессий подходит3

Разделы каталога профессий, в задачах которых используется эта модель

Все профессии
IV.6Отраслевые задачиНаучные исследования, математика и новые материалыAI помогает формировать гипотезы, анализировать научные данные и ускорять открытие новых материалов и методов.39 задач4 120моделейII.2Разработка и данныеСоздание и понимание программного кодаAI помогает писать, объяснять и связывать программный код с требованиями и существующей системой.20 задач21 443моделиIV.5Отраслевые задачиОбразование и развитие навыковAI помогает персонализировать обучение и снижать административную нагрузку на преподавателей.34 задачи6 641модель

Карточка модели

README от автора на Hugging Face, как он его опубликовал

Открыть на Hugging Face

qwen3-cpt-lean-sft-feedback-selfdistill-r1

This model is a fine-tuned version of formalmathatepfl/qwen3-sft-feedback-with-proof-repair on the lean_selfdistill_r1_train dataset.

Model description

More information needed

Intended uses & limitations

More information needed

Training and evaluation data

More information needed

Training procedure

Training hyperparameters

The following hyperparameters were used during training:

  • learning_rate: 2e-06
  • train_batch_size: 1
  • eval_batch_size: 8
  • seed: 42
  • distributed_type: multi-GPU
  • num_devices: 8
  • total_train_batch_size: 8
  • total_eval_batch_size: 64
  • optimizer: Use OptimizerNames.ADAMW_TORCH_FUSED with betas=(0.9,0.999) and epsilon=1e-08 and optimizer_args=No additional optimizer arguments
  • lr_scheduler_type: cosine
  • lr_scheduler_warmup_ratio: 0.03
  • num_epochs: 1.0

Training results

Framework versions

  • Transformers 4.57.3
  • Pytorch 2.9.0+cu129
  • Datasets 3.6.0
  • Tokenizers 0.22.1

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

На своей GPU в ailist. Цена — по текущим предложениям провайдеров

GPU в ailist

Универсальный рантайм · transformers

Можно запустить

Подбираем GPU…

Класс архитектуры
Qwen3ForCausalLM
Ревизия весов
26e919d

0 моделей

    Создать бенчмарк