ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen_SFT-full
ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen_SFT-full is a 0.5 billion parameter instruction-tuned model based on Qwen2.5-Coder-0.5B-Instruct. It is specifically fine-tuned for Dafny formal verification tasks, focusing on automatically generating loop invariants for Dafny programs to ensure verification. This model excels at completing Dafny programs by adding necessary loop invariants, achieving a 51.02% pass@1 on 733 DafnyBench-cleaned tasks.
Loading preview...
Overview
This model, ThuraAung1601/Qwen2.5-Coder-0.5B-Instruct_reform-dafny-loop-inv-gen_SFT-full, is a specialized fine-tune of the Qwen2.5-Coder-0.5B-Instruct base model. It has been trained with full-parameter Supervised Fine-Tuning (SFT) on the ThuraAung1601/reform-dafny-loop-inv-gen dataset. Its primary function is to automatically generate and insert loop invariants into Dafny programs, enabling them to pass formal verification.
Key Capabilities
- Dafny Loop Invariant Generation: Automatically adds correct loop invariants to Dafny programs.
- Program Completion: Outputs the complete, verifiable Dafny program without requiring natural language chain-of-thought.
- Specialized for Formal Verification: Tailored specifically for the nuances of Dafny's verification system.
Performance
The model achieves a 51.02% pass@1 on 733 tasks from the DafnyBench-cleaned benchmark, demonstrating its effectiveness in solving Dafny verification challenges related to loop invariants.
Good for
- Developers working with Dafny who need assistance in generating loop invariants.
- Automating parts of the formal verification process for Dafny code.
- Research into AI-assisted formal methods and program synthesis for verification.