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

Лицензия: CC BY-NC 4.0
Базовая модель: Qwen2.5-Coder-0.5B-Instruct
Библиотека: transformers
Опубликована: 7 окт 2026

Ссылки

Hugging Face

Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen-aug-alldata_GRPO

ThuraAung1601

Генерация текстаТекст → текст

Модель дополняет программы на Dafny циклическими инвариантами, чтобы они проходили формальную проверку.

171скачиваний за 30 дней0лайковвеса обновлены11 окт 2026

Бенчмарки

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

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

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

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

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

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

Это дообученная модель Qwen2.5-Coder-0.5B-Instruct от Thura Aung для добавления циклических инвариантов в программы на Dafny. Она принимает программу в блоке кода и генерирует её полную версию с инвариантами, чтобы программа проходила проверку верификатором Dafny. Модель обучена на наборе ThuraAung1601/reform-dafny-loop-inv-gen-aug: сначала применялось LoRA SFT, затем LoRA GRPO с вознаграждением от верификатора Dafny и проверкой, что исходная программа и спецификация не изменены. Естественная языковая цепочка рассуждений не генерируется; на выходе — программа целиком.

Архитектура — плотная Qwen2 causal language model с 494 млн параметров и контекстом до 32 768 токенов. Модель поставляется в формате safetensors и поддерживает диалоговый режим через Transformers. README описывает объединённые базовые веса, SFT и GRPO; отдельный GRPO LoRA-адаптер находится в каталоге lora/ и применяется поверх объединённой SFT-модели. Лицензия — CC BY-NC 4.0, допускающая использование с указанием авторства и ограничивающая коммерческое применение.

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

генерация циклических инвариантов для программ на Dafny
подготовка Dafny-программ к прохождению верификатора
автоматическое дополнение полного исходного кода Dafny
проверка сохранения исходной программы и спецификации при добавлении инвариантов

Ограничения

Модель специализирована на добавлении циклических инвариантов в Dafny-программы и не предназначена для общего программирования. Для коммерческого использования лицензия CC BY-NC 4.0 накладывает ограничения.

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

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

Открыть на Hugging Face

Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen-aug-alldata_GRPO

Qwen/Qwen2.5-Coder-0.5B-Instruct fine-tuned to add loop invariants to Dafny programs so that they verify, on ThuraAung1601/reform-dafny-loop-inv-gen-aug: LoRA SFT followed by LoRA GRPO whose reward comes only from the Dafny verifier (Re:Form-style: syntax 0.2 / verified 1.0, with a faithfulness gate against editing the program or its spec). Trained without natural-language chain of thought: the output is the complete program.

from transformers import AutoModelForCausalLM, AutoTokenizer
model = AutoModelForCausalLM.from_pretrained("ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen-aug-alldata_GRPO")      # base + SFT + GRPO, merged
tokenizer = AutoTokenizer.from_pretrained("ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen-aug-alldata_GRPO")

The GRPO LoRA adapter alone is in lora/; it applies on top of the merged SFT model.

Prompt -- system message:

You are an expert in Dafny formal verification. You are given a Dafny program whose loops are missing their loop invariants. Output the complete program with loop invariants added so that it verifies with `dafny verify`. Do not change anything else in the program. Output only the program in a ```dafny code block.

user message: the program inside a ```dafny code block.

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

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

GPU в ailist

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

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

Доступ к модели ограничен автором; у платформы нет доступа к весам.

Ревизия весов: d358dfa