Ultra-Low-Bit Quantization with IQ-DynamicGate (1-2 bit)

Our latest quantization method introduces precision-adaptive quantization for ultra-low-bit models (1-2 bit), with benchmark-proven improvements on Llama-3-8B. This approach uses layer-specific strategies to preserve accuracy while maintaining extreme memory efficiency.

Benchmark Context

All tests conducted on Llama-3-8B-Instruct using:

Standard perplexity evaluation pipeline
2048-token context window
Same prompt set across all quantizations

Method

Dynamic Precision Allocation:
- First/Last 25% of layers → IQ4_XS (selected layers)
- Middle 50% → IQ2_XXS/IQ3_S (increase efficiency)
Critical Component Protection:
- Embeddings/output layers use Q5_K
- Reduces error propagation by 38% vs standard 1-2bit

Quantization Performance Comparison (Llama-3-8B)

Quantization	Standard PPL	DynamicGate PPL	Δ PPL	Std Size	DG Size	Δ Size	Std Speed	DG Speed
IQ2_XXS	11.30	9.84	-12.9%	2.5G	2.6G	+0.1G	234s	246s
IQ2_XS	11.72	11.63	-0.8%	2.7G	2.8G	+0.1G	242s	246s
IQ2_S	14.31	9.02	-36.9%	2.7G	2.9G	+0.2G	238s	244s
IQ1_M	27.46	15.41	-43.9%	2.2G	2.5G	+0.3G	206s	212s
IQ1_S	53.07	32.00	-39.7%	2.1G	2.4G	+0.3G	184s	209s

Key:

PPL = Perplexity (lower is better)
Δ PPL = Percentage change from standard to DynamicGate
Speed = Inference time (CPU avx2, 2048 token context)
Size differences reflect mixed quantization overhead

Key Improvements:

🔥 IQ1_M shows massive 43.9% perplexity reduction (27.46 → 15.41)
🚀 IQ2_S cuts perplexity by 36.9% while adding only 0.2GB
⚡ IQ1_S maintains 39.7% better accuracy despite 1-bit quantization

Tradeoffs:

All variants have modest size increases (0.1-0.3GB)
Inference speeds remain comparable (<5% difference)

When to Use These Models

📌 Fitting models into GPU VRAM

✔ Memory-constrained deployments

✔ Cpu and Edge Devices where 1-2bit errors can be tolerated

✔ Research into ultra-low-bit quantization

Choosing the Right Model Format

Selecting the correct model format depends on your hardware capabilities and memory constraints.

BF16 (Brain Float 16) – Use if BF16 acceleration is available

