Дообученная CodeLlama для предсказания тактических шагов формальных доказательств в Lean.
Как модель справилась с задачами пользователей ailist и что о ней публикуют открытые лидерборды
Никто ещё не опубликовал тест этой модели. Соберите бенчмарк из своих задач — результат появится здесь.
Вместе с другими моделями категории «Текст» — сравнение идёт внутри одной категории.
Напишите запросы, при необходимости приложите файлы и эталонные ответы.
Модели ответят на каждую задачу, судья оценит ответы. Опубликованный результат появится на этой странице.
Из открытых лидербордов. Сравнивайте результаты одного теста при одинаковых условиях — отсутствие оценки не значит, что модель хуже.
В подключённых источниках результатов для этой модели пока нет.
Описание составлено по карточке модели и метаданным Hugging Face
HaimingW/Leandojo-CodeLLama-7b — языковая модель на архитектуре Llama, дообученная на бенчмарке LeanDojo для генерации тактических шагов доказательства в Lean. Она принимает состояние цели в формате GOAL $(tactic state) PROOFSTEP и генерирует следующий тактический шаг. Модель содержит 6,6 млрд параметров и поддерживает контекст до 16 384 токенов.
Модель предназначена для предсказания шагов формальных доказательств Lean и автоматизации доказательства теорем. В README заявлена точность pass@1 около 57,7% на случайном разбиении LeanDojo; это результат бенчмарка, а не гарантия успешного доказательства для произвольной цели. Модель распространяется в формате safetensors; сведения о лицензии в предоставленных данных отсутствуют.
Качество зависит от формулировки цели и контекста; заявленная точность около 57,7% pass@1 относится к случайному разбиению бенчмарка LeanDojo. Условия лицензии не приведены в доступных данных.
Разделы каталога профессий, в задачах которых используется эта модель
README от автора на Hugging Face, как он его опубликовал
This is a CodeLlama-7b model fine-tuned on LeanDojo Benchmark
The performance is comparable with the paper Temperature-scaled large language models for Lean proofstep prediction with around 57.7 pass@1 accuracy on LeanDojo "random" benchmark.
The training lines are formatted as follow:
GOAL $(tactic state) PROOFSTEP $(tactic)
For inference, use the following line:
GOAL $(tactic state) PROOFSTEP
На своей GPU в ailist. Цена — по текущим предложениям провайдеров
GPU в ailist
Универсальный рантайм
Подбираем GPU…