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

Model: mradermacher/OProver-8B-Base-GGUF
Source: Original Platform
This commit is contained in:
ModelHub XC
2026-06-01 02:43:17 +08:00
commit 7479e2ea1c
14 changed files with 163 additions and 0 deletions

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-Base.Q4_K_S.gguf filter=lfs diff=lfs merge=lfs -text
OProver-8B-Base.Q2_K.gguf filter=lfs diff=lfs merge=lfs -text
OProver-8B-Base.Q3_K_M.gguf filter=lfs diff=lfs merge=lfs -text
OProver-8B-Base.Q6_K.gguf filter=lfs diff=lfs merge=lfs -text
OProver-8B-Base.Q8_0.gguf filter=lfs diff=lfs merge=lfs -text
OProver-8B-Base.Q3_K_S.gguf filter=lfs diff=lfs merge=lfs -text
OProver-8B-Base.f16.gguf filter=lfs diff=lfs merge=lfs -text
OProver-8B-Base.Q3_K_L.gguf filter=lfs diff=lfs merge=lfs -text
OProver-8B-Base.Q4_K_M.gguf filter=lfs diff=lfs merge=lfs -text
OProver-8B-Base.Q5_K_S.gguf filter=lfs diff=lfs merge=lfs -text
OProver-8B-Base.Q5_K_M.gguf filter=lfs diff=lfs merge=lfs -text
OProver-8B-Base.IQ4_XS.gguf filter=lfs diff=lfs merge=lfs -text

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

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

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

80
README.md Normal file
View File

@@ -0,0 +1,80 @@
---
base_model: m-a-p/OProver-8B-Base
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-Base
<!-- provided-files -->
***For a convenient overview and download list, visit our [model page for this model](https://hf.tst.eu/model#OProver-8B-Base-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-Base-GGUF/resolve/main/OProver-8B-Base.Q2_K.gguf) | Q2_K | 3.4 | |
| [GGUF](https://huggingface.co/mradermacher/OProver-8B-Base-GGUF/resolve/main/OProver-8B-Base.Q3_K_S.gguf) | Q3_K_S | 3.9 | |
| [GGUF](https://huggingface.co/mradermacher/OProver-8B-Base-GGUF/resolve/main/OProver-8B-Base.Q3_K_M.gguf) | Q3_K_M | 4.2 | lower quality |
| [GGUF](https://huggingface.co/mradermacher/OProver-8B-Base-GGUF/resolve/main/OProver-8B-Base.Q3_K_L.gguf) | Q3_K_L | 4.5 | |
| [GGUF](https://huggingface.co/mradermacher/OProver-8B-Base-GGUF/resolve/main/OProver-8B-Base.IQ4_XS.gguf) | IQ4_XS | 4.7 | |
| [GGUF](https://huggingface.co/mradermacher/OProver-8B-Base-GGUF/resolve/main/OProver-8B-Base.Q4_K_S.gguf) | Q4_K_S | 4.9 | fast, recommended |
| [GGUF](https://huggingface.co/mradermacher/OProver-8B-Base-GGUF/resolve/main/OProver-8B-Base.Q4_K_M.gguf) | Q4_K_M | 5.1 | fast, recommended |
| [GGUF](https://huggingface.co/mradermacher/OProver-8B-Base-GGUF/resolve/main/OProver-8B-Base.Q5_K_S.gguf) | Q5_K_S | 5.8 | |
| [GGUF](https://huggingface.co/mradermacher/OProver-8B-Base-GGUF/resolve/main/OProver-8B-Base.Q5_K_M.gguf) | Q5_K_M | 6.0 | |
| [GGUF](https://huggingface.co/mradermacher/OProver-8B-Base-GGUF/resolve/main/OProver-8B-Base.Q6_K.gguf) | Q6_K | 6.8 | very good quality |
| [GGUF](https://huggingface.co/mradermacher/OProver-8B-Base-GGUF/resolve/main/OProver-8B-Base.Q8_0.gguf) | Q8_0 | 8.8 | fast, best quality |
| [GGUF](https://huggingface.co/mradermacher/OProver-8B-Base-GGUF/resolve/main/OProver-8B-Base.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 -->