A 16-bit floating-point format designed for faster computation while retaining good precision.
Provides similar dynamic range as FP32 but with lower memory usage.
Recommended if your hardware supports BF16 acceleration (check your device's specs).
Ideal for high-performance inference with reduced memory footprint compared to FP32.

📌 Use BF16 if:
✔ Your hardware has native BF16 support (e.g., newer GPUs, TPUs).
✔ You want higher precision while saving memory.
✔ You plan to requantize the model into another format.

📌 Avoid BF16 if:
❌ Your hardware does not support BF16 (it may fall back to FP32 and run slower).
❌ You need compatibility with older devices that lack BF16 optimization.

F16 (Float 16) – More widely supported than BF16

A 16-bit floating-point high precision but with less of range of values than BF16.
Works on most devices with FP16 acceleration support (including many GPUs and some CPUs).
Slightly lower numerical precision than BF16 but generally sufficient for inference.

📌 Use F16 if:
✔ Your hardware supports FP16 but not BF16.
✔ You need a balance between speed, memory usage, and accuracy.
✔ You are running on a GPU or another device optimized for FP16 computations.

📌 Avoid F16 if:
❌ Your device lacks native FP16 support (it may run slower than expected).
❌ You have memory limitations.

Quantized Models (Q4_K, Q6_K, Q8, etc.) – For CPU & Low-VRAM Inference

Quantization reduces model size and memory usage while maintaining as much accuracy as possible.

Lower-bit models (Q4_K) → Best for minimal memory usage, may have lower precision.
Higher-bit models (Q6_K, Q8_0) → Better accuracy, requires more memory.

📌 Use Quantized Models if:
✔ You are running inference on a CPU and need an optimized model.
✔ Your device has low VRAM and cannot load full-precision models.
✔ You want to reduce memory footprint while keeping reasonable accuracy.

📌 Avoid Quantized Models if:
❌ You need maximum accuracy (full-precision models are better for this).
❌ Your hardware has enough VRAM for higher-precision formats (BF16/F16).

Very Low-Bit Quantization (IQ3_XS, IQ3_S, IQ3_M, Q4_K, Q4_0)

These models are optimized for extreme memory efficiency, making them ideal for low-power devices or large-scale deployments where memory is a critical constraint.

IQ3_XS: Ultra-low-bit quantization (3-bit) with extreme memory efficiency.
- Use case: Best for ultra-low-memory devices where even Q4_K is too large.
- Trade-off: Lower accuracy compared to higher-bit quantizations.
IQ3_S: Small block size for maximum memory efficiency.
- Use case: Best for low-memory devices where IQ3_XS is too aggressive.
IQ3_M: Medium block size for better accuracy than IQ3_S.
- Use case: Suitable for low-memory devices where IQ3_S is too limiting.
Q4_K: 4-bit quantization with block-wise optimization for better accuracy.
- Use case: Best for low-memory devices where Q6_K is too large.
Q4_0: Pure 4-bit quantization, optimized for ARM devices.
- Use case: Best for ARM-based devices or low-memory environments.

Summary Table: Model Format Selection

Model Format	Precision	Memory Usage	Device Requirements	Best Use Case
BF16	Highest	High	BF16-supported GPU/CPUs	High-speed inference with reduced memory
F16	High	High	FP16-supported devices	GPU inference when BF16 isn't available
Q4_K	Medium Low	Low	CPU or Low-VRAM devices	Best for memory-constrained environments
Q6_K	Medium	Moderate	CPU with more memory	Better accuracy while still being quantized
Q8_0	High	Moderate	CPU or GPU with enough VRAM	Best accuracy among quantized models
IQ3_XS	Very Low	Very Low	Ultra-low-memory devices	Extreme memory efficiency and low accuracy
Q4_0	Low	Low	ARM or low-memory devices	llama.cpp can optimize for ARM devices

Included Files & Details

`DeepSeek-Prover-V2-7B-bf16.gguf`

Model weights preserved in BF16.
Use this if you want to requantize the model into a different format.
Best if your device supports BF16 acceleration.

`DeepSeek-Prover-V2-7B-f16.gguf`

Model weights stored in F16.
Use if your device supports FP16, especially if BF16 is not available.

`DeepSeek-Prover-V2-7B-bf16-q8_0.gguf`

Output & embeddings remain in BF16.
All other layers quantized to Q8_0.
Use if your device supports BF16 and you want a quantized version.

`DeepSeek-Prover-V2-7B-f16-q8_0.gguf`

Output & embeddings remain in F16.
All other layers quantized to Q8_0.

`DeepSeek-Prover-V2-7B-q4_k.gguf`

Output & embeddings quantized to Q8_0.
All other layers quantized to Q4_K.
Good for CPU inference with limited memory.

`DeepSeek-Prover-V2-7B-q4_k_s.gguf`

Smallest Q4_K variant, using less memory at the cost of accuracy.
Best for very low-memory setups.

`DeepSeek-Prover-V2-7B-q6_k.gguf`

Output & embeddings quantized to Q8_0.
All other layers quantized to Q6_K .

`DeepSeek-Prover-V2-7B-q8_0.gguf`

Fully Q8 quantized model for better accuracy.
Requires more memory but offers higher precision.

`DeepSeek-Prover-V2-7B-iq3_xs.gguf`

IQ3_XS quantization, optimized for extreme memory efficiency.
Best for ultra-low-memory devices.

`DeepSeek-Prover-V2-7B-iq3_m.gguf`

IQ3_M quantization, offering a medium block size for better accuracy.
Suitable for low-memory devices.

`DeepSeek-Prover-V2-7B-q4_0.gguf`

Pure Q4_0 quantization, optimized for ARM devices.
Best for low-memory environments.
Prefer IQ4_NL for better accuracy.

🚀 If you find these models useful

❤ Please click "Like" if you find this useful!
Help me test my AI-Powered Network Monitor Assistant with quantum-ready security checks:
👉 Quantum Network Monitor

💬 How to test:
Choose an AI assistant type:

TurboLLM (GPT-4o-mini)
HugLLM (Hugginface Open-source)
TestLLM (Experimental CPU-only)

What I’m Testing

I’m pushing the limits of small open-source models for AI network monitoring, specifically:

Function calling against live network services
How small can a model go while still handling:
- Automated Nmap scans
- Quantum-readiness checks
- Network Monitoring tasks

🟡 TestLLM – Current experimental model (llama.cpp on 2 CPU threads):

✅ Zero-configuration setup
⏳ 30s load time (slow inference but no API costs)
🔧 Help wanted! If you’re into edge-device AI, let’s collaborate!

Other Assistants

🟢 TurboLLM – Uses gpt-4o-mini for:

Create custom cmd processors to run .net code on Quantum Network Monitor Agents
Real-time network diagnostics and monitoring
Security Audits
Penetration testing (Nmap/Metasploit)

🔵 HugLLM – Latest Open-source models:

🌐 Runs on Hugging Face Inference API

💡 Example commands to you could test:

"Give me info on my websites SSL certificate"
"Check if my server is using quantum safe encyption for communication"
"Run a comprehensive security audit on my server"
'"Create a cmd processor to .. (what ever you want)" Note you need to install a Quantum Network Monitor Agent to run the .net code from. This is a very flexible and powerful feature. Use with caution!

Final Word

I fund the servers used to create these model files, run the Quantum Network Monitor service, and pay for inference from Novita and OpenAI—all out of my own pocket. All the code behind the model creation and the Quantum Network Monitor project is open source. Feel free to use whatever you find helpful.

If you appreciate the work, please consider buying me a coffee ☕. Your support helps cover service costs and allows me to raise token limits for everyone.

I'm also open to job opportunities or sponsorship.

Thank you! 😊

1. Introduction

We introduce DeepSeek-Prover-V2, an open-source large language model designed for formal theorem proving in Lean 4, with initialization data collected through a recursive theorem proving pipeline powered by DeepSeek-V3. The cold-start training procedure begins by prompting DeepSeek-V3 to decompose complex problems into a series of subgoals. The proofs of resolved subgoals are synthesized into a chain-of-thought process, combined with DeepSeek-V3's step-by-step reasoning, to create an initial cold start for reinforcement learning. This process enables us to integrate both informal and formal mathematical reasoning into a unified model.

2. Model Summary

Synthesize Cold-Start Reasoning Data through Recursive Proof Search

To construct the cold-start dataset, we develop a simple yet effective pipeline for recursive theorem proving, utilizing DeepSeek-V3 as a unified tool for both subgoal decomposition and formalization. We prompt DeepSeek-V3 to decompose theorems into high-level proof sketches while simultaneously formalizing these proof steps in Lean 4, resulting in a sequence of subgoals.
We use a smaller 7B model to handle the proof search for each subgoal, thereby reducing the associated computational burden. Once the decomposed steps of a challenging problem are resolved, we pair the complete step-by-step formal proof with the corresponding chain-of-thought from DeepSeek-V3 to create cold-start reasoning data.

DeepSeek-Prover-V2-7B GGUF Models

Model Generation Details

This model was generated using llama.cpp at commit 5e7d95e2.

Reinforcement Learning with Synthetic Cold-Start Data

We curate a subset of challenging problems that remain unsolved by the 7B prover model in an end-to-end manner, but for which all decomposed subgoals have been successfully resolved. By composing the proofs of all subgoals, we construct a complete formal proof for the original problem. This proof is then appended to DeepSeek-V3's chain-of-thought, which outlines the corresponding lemma decomposition, thereby producing a cohesive synthesis of informal reasoning and subsequent formalization.
After fine-tuning the prover model on the synthetic cold-start data, we perform a reinforcement learning stage to further enhance its ability to bridge informal reasoning with formal proof construction. Following the standard training objective for reasoning models, we use binary correct-or-incorrect feedback as the primary form of reward supervision.
The resulting model, DeepSeek-Prover-V2-671B, achieves state-of-the-art performance in neural theorem proving, reaching $88.9$% pass ratio on the MiniF2F-test and solving 49 out of 658 problems from PutnamBench. The proofs generated by DeepSeek-Prover-V2 for the miniF2F dataset are available for download as a ZIP archive.

3. ProverBench: Formalization of AIME and Textbook Problems

we introduce ProverBench, a benchmark dataset comprising 325 problems. Of these, 15 are formalized from number theory and algebra questions featured in the recent AIME competitions (AIME 24 and 25), offering authentic high-school competition-level challenges. The remaining 310 problems are drawn from curated textbook examples and educational tutorials, contributing a diverse and pedagogically grounded collection of formalized mathematical problems. This benchmark is designed to enable more comprehensive evaluation across both high-school competition problems and undergraduate-level mathematics.

Area	Count
AIME 24&25	15
Number Theory	40
Elementary Algebra	30
Linear Algebra	50
Abstract Algebra	40
Calculus	90
Real Analysis	30
Complex Analysis	10
Functional Analysis	10
Probability	10
Total	325

4. Model & Dataset Downloads

We release DeepSeek-Prover-V2 in two model sizes: 7B and 671B parameters. DeepSeek-Prover-V2-671B is trained on top of DeepSeek-V3-Base. DeepSeek-Prover-V2-7B is built upon DeepSeek-Prover-V1.5-Base and features an extended context length of up to 32K tokens.

Model	Download
DeepSeek-Prover-V2-7B	🤗 HuggingFace
DeepSeek-Prover-V2-671B	🤗 HuggingFace

Dataset	Download
DeepSeek-ProverBench	🤗 HuggingFace

5. Quick Start

You can directly use Huggingface's Transformers for model inference. DeepSeek-Prover-V2-671B shares the same architecture as DeepSeek-V3. For detailed information and supported features, please refer to the DeepSeek-V3 documentation on Hugging Face.

The following is a basic example of generating a proof for a problem from the miniF2F dataset:

from transformers import AutoModelForCausalLM, AutoTokenizer
import torch
torch.manual_seed(30)

model_id = "DeepSeek-Prover-V2-7B"  # or DeepSeek-Prover-V2-671B
tokenizer = AutoTokenizer.from_pretrained(model_id)

formal_statement = """
import Mathlib
import Aesop

set_option maxHeartbeats 0

open BigOperators Real Nat Topology Rat

/-- What is the positive difference between $120\%$ of 30 and $130\%$ of 20? Show that it is 10.-/
theorem mathd_algebra_10 : abs ((120 : ℝ) / 100 * 30 - 130 / 100 * 20) = 10 := by
  sorry
""".strip()

prompt = """
Complete the following Lean 4 code:

```lean4
{}
```

Before producing the Lean 4 code to formally prove the given theorem, provide a detailed proof plan outlining the main proof steps and strategies.
The plan should highlight key ideas, intermediate lemmas, and proof structures that will guide the construction of the final formal proof.
""".strip()

chat = [
  {"role": "user", "content": prompt.format(formal_statement)},
]

model = AutoModelForCausalLM.from_pretrained(model_id, device_map="auto", torch_dtype=torch.bfloat16, trust_remote_code=True)
inputs = tokenizer.apply_chat_template(chat, tokenize=True, add_generation_prompt=True, return_tensors="pt").to(model.device)

import time
start = time.time()
outputs = model.generate(inputs, max_new_tokens=8192)
print(tokenizer.batch_decode(outputs))
print(time.time() - start)

6. License

The use of DeepSeek-Prover-V2 models is subject to the Model License.

7. Contact

If you have any questions, please raise an issue or contact us at [email protected].

Mungert
/

DeepSeek-Prover-V2-7B-GGUF