Add GitHub repository link to model card

#2
by nielsr HF Staff - opened
Files changed (1) hide show
  1. README.md +7 -5
README.md CHANGED
@@ -1,15 +1,15 @@
1
  ---
2
- license: apache-2.0
 
3
  datasets:
4
  - internlm/Lean-Workbook
5
  - internlm/Lean-Github
6
  - AI-MO/NuminaMath-CoT
7
  language:
8
  - en
9
- base_model:
10
- - Qwen/Qwen2.5-Math-7B
11
- pipeline_tag: text-generation
12
  library_name: transformers
 
 
13
  tags:
14
  - lean4
15
  - theorem-proving
@@ -20,6 +20,7 @@ tags:
20
  <h1 style="font-size: 2.0em;">πŸš€ BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving</h1>
21
  <div style="display: flex; justify-content: center; gap: 8px; flex-wrap: wrap;">
22
  <a href="https://arxiv.org/abs/2502.03438"><img src="https://img.shields.io/badge/arXiv-2502.03438-b31b1b.svg" alt="arXiv"></a>
 
23
  <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>
24
  <a href="https://github.com/leanprover-community/mathlib4"><img src="https://img.shields.io/badge/Lean-4-orange" alt="Lean 4"></a>
25
  </div>
@@ -28,8 +29,9 @@ tags:
28
 
29
  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 here. 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.
30
 
31
- **πŸ“„ Paper: [BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving](https://arxiv.org/abs/2502.03438)**
32
 
 
33
 
34
  ## ✨ Model Details
35
 
 
1
  ---
2
+ base_model:
3
+ - Qwen/Qwen2.5-Math-7B
4
  datasets:
5
  - internlm/Lean-Workbook
6
  - internlm/Lean-Github
7
  - AI-MO/NuminaMath-CoT
8
  language:
9
  - en
 
 
 
10
  library_name: transformers
11
+ license: apache-2.0
12
+ pipeline_tag: text-generation
13
  tags:
14
  - lean4
15
  - theorem-proving
 
20
  <h1 style="font-size: 2.0em;">πŸš€ BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving</h1>
21
  <div style="display: flex; justify-content: center; gap: 8px; flex-wrap: wrap;">
22
  <a href="https://arxiv.org/abs/2502.03438"><img src="https://img.shields.io/badge/arXiv-2502.03438-b31b1b.svg" alt="arXiv"></a>
23
+ <a href="https://github.com/bytedance-research/BFS-Prover"><img src="https://img.shields.io/badge/GitHub-Code-blue.svg?logo=github" alt="GitHub Code"></a>
24
  <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>
25
  <a href="https://github.com/leanprover-community/mathlib4"><img src="https://img.shields.io/badge/Lean-4-orange" alt="Lean 4"></a>
26
  </div>
 
29
 
30
  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 here. 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.
31
 
32
+ **πŸ“‘ Paper: [BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving](https://arxiv.org/abs/2502.03438)**
33
 
34
+ **πŸ’» Code: [GitHub Repository](https://github.com/ByteDance-Seed/BFS-Prover-V2)**
35
 
36
  ## ✨ Model Details
37