README.md

---
base_model:
- deepseek-ai/deepseek-coder-7b-instruct-v1.5
language:
- en
license: mit
pipeline_tag: text-generation
library_name: transformers
---

<p align="center">
  <img width=20%" src="figures/logo.png">
</p>

## Introduction

This model, presented in the paper [From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs](https://hf.co/papers/2501.16207), is a fine-tuned LLM for formal verification tasks.  Trained on 18k high-quality instruction-response pairs across five formal specification languages (Coq, Dafny, Lean4, ACSL, and TLA+), it excels at various sub-tasks including requirement analysis, proof/model generation, and code-to-proof translation (for ACSL).  Interestingly, fine-tuning on this formal data also enhances the model's mathematics, reasoning, and coding capabilities.


## 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>

## Quickstart
Here provides a code snippet with apply_chat_template to show you how to load the tokenizer and model and how to inference fmbench.

``` python
from transformers import AutoModelForCausalLM, AutoTokenizer

instruct = """
Translate the given requirement using TLA's syntax and semantics.
You only need to return the TLA formal specification without explanation.
"""

input_text = """
An operation `LM_Inner_Rsp(p)` that represents a response process for a given parameter `p`. It satisfies the following conditions:
  - The control state `octl[p]` is equal to `"done"`.
  - The `Reply(p, obuf[p], memInt, memInt')` operation is executed.
  - The control state `octl` is updated by setting the `p` index of `octl` to `"rdy"`.
  - The variables `omem` and `obuf` remain unchanged.
"""

model_name = "fm-universe/deepseek-coder-7b-instruct-v1.5-fma"

model = AutoModelForCausalLM.from_pretrained(
    model_name, torch_dtype="auto", device_map="auto"
)
tokenizer = AutoTokenizer.from_pretrained(model_name)

messages = [{"role": "user", "content": f"{instruct}
{input_text}"}]

text = tokenizer.apply_chat_template(
    messages, tokenize=False, add_generation_prompt=True
)
model_inputs = tokenizer([text], return_tensors="pt").to(model.device)

generated_ids = model.generate(**model_inputs, max_new_tokens=4096)
generated_ids = [
    output_ids[len(input_ids) :]
    for input_ids, output_ids in zip(model_inputs.input_ids, generated_ids)
]

response = tokenizer.batch_decode(generated_ids, skip_special_tokens=True)[0]
print(response)
```

## Example of Offline Inference

vLLM supports offline inference.

``` python
from vllm import LLM, SamplingParams

instruct = """
Translate the given requirement using TLA's syntax and semantics.
You only need to return the TLA formal specification without explanation.
"""

input_text = """
An operation `LM_Inner_Rsp(p)` that represents a response process for a given parameter `p`. It satisfies the following conditions:
  - The control state `octl[p]` is equal to `"done"`.
  - The `Reply(p, obuf[p], memInt, memInt')` operation is executed.
  - The control state `octl` is updated by setting the `p` index of `octl` to `"rdy"`.
  - The variables `omem` and `obuf` remain unchanged.
"""

model_name = "fm-universe/deepseek-coder-7b-instruct-v1.5-fma"

# Pass the default decoding hyperparameters
# max_tokens is for the maximum length for generation.
greed_sampling = SamplingParams(temperature=0, max_tokens=4096)

# load the model
llm = LLM(
    model=model_name,
    tensor_parallel_size=1,
    max_model_len=4096,
    enable_chunked_prefill=True,
    # quantization="fp8", # Enabling FP8 quantization for model weights can reduce memory usage.
)

# Prepare chat messages
chat_message = [{"role": "user", "content": f"{instruct}
{input_text}"}]

# Inference
responses = llm.chat(chat_message, greed_sampling, use_tqdm=True)

print(responses[0].outputs[0].text)
```

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