|
--- |
|
license: mit |
|
language: |
|
- en |
|
base_model: |
|
- meta-llama/Llama-3.1-8B |
|
--- |
|
|
|
<p align="center"> |
|
<img width=20%" src="figures/logo.png"> |
|
</p> |
|
|
|
## Introduction |
|
|
|
We present a fine-tuned model based on llama-3.1-8B 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: |
|
|
|
The fm-alpaca (the fine-tuning dataset) will be released soon. |
|
|
|
- **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 |
|
|
|
<p align="center"> |
|
<img width=100%" src="figures/application.png"> |
|
</p> |
|
|
|
|
|
## Supported Formal Specification Languages |
|
|
|
<p align="center"> |
|
<img width=100%" src="figures/examples.png"> |
|
</p> |
|
|
|
## Data Preparation Pipeline |
|
<p align="center"> |
|
<img width=60%" src="figures/data-prepare.png"> |
|
</p> |
|
|
|
|
