Hugging Face's logo

tensorblock
/
BFS-Prover-GGUF

Text Generation
Transformers
GGUF
English
lean4
theorem-proving
formal-mathematics
TensorBlock
GGUF
conversational
Model card Files
xet
 Community
morriszms commited on
Commit
f260e55
·
verified ·
1 Parent(s): a1ab4ff

Upload folder using huggingface_hub

Browse files
Files changed (14) hide show
  1. .gitattributes +12 -0
  2. BFS-Prover-Q2_K.gguf +3 -0
  3. BFS-Prover-Q3_K_L.gguf +3 -0
  4. BFS-Prover-Q3_K_M.gguf +3 -0
  5. BFS-Prover-Q3_K_S.gguf +3 -0
  6. BFS-Prover-Q4_0.gguf +3 -0
  7. BFS-Prover-Q4_K_M.gguf +3 -0
  8. BFS-Prover-Q4_K_S.gguf +3 -0
  9. BFS-Prover-Q5_0.gguf +3 -0
  10. BFS-Prover-Q5_K_M.gguf +3 -0
  11. BFS-Prover-Q5_K_S.gguf +3 -0
  12. BFS-Prover-Q6_K.gguf +3 -0
  13. BFS-Prover-Q8_0.gguf +3 -0
  14. README.md +91 -0
.gitattributes CHANGED
@@ -33,3 +33,15 @@ saved_model/**/* filter=lfs diff=lfs merge=lfs -text
33
  *.zip filter=lfs diff=lfs merge=lfs -text
34
  *.zst filter=lfs diff=lfs merge=lfs -text
35
  *tfevents* filter=lfs diff=lfs merge=lfs -text
 
 
 
 
 
 
 
 
 
 
 
 
 
33
  *.zip filter=lfs diff=lfs merge=lfs -text
34
  *.zst filter=lfs diff=lfs merge=lfs -text
35
  *tfevents* filter=lfs diff=lfs merge=lfs -text
