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

Параметры: 365 млн
Лицензия: MIT
Архитектура: t5 · dense
Опубликована: 25 июн 2023

Ссылки

Hugging Face

leandojo-lean4-tacgen-byt5-small

kaiyuy

Языковая модель3 профессии

Модель ByT5-small из проекта LeanDojo генерирует тактики Lean 4 для автоматизированного доказательства теорем.

834скачиваний за 30 дней15лайковвеса обновлены16 июл 2024

Бенчмарки

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

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

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

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

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

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

kaiyuy/leandojo-lean4-tacgen-byt5-small — модель семейства T5, разработанная Kaiyu Yang и соавторами в рамках проекта LeanDojo. Это компактный вариант ByT5-small для генерации тактик доказательства теорем в Lean 4; в метаданных указано 364,6 млн параметров и формат safetensors. Работа LeanDojo посвящена языковым моделям с поиском контекста для автоматизированного доказательства теорем.

Модель предназначена для генерации тактических шагов Lean 4 в сценариях автоматического доказательства теорем. Карточка связывает её с исследовательской работой NeurIPS 2023, но не описывает отдельные ограничения или условия применения сверх лицензии MIT. Метаданные не содержат явного pipeline-тега, а README не раскрывает детали длины контекста и языковой поддержки.

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

генерация следующего тактического шага в доказательстве Lean 4
автоматизация доказательства математических теорем
эксперименты с языковыми моделями для формальной верификации

Ограничения

Карточка не приводит оценок качества или конкретных ограничений применения; модель специализирована на генерации тактик Lean 4 и не описана как универсальный чат-ассистент.

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

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

Все профессии

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

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

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

Открыть на Hugging Face

LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
NeurIPS (Datasets and Benchmarks Track), 2023
Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala,
Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, Anima Anandkumar

@inproceedings{yang2023leandojo,
    title={{LeanDojo}: Theorem Proving with Retrieval-Augmented Language Models},
    author={Yang, Kaiyu and Swope, Aidan and Gu, Alex and Chalamala, Rahul and Song, Peiyang and Yu, Shixing and Godil, Saad and Prenger, Ryan and Anandkumar, Anima},
    booktitle={Neural Information Processing Systems (NeurIPS)},
    year={2023}
}

Please visit LeanDojo Website for details.

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

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

GPU в ailist

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

Нельзя запустить

У модели не указана задача.

Класс архитектуры: T5ForConditionalGeneration
Ревизия весов: 67a2c53