Improve model card with pipeline tag, library name, and links

README.md

@@ -1,14 +1,16 @@
 ---
-license: mit
-language:
-- en
 base_model:
 - Qwen/Qwen2.5-Coder-7B-Instruct
+language:
+- en
+license: mit
+pipeline_tag: text-generation
+library_name: transformers
 ---
 
 ## 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:
+This model is a fine-tuned version of Qwen/Qwen2.5-Coder-7B-Instruct for formal verification tasks, as presented in [From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs](https://hf.co/papers/2501.16207). It's fine-tuned in five formal specification languages (Coq, 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
 
@@ -66,7 +68,8 @@ model = AutoModelForCausalLM.from_pretrained(
 )
 tokenizer = AutoTokenizer.from_pretrained(model_name)
 
-messages = [{"role": "user", "content": f"{instruct}\n{input_text}"}]
+messages = [{"role": "user", "content": f"{instruct}
+{input_text}"}]
 
 text = tokenizer.apply_chat_template(
     messages, tokenize=False, add_generation_prompt=True
@@ -119,7 +122,8 @@ llm = LLM(
 )
 
 # Prepare chat messages
-chat_message = [{"role": "user", "content": f"{instruct}\n{input_text}"}]
+chat_message = [{"role": "user", "content": f"{instruct}
+{input_text}"}]
 
 # Inference
 responses = llm.chat(chat_message, greed_sampling, use_tqdm=True)
@@ -140,3 +144,7 @@ print(responses[0].outputs[0].text)
 }
 
 ```
+
+Code: [https://github.com/fmbench/fmbench](https://github.com/fmbench/fmbench)
+
+Project Page: https://huggingface.co/fm-universe