36
+ BFS-Prover-Q2_K.gguf filter=lfs diff=lfs merge=lfs -text
37
+ BFS-Prover-Q3_K_L.gguf filter=lfs diff=lfs merge=lfs -text
38
+ BFS-Prover-Q3_K_M.gguf filter=lfs diff=lfs merge=lfs -text
39
+ BFS-Prover-Q3_K_S.gguf filter=lfs diff=lfs merge=lfs -text
40
+ BFS-Prover-Q4_0.gguf filter=lfs diff=lfs merge=lfs -text
41
+ BFS-Prover-Q4_K_M.gguf filter=lfs diff=lfs merge=lfs -text
42
+ BFS-Prover-Q4_K_S.gguf filter=lfs diff=lfs merge=lfs -text
43
+ BFS-Prover-Q5_0.gguf filter=lfs diff=lfs merge=lfs -text
44
+ BFS-Prover-Q5_K_M.gguf filter=lfs diff=lfs merge=lfs -text
45
+ BFS-Prover-Q5_K_S.gguf filter=lfs diff=lfs merge=lfs -text
46
+ BFS-Prover-Q6_K.gguf filter=lfs diff=lfs merge=lfs -text
47
+ BFS-Prover-Q8_0.gguf filter=lfs diff=lfs merge=lfs -text
BFS-Prover-Q2_K.gguf ADDED
@@ -0,0 +1,3 @@
 
 
 
 
1
+ version https://git-lfs.github.com/spec/v1
2
+ oid sha256:651395ea4d0d8bfda52be70c8c125318ed09f718dae559dcabb48fd7ce6b2dac
3
+ size 3015941056
BFS-Prover-Q3_K_L.gguf ADDED
@@ -0,0 +1,3 @@
 
 
 
 
1
+ version https://git-lfs.github.com/spec/v1
2
+ oid sha256:bc2cdaee0bb85575194b793092413f00f719f8c13f7d36e08d804c91b9205e7f
3
+ size 4088460224
BFS-Prover-Q3_K_M.gguf ADDED
@@ -0,0 +1,3 @@
 
 
 
 
1
+ version https://git-lfs.github.com/spec/v1
2
+ oid sha256:73332c65a6d5b475b17e0898cbc48620d5cb92349e7e7d2b84ce4233b62a2910
3
+ size 3808392128
BFS-Prover-Q3_K_S.gguf ADDED
@@ -0,0 +1,3 @@
 
 
 
 
1
+ version https://git-lfs.github.com/spec/v1
2
+ oid sha256:13c0f3c41d5416752946acf8ee80604c37d8afb9e00326c5dc657e986f7a2e60
3
+ size 3492369344
BFS-Prover-Q4_0.gguf ADDED
@@ -0,0 +1,3 @@
 
 
 
 
1
+ version https://git-lfs.github.com/spec/v1
2
+ oid sha256:b65c9bf9c2c120918608036c40eb504d17654e5d5621f4e526ff0254c9b40ff0
3
+ size 4431391680
BFS-Prover-Q4_K_M.gguf ADDED
@@ -0,0 +1,3 @@
 
 
 
 
1
+ version https://git-lfs.github.com/spec/v1
2
+ oid sha256:557e8b77f51e21b55fa562a91163c113161eb6e3afe144c52c322d2b0b9e841c
3
+ size 4683074496
BFS-Prover-Q4_K_S.gguf ADDED
@@ -0,0 +1,3 @@
 
 
 
 
1
+ version https://git-lfs.github.com/spec/v1
2
+ oid sha256:0a84d064c9fa4435e78930b68d57c35558bd5471cbe91fc88f682d18f5833dcf
3
+ size 4457769920
BFS-Prover-Q5_0.gguf ADDED
@@ -0,0 +1,3 @@
 
 
 
 
1
+ version https://git-lfs.github.com/spec/v1
2
+ oid sha256:72a6c567984d1a24d93f3bd78debfa2e8b0b246f2fb61b777cadbc404050e29e
3
+ size 5315177408
BFS-Prover-Q5_K_M.gguf ADDED
@@ -0,0 +1,3 @@
 
 
 
 
1
+ version https://git-lfs.github.com/spec/v1
2
+ oid sha256:3c8312ee4e3ac916965dc5ddef407bbfdb3ec119fc61f5f8a48db1f965799881
3
+ size 5444832192
BFS-Prover-Q5_K_S.gguf ADDED
@@ -0,0 +1,3 @@
 
 
 
 
1
+ version https://git-lfs.github.com/spec/v1
2
+ oid sha256:3ccd08ad1f5e0538562daf6732ce874231d777888c9b32917d6ab5b955e56bbc
3
+ size 5315177408
BFS-Prover-Q6_K.gguf ADDED
@@ -0,0 +1,3 @@
 
 
 
 
1
+ version https://git-lfs.github.com/spec/v1
2
+ oid sha256:1dd809f6fd16abc101b2ea831330d0ce1f1e8db5473fb318e70f30fa48a7a607
3
+ size 6254199744
BFS-Prover-Q8_0.gguf ADDED
@@ -0,0 +1,3 @@
 
 
 
 
1
+ version https://git-lfs.github.com/spec/v1
2
+ oid sha256:777ed32d2ab6f4418bb4f82eb70d32c83b3bc2ae0e18f6aabb25aedfb047bf85
3
+ size 8098526144
README.md ADDED
@@ -0,0 +1,91 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
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: bytedance-research/BFS-Prover
10
+ pipeline_tag: text-generation
11
+ library_name: transformers
12
+ tags:
13
+ - lean4
14
+ - theorem-proving
15
+ - formal-mathematics
16
+ - TensorBlock
17
+ - GGUF
18
+ ---
19
+
20
+ <div style="width: auto; margin-left: auto; margin-right: auto">
21
+ <img src="https://i.imgur.com/jC7kdl8.jpeg" alt="TensorBlock" style="width: 100%; min-width: 400px; display: block; margin: auto;">
22
+ </div>
23
+ <div style="display: flex; justify-content: space-between; width: 100%;">
24
+ <div style="display: flex; flex-direction: column; align-items: flex-start;">
25
+ <p style="margin-top: 0.5em; margin-bottom: 0em;">
26
+ Feedback and support: TensorBlock's <a href="https://x.com/tensorblock_aoi">Twitter/X</a>, <a href="https://t.me/TensorBlock">Telegram Group</a> and <a href="https://x.com/tensorblock_aoi">Discord server</a>
27
+ </p>
28
+ </div>
29
+ </div>
30
+
31
+ ## bytedance-research/BFS-Prover - GGUF
32
+
33
+ This repo contains GGUF format model files for [bytedance-research/BFS-Prover](https://huggingface.co/bytedance-research/BFS-Prover).
34
+
35
+ The files were quantized using machines provided by [TensorBlock](https://tensorblock.co/), and they are compatible with llama.cpp as of [commit b4823](https://github.com/ggml-org/llama.cpp/commit/5bbe6a9fe9a8796a9389c85accec89dbc4d91e39).
36
+
37
+ <div style="text-align: left; margin: 20px 0;">
38
+ <a href="https://tensorblock.co/waitlist/client" style="display: inline-block; padding: 10px 20px; background-color: #007bff; color: white; text-decoration: none; border-radius: 5px; font-weight: bold;">
39
+ Run them on the TensorBlock client using your local machine ↗
40
+ </a>
41
+ </div>
42
+
43
+ ## Prompt template
44
+
45
+ ```
46
+ <|im_start|>system
47
+ {system_prompt}<|im_end|>
48
+ <|im_start|>user
49
+ {prompt}<|im_end|>
50
+ <|im_start|>assistant
51
+ ```
52
+
53
+ ## Model file specification
54
+
55
+ | Filename | Quant type | File Size | Description |
56
+ | -------- | ---------- | --------- | ----------- |
57
+ | [BFS-Prover-Q2_K.gguf](https://huggingface.co/tensorblock/BFS-Prover-GGUF/blob/main/BFS-Prover-Q2_K.gguf) | Q2_K | 3.016 GB | smallest, significant quality loss - not recommended for most purposes |
58
+ | [BFS-Prover-Q3_K_S.gguf](https://huggingface.co/tensorblock/BFS-Prover-GGUF/blob/main/BFS-Prover-Q3_K_S.gguf) | Q3_K_S | 3.492 GB | very small, high quality loss |
59
+ | [BFS-Prover-Q3_K_M.gguf](https://huggingface.co/tensorblock/BFS-Prover-GGUF/blob/main/BFS-Prover-Q3_K_M.gguf) | Q3_K_M | 3.808 GB | very small, high quality loss |
60
+ | [BFS-Prover-Q3_K_L.gguf](https://huggingface.co/tensorblock/BFS-Prover-GGUF/blob/main/BFS-Prover-Q3_K_L.gguf) | Q3_K_L | 4.088 GB | small, substantial quality loss |
61
+ | [BFS-Prover-Q4_0.gguf](https://huggingface.co/tensorblock/BFS-Prover-GGUF/blob/main/BFS-Prover-Q4_0.gguf) | Q4_0 | 4.431 GB | legacy; small, very high quality loss - prefer using Q3_K_M |
62
+ | [BFS-Prover-Q4_K_S.gguf](https://huggingface.co/tensorblock/BFS-Prover-GGUF/blob/main/BFS-Prover-Q4_K_S.gguf) | Q4_K_S | 4.458 GB | small, greater quality loss |
63
+ | [BFS-Prover-Q4_K_M.gguf](https://huggingface.co/tensorblock/BFS-Prover-GGUF/blob/main/BFS-Prover-Q4_K_M.gguf) | Q4_K_M | 4.683 GB | medium, balanced quality - recommended |
64
+ | [BFS-Prover-Q5_0.gguf](https://huggingface.co/tensorblock/BFS-Prover-GGUF/blob/main/BFS-Prover-Q5_0.gguf) | Q5_0 | 5.315 GB | legacy; medium, balanced quality - prefer using Q4_K_M |
65
+ | [BFS-Prover-Q5_K_S.gguf](https://huggingface.co/tensorblock/BFS-Prover-GGUF/blob/main/BFS-Prover-Q5_K_S.gguf) | Q5_K_S | 5.315 GB | large, low quality loss - recommended |
66
+ | [BFS-Prover-Q5_K_M.gguf](https://huggingface.co/tensorblock/BFS-Prover-GGUF/blob/main/BFS-Prover-Q5_K_M.gguf) | Q5_K_M | 5.445 GB | large, very low quality loss - recommended |
67
+ | [BFS-Prover-Q6_K.gguf](https://huggingface.co/tensorblock/BFS-Prover-GGUF/blob/main/BFS-Prover-Q6_K.gguf) | Q6_K | 6.254 GB | very large, extremely low quality loss |
68
+ | [BFS-Prover-Q8_0.gguf](https://huggingface.co/tensorblock/BFS-Prover-GGUF/blob/main/BFS-Prover-Q8_0.gguf) | Q8_0 | 8.099 GB | very large, extremely low quality loss - not recommended |
69
+
70
+
71
+ ## Downloading instruction
72
+
73
+ ### Command line
74
+
75
+ Firstly, install Huggingface Client
76
+
77
+ ```shell
78
+ pip install -U "huggingface_hub[cli]"
79
+ ```
80
+
81
+ Then, downoad the individual model file the a local directory
82
+
83
+ ```shell
84
+ huggingface-cli download tensorblock/BFS-Prover-GGUF --include "BFS-Prover-Q2_K.gguf" --local-dir MY_LOCAL_DIR
85
+ ```
86
+
87
+ If you wanna download multiple model files with a pattern (e.g., `*Q4_K*gguf`), you can try:
88
+
89
+ ```shell
90
+ huggingface-cli download tensorblock/BFS-Prover-GGUF --local-dir MY_LOCAL_DIR --local-dir-use-symlinks False --include='*Q4_K*gguf'
91
+ ```