Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen_SFT

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: LoRA SFT. Trained without natural-language chain of thought: the output is the complete program.

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

from peft import AutoPeftModelForCausalLM
model = AutoPeftModelForCausalLM.from_pretrained("ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen_SFT")

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.