Instructions to use ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-multitask6-rl-pa-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-multitask6-rl-pa-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-multitask6-rl-pa-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-multitask6-rl-pa-alldata_GRPO")
model = AutoModelForCausalLM.from_pretrained("ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-multitask6-rl-pa-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-multitask6-rl-pa-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-multitask6-rl-pa-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-multitask6-rl-pa-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-multitask6-rl-pa-alldata_GRPO

SGLang

How to use ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-multitask6-rl-pa-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-multitask6-rl-pa-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-multitask6-rl-pa-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-multitask6-rl-pa-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-multitask6-rl-pa-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-multitask6-rl-pa-alldata_GRPO with Docker Model Runner:
```
docker model run hf.co/ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-multitask6-rl-pa-alldata_GRPO
```

You need to agree to share your Hugging Face information to access this model

This repository is publicly accessible, but you have to accept the conditions to access its files and content.

Qwen2.5-Coder-0.5B-Instruct_reform-dafny-multitask6-rl-pa-alldata_GRPO

Qwen/Qwen2.5-Coder-0.5B-Instruct fine-tuned for Dafny verification tasks, multi-task (ThuraAung1601/reform-dafny-multitask: loop-invariants, proof-annotations, single-hint, termination, proof-repair, spec-generation), each with its own system prompt: LoRA SFT (ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-multitask6-alldata_SFT) followed by LoRA GRPO on proof-annotations only, 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; spec-generation also needs specs at least as strong as the ground truth's, weaker ones get 0.4). 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-multitask6-rl-pa-alldata_GRPO")      # base + SFT + GRPO, merged
tokenizer = AutoTokenizer.from_pretrained("ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-multitask6-rl-pa-alldata_GRPO")

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

System prompts (use proof-annotations for DafnyBench-style tasks):

loop-invariants

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.

proof-annotations

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.

single-hint

You are an expert in Dafny formal verification. You are given a Dafny program from which exactly one proof annotation (a loop invariant, an assertion or a decreases clause) has been removed, so it no longer verifies. Output the complete program with the missing annotation restored so that it verifies with `dafny verify`. Do not change anything else in the program. Output only the program in a ```dafny code block.

termination

You are an expert in Dafny formal verification. You are given a Dafny program whose decreases clauses have been removed, so Dafny cannot prove that all of its loops and recursive calls terminate. Output the complete program with the decreases clauses it needs added so that it verifies with `dafny verify`. Do not use `decreases *` and do not change anything else in the program. Output only the program in a ```dafny code block.

proof-repair

You are an expert in Dafny formal verification. You are given a Dafny program that fails verification because one of its proof annotations (a loop invariant, an assertion or a decreases clause) is wrong or missing, together with the Dafny verifier's error output. Output the complete corrected program so that it verifies with `dafny verify`. Only change loop invariants, assertions and decreases clauses; do not change the code or its requires/ensures specification. Output only the program in a ```dafny code block.

spec-generation

You are an expert in Dafny formal verification. You are given a Dafny program whose methods are missing their requires and ensures clauses. Output the complete program with requires and ensures clauses added to every method: the weakest preconditions under which the code is correct and the strongest postconditions it guarantees, so that the program 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; for proof-repair followed by "Dafny verifier output:" and the error output in a text 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-multitask6-rl-pa-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

(87)

this model

ThuraAung1601
/

Qwen2.5-Coder-0.5B-Instruct_reform-dafny-multitask6-rl-pa-alldata_GRPO

You need to agree to share your Hugging Face information to access this model

Qwen2.5-Coder-0.5B-Instruct_reform-dafny-multitask6-rl-pa-alldata_GRPO

Model tree for ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-multitask6-rl-pa-alldata_GRPO

Dataset used to train ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-multitask6-rl-pa-alldata_GRPO