Instructions to use ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen-rlhint-alldata_GRPO with libraries, inference providers, notebooks, and local apps. Follow these links to get started.

Libraries

How to use ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen-rlhint-alldata_GRPO with Transformers:

# Use a pipeline as a high-level helper
from transformers import pipeline

pipe = pipeline("text-generation", model="ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen-rlhint-alldata_GRPO")
messages = [
    {"role": "user", "content": "Who are you?"},
]
pipe(messages)

# pip install -U transformers accelerate
# Load model directly
from transformers import AutoTokenizer, AutoModelForCausalLM

tokenizer = AutoTokenizer.from_pretrained("ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen-rlhint-alldata_GRPO")
model = AutoModelForCausalLM.from_pretrained("ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen-rlhint-alldata_GRPO", device_map="auto")
messages = [
    {"role": "user", "content": "Who are you?"},
]
inputs = tokenizer.apply_chat_template(
	messages,
	add_generation_prompt=True,
	tokenize=True,
	return_dict=True,
	return_tensors="pt",
).to(model.device)

outputs = model.generate(**inputs, max_new_tokens=256)
print(tokenizer.decode(outputs[0][inputs["input_ids"].shape[-1]:]))

Notebooks
Google Colab
Kaggle
Local Apps Settings

vLLM

How to use ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen-rlhint-alldata_GRPO with vLLM:

Install from pip and serve model

# Install vLLM from pip:
pip install vllm
# Start the vLLM server:
vllm serve "ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen-rlhint-alldata_GRPO"
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:8000/v1/chat/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen-rlhint-alldata_GRPO",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Use Docker

docker model run hf.co/ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen-rlhint-alldata_GRPO

SGLang

How to use ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen-rlhint-alldata_GRPO with SGLang:

Install from pip and serve model

# Install SGLang from pip:
pip install sglang
# Start the SGLang server:
python3 -m sglang.launch_server \
    --model-path "ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen-rlhint-alldata_GRPO" \
    --host 0.0.0.0 \
    --port 30000
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:30000/v1/chat/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen-rlhint-alldata_GRPO",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Use Docker images

docker run --gpus all \
    --shm-size 32g \
    -p 30000:30000 \
    -v ~/.cache/huggingface:/root/.cache/huggingface \
    --env "HF_TOKEN=<secret>" \
    --ipc=host \
    lmsysorg/sglang:latest \
    python3 -m sglang.launch_server \
        --model-path "ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen-rlhint-alldata_GRPO" \
        --host 0.0.0.0 \
        --port 30000
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:30000/v1/chat/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen-rlhint-alldata_GRPO",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Docker Model Runner
How to use ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen-rlhint-alldata_GRPO with Docker Model Runner:
```
docker model run hf.co/ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen-rlhint-alldata_GRPO
```

Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen-rlhint-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: LoRA SFT followed by LoRA GRPO on DafnyBench-style tasks (ThuraAung1601/reform-dafny-hint-gen: every invariant / assert / decreases line removed) 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-rlhint-alldata_GRPO")      # base + SFT + GRPO, merged
tokenizer = AutoTokenizer.from_pretrained("ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen-rlhint-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 loop invariants, assertions and decreases clauses have been removed. Output the complete program with the invariants, assertions and decreases clauses it needs 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.

Downloads last month: -

Safetensors

Model size

0.5B params

Tensor type

BF16

Model tree for ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen-rlhint-alldata_GRPO

Base model

Qwen/Qwen2.5-0.5B

Finetuned

Qwen/Qwen2.5-Coder-0.5B

Finetuned

Qwen/Qwen2.5-Coder-0.5B-Instruct

Adapter

(78)

this model

ThuraAung1601
/

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

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

Model tree for ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen-rlhint-alldata_GRPO

Datasets used to train ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen-rlhint-alldata_GRPO