mradermacher/OProver-8B-GGUF
1
0
Fork 0
Code Issues Pull Requests Actions Projects Releases Wiki Activity

初始化项目，由ModelHub XC社区提供模型

Browse Source 
Model: mradermacher/OProver-8B-GGUF
Source: Original Platform
This commit is contained in:
ModelHub XC
2026-08-23 19:03:16 +08:00
commit 4e9cf82bb2
14 changed files with 163 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

47
.gitattributes vendored Normal file
View File

@@ -0,0 +1,47 @@
*.7z filter=lfs diff=lfs merge=lfs -text
*.arrow filter=lfs diff=lfs merge=lfs -text
*.bin filter=lfs diff=lfs merge=lfs -text
*.bz2 filter=lfs diff=lfs merge=lfs -text
*.ckpt filter=lfs diff=lfs merge=lfs -text
*.ftz filter=lfs diff=lfs merge=lfs -text
*.gz filter=lfs diff=lfs merge=lfs -text
*.h5 filter=lfs diff=lfs merge=lfs -text
*.joblib filter=lfs diff=lfs merge=lfs -text
*.lfs.* filter=lfs diff=lfs merge=lfs -text
*.mlmodel filter=lfs diff=lfs merge=lfs -text
*.model filter=lfs diff=lfs merge=lfs -text
*.msgpack filter=lfs diff=lfs merge=lfs -text
*.npy filter=lfs diff=lfs merge=lfs -text
*.npz filter=lfs diff=lfs merge=lfs -text
*.onnx filter=lfs diff=lfs merge=lfs -text
*.ot filter=lfs diff=lfs merge=lfs -text
*.parquet filter=lfs diff=lfs merge=lfs -text
*.pb filter=lfs diff=lfs merge=lfs -text
*.pickle filter=lfs diff=lfs merge=lfs -text
*.pkl filter=lfs diff=lfs merge=lfs -text
*.pt filter=lfs diff=lfs merge=lfs -text
*.pth filter=lfs diff=lfs merge=lfs -text
*.rar filter=lfs diff=lfs merge=lfs -text
*.safetensors filter=lfs diff=lfs merge=lfs -text
saved_model/**/* filter=lfs diff=lfs merge=lfs -text
*.tar.* filter=lfs diff=lfs merge=lfs -text
*.tar filter=lfs diff=lfs merge=lfs -text
*.tflite filter=lfs diff=lfs merge=lfs -text
*.tgz filter=lfs diff=lfs merge=lfs -text
*.wasm filter=lfs diff=lfs merge=lfs -text
*.xz filter=lfs diff=lfs merge=lfs -text
*.zip filter=lfs diff=lfs merge=lfs -text
*.zst filter=lfs diff=lfs merge=lfs -text
*tfevents* filter=lfs diff=lfs merge=lfs -text
OProver-8B.Q4_K_S.gguf filter=lfs diff=lfs merge=lfs -text
OProver-8B.Q2_K.gguf filter=lfs diff=lfs merge=lfs -text
OProver-8B.f16.gguf filter=lfs diff=lfs merge=lfs -text
OProver-8B.Q3_K_M.gguf filter=lfs diff=lfs merge=lfs -text
OProver-8B.Q8_0.gguf filter=lfs diff=lfs merge=lfs -text
OProver-8B.Q6_K.gguf filter=lfs diff=lfs merge=lfs -text
OProver-8B.Q3_K_S.gguf filter=lfs diff=lfs merge=lfs -text
OProver-8B.Q3_K_L.gguf filter=lfs diff=lfs merge=lfs -text
OProver-8B.Q4_K_M.gguf filter=lfs diff=lfs merge=lfs -text
OProver-8B.Q5_K_S.gguf filter=lfs diff=lfs merge=lfs -text
OProver-8B.Q5_K_M.gguf filter=lfs diff=lfs merge=lfs -text
OProver-8B.IQ4_XS.gguf filter=lfs diff=lfs merge=lfs -text

3
OProver-8B.IQ4_XS.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:7a0cb2a952af95814e7a5bf7af07113764a08027eacedb3f25577915ed549137
size 4593296704

3
OProver-8B.Q2_K.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:9a43b04ea2fc1a10c38854b56f36bcb322766a58979416980ab75eced2efba26
size 3281732928

3
OProver-8B.Q3_K_L.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:2d827eb8e7768373f2025ad96848e26140eb3294e285d3e0c9691974b1dadcbf
size 4431394112

3
OProver-8B.Q3_K_M.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:18eaa337b04a8d337a8a40fcee3059d8c3cf61b75130b10a455d7b31ea57284a
size 4124161344

3
OProver-8B.Q3_K_S.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:8a157487ab933de22fa2742544799050fa9f404a9d5c024ede4e2ce05bebf87f
size 3769611584

3
OProver-8B.Q4_K_M.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:415c30546446c712898e4a162453bc229c49cc77ad61430de3d81afa88777aff
size 5027784000

3
OProver-8B.Q4_K_S.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:15df3a99eeb7f6874479c7033300b843ff4d370b28b46ab9bfa020957ec931ad
size 4802012480

3
OProver-8B.Q5_K_M.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:f878ebbf7fdb417aa96497f1ba91ec33c4a0d17c2f712ee6bb51fcb334f281d1
size 5851112768

