license: mit
language:
- en
base_model:
- deepseek-ai/deepseek-coder-7b-instruct-v1.5
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},
}