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

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

## Supported Formal Specification Languages

## Data Preparation Pipeline

## 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}, } ```