Update README.md

README.md

@@ -16,12 +16,19 @@ tags:
 - formal-mathematics
 ---
 
-# ⚙️ BFS-Prover Tactic Generator
+<div align="center">
+<h1 style="font-size: 2.0em;">🚀 BFS-Prover Tactic Generator</h1>
+<a href="https://arxiv.org/abs/2502.03438"><img src="https://img.shields.io/badge/arXiv-2502.03438-b31b1b.svg" alt="arXiv"></a>
+<a href="https://choosealicense.com/licenses/apache-2.0/"><img src="https://img.shields.io/badge/License-Apache%202.0-blue.svg" alt="License: Apache 2.0"></a>
+<img src="https://img.shields.io/badge/Lean-4-orange" alt="Lean 4">
+State-of-the-art tactic generation model in Lean4
+</div>
 
 This repository contains the latest tactic generator model checkpoint from BFS-Prover, a state-of-the-art theorem proving system in Lean4. While the full BFS-Prover system integrates multiple components for scalable theorem proving, we are releasing the core tactic generation model that achieved state-of-the-art performance on formal mathematics tasks. Given a proof state in Lean4, the model generates a tactic that transforms the current proof state into a new state, progressively working towards completing the proof.
 
 **📄 Paper: [BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving](https://arxiv.org/abs/2502.03438)**
 
+
 ## ✨ Model Details
 
 - Base Model: Qwen2.5-Math-7B
@@ -52,7 +59,7 @@ BFS-Prover achieves state-of-the-art performance on the MiniF2F test benchmark.
 - ✅ Achieves better performance without requiring a critic model (value function)
 - ✅ Combined with simpler search method (BFS) rather than MCTS
 
-## 🚀 Usage
+## ⚙️ Usage
 - The model expects Lean4 tactic states in the format `"{state}:::"`
 - `:::` serves as a special indicator to signal the model to generate a tactic for the given state. 
 - The model will echo back the input state followed by the generated tactic.