Qwen2.5-Coder-1.5B-Instruct_reform-dafny-loop-inv-gen_GRPO

Qwen/Qwen2.5-Coder-1.5B-Instruct fine-tuned to add loop invariants to Dafny programs so that they verify, on ThuraAung1601/reform-dafny-loop-inv-gen: 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.

DafnyBench-cleaned (pass@1, 733 tasks): 51.16% solved (base model: 11.19%).

from transformers import AutoModelForCausalLM, AutoTokenizer
model = AutoModelForCausalLM.from_pretrained("ThuraAung1601/Qwen2.5-Coder-1.5B-Instruct_reform-dafny-loop-inv-gen_GRPO")      # base + SFT + GRPO, merged
tokenizer = AutoTokenizer.from_pretrained("ThuraAung1601/Qwen2.5-Coder-1.5B-Instruct_reform-dafny-loop-inv-gen_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.