Views
No views yet
1from transformers import AutoModelForCausalLM, AutoTokenizer
2
3instruct = """
4Translate the given requirement using TLA's syntax and semantics.
5You only need to return the TLA formal specification without explanation.
6"""
7
8input_text = """
9An operation `LM_Inner_Rsp(p)` that represents a response process for a given parameter `p`. It satisfies the following conditions:
10 - The control state `octl[p]` is equal to `\"done\"`.
11 - The `Reply(p, obuf[p], memInt, memInt')` operation is executed.
12 - The control state `octl` is updated by setting the `p` index of `octl` to `\"rdy\"`.
13 - The variables `omem` and `obuf` remain unchanged.
14"""
15
16model_name = "fm-universe/deepseek-coder-7b-instruct-v1.5-fma"
17
18model = AutoModelForCausalLM.from_pretrained(
19 model_name, torch_dtype="auto", device_map="auto"
20)
21tokenizer = AutoTokenizer.from_pretrained(model_name)
22
23messages = [{"role": "user", "content": f"{instruct}\n{input_text}"}]
24
25text = tokenizer.apply_chat_template(
26 messages, tokenize=False, add_generation_prompt=True
27)
28model_inputs = tokenizer([text], return_tensors="pt").to(model.device)
29
30generated_ids = model.generate(**model_inputs, max_new_tokens=4096)
31generated_ids = [
32 output_ids[len(input_ids) :]
33 for input_ids, output_ids in zip(model_inputs.input_ids, generated_ids)
34]
35
36response = tokenizer.batch_decode(generated_ids, skip_special_tokens=True)[0]
37print(response)1from vllm import LLM, SamplingParams
2
3instruct = """
4Translate the given requirement using TLA's syntax and semantics.
5You only need to return the TLA formal specification without explanation.
6"""
7
8input_text = """
9An operation `LM_Inner_Rsp(p)` that represents a response process for a given parameter `p`. It satisfies the following conditions:
10 - The control state `octl[p]` is equal to `\"done\"`.
11 - The `Reply(p, obuf[p], memInt, memInt')` operation is executed.
12 - The control state `octl` is updated by setting the `p` index of `octl` to `\"rdy\"`.
13 - The variables `omem` and `obuf` remain unchanged.
14"""
15
16model_name = "fm-universe/deepseek-coder-7b-instruct-v1.5-fma"
17
18# Pass the default decoding hyperparameters
19# max_tokens is for the maximum length for generation.
20greed_sampling = SamplingParams(temperature=0, max_tokens=4096)
21
22# load the model
23llm = LLM(
24 model=model_name,
25 tensor_parallel_size=1,
26 max_model_len=4096,
27 enable_chunked_prefill=True,
28 # quantization="fp8", # Enabling FP8 quantization for model weights can reduce memory usage.
29)
30
31# Prepare chat messages
32chat_message = [{"role": "user", "content": f"{instruct}\n{input_text}"}]
33
34# Inference
35responses = llm.chat(chat_message, greed_sampling, use_tqdm=True)
36
37print(responses[0].outputs[0].text)@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},
}