3
OProver-8B.Q5_K_S.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:4bcd8ca4e6c1cc31828a88979ff0d6b07a7ab7ad815b1e0f41a34024d9180d1a
size 5720761664

3
OProver-8B.Q6_K.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:779aa97304daec3faf747256f4994d6a498031c602d883b05aa38ff2ddc0ff34
size 6725899584

3
OProver-8B.Q8_0.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:3e08c36a8f91d968900d5823c9ad32655c850d41aef3abeab2629400de7ad174
size 8709518656

3
OProver-8B.f16.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:ba51946c9f5ee78d4df00038ef5b5441b4976616f6b16182eddcc24ba73b24f7
size 16388044096

80
README.md Normal file
View File

@@ -0,0 +1,80 @@
---
base_model: m-a-p/OProver-8B
datasets:
- m-a-p/OProofs
language:
- en
library_name: transformers
license: apache-2.0
mradermacher:
readme_rev: 1
quantized_by: mradermacher
tags:
- lean4
- theorem-proving
- formal-mathematics
- agentic
- retrieval-augmented
---
## About
<!-- ### quantize_version: 2 -->
<!-- ### output_tensor_quantised: 1 -->
<!-- ### convert_type: hf -->
<!-- ### vocab_type: -->
<!-- ### tags: -->
<!-- ### quants: x-f16 Q4_K_S Q2_K Q8_0 Q6_K Q3_K_M Q3_K_S Q3_K_L Q4_K_M Q5_K_S Q5_K_M IQ4_XS -->
<!-- ### quants_skip: -->
<!-- ### skip_mmproj: -->
static quants of https://huggingface.co/m-a-p/OProver-8B
<!-- provided-files -->
***For a convenient overview and download list, visit our [model page for this model](https://hf.tst.eu/model#OProver-8B-GGUF).***
weighted/imatrix quants seem not to be available (by me) at this time. If they do not show up a week or so after the static ones, I have probably not planned for them. Feel free to request them by opening a Community Discussion.
## Usage
If you are unsure how to use GGUF files, refer to one of [TheBloke's
READMEs](https://huggingface.co/TheBloke/KafkaLM-70B-German-V0.1-GGUF) for
more details, including on how to concatenate multi-part files.
## Provided Quants
(sorted by size, not necessarily quality. IQ-quants are often preferable over similar sized non-IQ quants)
| Link | Type | Size/GB | Notes |
|:-----|:-----|--------:|:------|
| [GGUF](https://huggingface.co/mradermacher/OProver-8B-GGUF/resolve/main/OProver-8B.Q2_K.gguf) | Q2_K | 3.4 | |
| [GGUF](https://huggingface.co/mradermacher/OProver-8B-GGUF/resolve/main/OProver-8B.Q3_K_S.gguf) | Q3_K_S | 3.9 | |
| [GGUF](https://huggingface.co/mradermacher/OProver-8B-GGUF/resolve/main/OProver-8B.Q3_K_M.gguf) | Q3_K_M | 4.2 | lower quality |
| [GGUF](https://huggingface.co/mradermacher/OProver-8B-GGUF/resolve/main/OProver-8B.Q3_K_L.gguf) | Q3_K_L | 4.5 | |
| [GGUF](https://huggingface.co/mradermacher/OProver-8B-GGUF/resolve/main/OProver-8B.IQ4_XS.gguf) | IQ4_XS | 4.7 | |
| [GGUF](https://huggingface.co/mradermacher/OProver-8B-GGUF/resolve/main/OProver-8B.Q4_K_S.gguf) | Q4_K_S | 4.9 | fast, recommended |
| [GGUF](https://huggingface.co/mradermacher/OProver-8B-GGUF/resolve/main/OProver-8B.Q4_K_M.gguf) | Q4_K_M | 5.1 | fast, recommended |
| [GGUF](https://huggingface.co/mradermacher/OProver-8B-GGUF/resolve/main/OProver-8B.Q5_K_S.gguf) | Q5_K_S | 5.8 | |
| [GGUF](https://huggingface.co/mradermacher/OProver-8B-GGUF/resolve/main/OProver-8B.Q5_K_M.gguf) | Q5_K_M | 6.0 | |
| [GGUF](https://huggingface.co/mradermacher/OProver-8B-GGUF/resolve/main/OProver-8B.Q6_K.gguf) | Q6_K | 6.8 | very good quality |
| [GGUF](https://huggingface.co/mradermacher/OProver-8B-GGUF/resolve/main/OProver-8B.Q8_0.gguf) | Q8_0 | 8.8 | fast, best quality |
| [GGUF](https://huggingface.co/mradermacher/OProver-8B-GGUF/resolve/main/OProver-8B.f16.gguf) | f16 | 16.5 | 16 bpw, overkill |
Here is a handy graph by ikawrakow comparing some lower-quality quant
types (lower is better):
![image.png](https://www.nethype.de/huggingface_embed/quantpplgraph.png)
And here are Artefact2's thoughts on the matter:
https://gist.github.com/Artefact2/b5f810600771265fc1e39442288e8ec9
## FAQ / Model Request
See https://huggingface.co/mradermacher/model_requests for some answers to
questions you might have and/or if you want some other model quantized.
## Thanks
I thank my company, [nethype GmbH](https://www.nethype.de/), for letting
me use its servers and providing upgrades to my workstation to enable
this work in my free time.
<!-- end -->