fm-universe/qwen2.5-coder-7b-instruct-fma

Introduction

We present a fine-tuned model for formal verification tasks. It is fine-tuned in five formal specification languages (Cog, Dafny, Lean4, ACSL, and TLA) on six formal-verification-related tasks:

• Requirement Analysis: given requirements and description of the verification or modeling goals, decomposing the goal into detailed verification steps

• Proof/Model Generation: given requirements and description of the verification or modeling goals, writing formal proofs or models that can be verified by verifier/model checker.

• Proof segment generation

• Proof Completion: complete the given incomplete proofs or models

• Proof Infilling: filling in the middle of the given incomplete proofs or models

• Code 2 Proof: (Currently only support for ACSL whose specification is in form of code annotations) given the code under verification, generate the proof with the specifications

Application Scenario

Supported Formal Specification Languages

Data Preparation Pipeline

Citation

@misc{fmbench25jialun,
      title={From Informal to Formal--Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs}, 
      author={Jialun Cao, Yaojie Lu, Meiziniu Li, Haoyang Ma, Haokun Li, Mengda He, Cheng Wen, Le Sun, Hongyu Zhang, Shengchao Qin, Shing-Chi Cheung, Cong Tian},
      year={2025},
      eprint={2501.16207},
      archivePrefix={arXiv},
      primaryClass={cs.AI},
      url={https://arxiv.org/abs/2501.16207}, 
}