Add GitHub repository link to model card
#2
by
nielsr
HF Staff
- opened
README.md
CHANGED
|
@@ -1,15 +1,15 @@
|
|
| 1 |
---
|
| 2 |
-
|
|
|
|
| 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 |
-
|
| 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 |
|