Add comprehensive model card with documentation

README.md

@@ -0,0 +1,574 @@
+---
+license: apache-2.0
+base_model: ByteDance-Seed/BFS-Prover-V2-32B
+language:
+- en
+library_name: gguf
+tags:
+- gguf
+- quantized
+- llama-cpp
+- ollama
+- qwen2.5
+- formal-verification
+- theorem-proving
+- lean4
+- mathematics
+- proof-generation
+- 32b
+- 131k-context
+pipeline_tag: text-generation
+widget:
+- text: "theorem add_comm (a b : Nat) : a + b = b + a :::"
+  example_title: "Lean4 Proof State"
+- text: "∀ n : Nat, n + 0 = n :::"
+  example_title: "Natural Number Property"
+model-index:
+- name: BFS-Prover-V2-32B-GGUF
+  results: []
+---
+
+# BFS-Prover-V2-32B (GGUF Quantized)
+
+<div align="center">
+
+[![Model on HF](https://huggingface.co/datasets/huggingface/badges/resolve/main/model-on-hf-md.svg)](https://huggingface.co/richardyoung/bfs-prover-v2-32b)
+[![License: Apache 2.0](https://img.shields.io/badge/License-Apache%202.0-blue.svg)](https://opensource.org/licenses/Apache-2.0)
+[![GGUF](https://img.shields.io/badge/Format-GGUF-green)](https://github.com/ggerganov/llama.cpp)
+[![Qwen2.5](https://img.shields.io/badge/Architecture-Qwen2.5--32B-purple)](https://huggingface.co/Qwen)
+
+**Formal Mathematical Proof Generation · Lean4 Theorem Proving · 131K Context**
+
+</div>
+
+## Model Overview
+
+**BFS-Prover-V2-32B** is a specialized large language model fine-tuned for **formal mathematical proof generation** and **theorem proving** in Lean4. This model excels at generating formal proofs, completing proof states, and assisting with mathematical formalization tasks.
+
+This repository contains **GGUF-quantized versions** optimized for efficient inference with **llama.cpp** and **Ollama**.
+
+### Key Features
+
+- 🔬 **Formal Verification**: Generates valid Lean4 proofs
+- 🧮 **Mathematical Reasoning**: Strong understanding of mathematical concepts
+- 📚 **131K Context**: Handle complex proof sequences and large mathematical contexts
+- ⚡ **GGUF Format**: Optimized for fast inference with llama.cpp
+- 🔧 **Multiple Quantizations**: Choose the right balance for your hardware
+- 🎯 **Specialized Prompting**: Custom Lean4 proof state format
+
+---
+
+## Table of Contents
+
+- [Model Details](#model-details)
+- [Quantization Variants](#quantization-variants)
+- [Usage](#usage)
+  - [Ollama](#ollama)
+  - [llama.cpp](#llamacpp)
+  - [Python](#python)
+- [Prompt Format](#prompt-format)
+- [Use Cases](#use-cases)
+- [Limitations](#limitations)
+- [Citation](#citation)
+- [License](#license)
+
+---
+
+## Model Details
+
+### Architecture
+
+- **Base Model**: [ByteDance-Seed/BFS-Prover-V2-32B](https://huggingface.co/ByteDance-Seed/BFS-Prover-V2-32B)
+- **Architecture**: Qwen2.5-32B
+- **Parameters**: 32 Billion
+- **Context Length**: 131,072 tokens (131K)
+- **Format**: GGUF (optimized for llama.cpp)
+- **Quantization**: Multiple variants (F16, Q5_K_M, Q4_K_M)
+- **License**: Apache 2.0
+
+### Specialization
+
+This model is specifically fine-tuned for:
+
+- **Lean4 Theorem Proving**: Generate formal proofs in Lean4
+- **Proof Completion**: Complete partial proof states
+- **Mathematical Formalization**: Translate informal math to formal statements
+- **Tactic Generation**: Suggest proof tactics for given goals
+- **Proof Search**: Explore proof spaces using BFS (Breadth-First Search)
+
+### Training
+
+- **Developed by**: ByteDance-Seed Team
+- **Quantized by**: richardyoung
+- **Base Architecture**: Qwen2.5-32B
+- **Fine-tuning**: Specialized on formal mathematics and Lean4 proofs
+- **Training Data**: Formal mathematics, Lean4 libraries, and proof corpora
+
+---
+
+## Quantization Variants
+
+Choose the variant that best fits your hardware and performance requirements:
+
+| Variant | Size | Memory Required | Speed | Quality | Use Case |
+|---------|------|-----------------|-------|---------|----------|
+| **F16** | ~61 GB | 64+ GB RAM | Slowest | Highest | Research, maximum precision |
+| **Q5_K_M** ⭐ | ~22 GB | 24+ GB RAM | Balanced | Excellent | **Recommended default** |
+| **Q4_K_M** | ~18 GB | 20+ GB RAM | Fastest | Very Good | Consumer GPUs, lower memory |
+
+### Recommended Configurations
+
+**High-End Workstation (32+ GB RAM):**
+```bash
+# Use Q5_K_M for best quality/performance balance
+ollama run richardyoung/bfs-prover-v2-32b:Q5_K_M
+```
+
+**Consumer Hardware (20-32 GB RAM):**
+```bash
+# Use Q4_K_M for faster inference with lower memory
+ollama run richardyoung/bfs-prover-v2-32b:Q4_K_M
+```
+
+**Research/Maximum Precision:**
+```bash
+# Use F16 for highest fidelity (requires 64+ GB RAM)
+llama-cli -m BFS-Prover-V2-32B-F16.gguf
+```
+
+---
+
+## Usage
+
+### Ollama
+
+#### Installation
+
+```bash
+# Pull the model (Q5_K_M recommended)
+ollama pull richardyoung/bfs-prover-v2-32b:Q5_K_M
+
+# Or create from local Modelfile
+cd /path/to/model
+ollama create richardyoung/bfs-prover-v2-32b:Q5_K_M -f Modelfile.Q5_K_M
+```
+
+#### Basic Usage
+
+```bash
+# Start an interactive session
+ollama run richardyoung/bfs-prover-v2-32b:Q5_K_M
+
+# Single proof query (note the ::: suffix)
+ollama run richardyoung/bfs-prover-v2-32b:Q5_K_M "theorem add_comm (a b : Nat) : a + b = b + a :::"
+```
+
+#### Modelfile
+
+```dockerfile
+FROM ./BFS-Prover-V2-32B-Q5_K_M.gguf
+
+# Lean4-specific prompt template (appends ::: to user messages)
+TEMPLATE """{{- range $i, $m := .Messages }}{{- if eq $m.Role "user" }}{{ $m.Content }}:::{{ end }}{{- if eq $m.Role "assistant" }}{{ $m.Content }}{{ end }}{{- end }}"""
+
+# Optimized parameters for formal proof generation
+PARAMETER temperature 0.2
+PARAMETER top_p 0.95
+PARAMETER num_ctx 131072
+
+# System message
+SYSTEM """You are a formal mathematics expert specializing in Lean4 theorem proving. Generate valid, well-structured proofs."""
+```
+
+### llama.cpp
+
+#### Command Line
+
+```bash
+# Download model
+wget https://huggingface.co/richardyoung/bfs-prover-v2-32b/resolve/main/BFS-Prover-V2-32B-Q5_K_M.gguf
+
+# Run inference
+./llama-cli \
+  -m BFS-Prover-V2-32B-Q5_K_M.gguf \
+  -p "theorem zero_add (n : Nat) : 0 + n = n :::" \
+  -n 512 \
+  -c 131072 \
+  --temp 0.2 \
+  --top-p 0.95
+```
+
+#### C++ API
+
+```cpp
+#include "llama.h"
+
+// Load model
+auto model = llama_load_model_from_file("BFS-Prover-V2-32B-Q5_K_M.gguf", params);
+
+// Set context with large window
+llama_context_params ctx_params = llama_context_default_params();
+ctx_params.n_ctx = 131072;
+auto ctx = llama_new_context_with_model(model, ctx_params);
+
+// Generate proof
+std::string prompt = "theorem add_comm (a b : Nat) : a + b = b + a :::";
+// ... inference code
+```
+
+### Python
+
+#### Using llama-cpp-python
+
+```python
+from llama_cpp import Llama
+
+# Load model
+llm = Llama(
+    model_path="./BFS-Prover-V2-32B-Q5_K_M.gguf",
+    n_ctx=131072,
+    n_threads=8,
+    n_gpu_layers=35  # Adjust based on your GPU
+)
+
+# Generate proof
+proof_state = "theorem mul_comm (a b : Nat) : a * b = b * a :::"
+
+output = llm(
+    proof_state,
+    max_tokens=512,
+    temperature=0.2,
+    top_p=0.95,
+    stop=["<|endoftext|>"]
+)
+
+print(output['choices'][0]['text'])
+```
+
+#### Batch Processing
+
+```python
+proof_states = [
+    "theorem add_zero (n : Nat) : n + 0 = n :::",
+    "theorem mul_one (n : Nat) : n * 1 = n :::",
+    "theorem succ_pred (n : Nat) (h : n ≠ 0) : Nat.succ (Nat.pred n) = n :::"
+]
+
+for state in proof_states:
+    proof = llm(state, max_tokens=512, temperature=0.2)
+    print(f"State: {state}")
+    print(f"Proof: {proof['choices'][0]['text']}\n")
+```
+
+---
+
+## Prompt Format
+
+### Lean4 Proof State Format
+
+The model expects proof states in a specific format with the `:::` delimiter:
+
+```
+<proof_state>:::
+```
+
+### Examples
+
+**Basic Theorem:**
+```lean4
+theorem add_comm (a b : Nat) : a + b = b + a :::
+```
+
+**With Hypotheses:**
+```lean4
+theorem le_trans (a b c : Nat) (hab : a ≤ b) (hbc : b ≤ c) : a ≤ c :::
+```
+
+**Complex Goal:**
+```lean4
+∀ (n m : Nat), n + m = m + n :::
+```
+
+**Proof Tactic Completion:**
+```lean4
+theorem example_thm : 2 + 2 = 4 := by
+  -- Goal: ⊢ 2 + 2 = 4
+  :::
+```
+
+### Response Format
+
+The model generates:
+- **Proof tactics**: `rw [theorem_name]`, `intro`, `apply`, etc.
+- **Complete proofs**: Full proof terms
+- **Proof strategies**: High-level approach descriptions
+- **Tactic suggestions**: Next steps in proof construction
+
+---
+
+## Use Cases
+
+### 1. Interactive Theorem Proving
+
+Assist mathematicians and researchers in constructing formal proofs:
+
+```python
+proof_state = """
+theorem fermat_last_special : ∀ n : Nat, n > 2 → ¬∃ a b c : Nat,
+  a ≠ 0 ∧ b ≠ 0 ∧ c ≠ 0 ∧ a^n + b^n = c^n :::
+"""
+guidance = llm(proof_state, max_tokens=1000)
+```
+
+### 2. Proof Automation
+
+Automatically complete routine proofs:
+
+```python
+simple_proofs = [
+    "theorem add_zero (n : Nat) : n + 0 = n :::",
+    "theorem zero_add (n : Nat) : 0 + n = n :::",
+]
+
+for proof in simple_proofs:
+    completed = llm(proof, temperature=0.1)  # Lower temp for determinism
+```
+
+### 3. Mathematical Education
+
+Help students learn formal proof techniques:
+
+```python
+student_attempt = """
+theorem distributivity (a b c : Nat) : a * (b + c) = a * b + a * c := by
+  -- Student got stuck here
+  :::
+"""
+
+hint = llm(student_attempt, max_tokens=256, temperature=0.3)
+print(f"Hint: {hint}")
+```
+
+### 4. Formalization Projects
+
+Assist in formalizing mathematical theories:
+
+```python
+informal = "Prove that the square root of 2 is irrational"
+formal_state = "theorem sqrt_two_irrational : Irrational (Real.sqrt 2) :::"
+proof_sketch = llm(formal_state, max_tokens=2000)
+```
+
+---
+
+## System Requirements
+
+### Minimum Requirements
+
+| Variant | RAM | GPU VRAM | Storage | CPU |
+|---------|-----|----------|---------|-----|
+| Q4_K_M | 20 GB | Optional | 20 GB | 4+ cores |
+| Q5_K_M | 24 GB | Optional | 25 GB | 4+ cores |
+| F16 | 64 GB | Optional | 65 GB | 8+ cores |
+
+### Recommended Hardware
+
+**For Q5_K_M (Recommended):**
+- **CPU**: 8+ cores (Intel i7/i9, AMD Ryzen 7/9, Apple M1/M2/M3)
+- **RAM**: 32 GB
+- **GPU**: RTX 3090/4090 (24GB VRAM) for GPU acceleration
+- **Storage**: 50 GB SSD
+
+**For GPU Acceleration:**
+- NVIDIA RTX 30/40 series (24GB+ VRAM)
+- Apple Silicon M1 Max/Ultra, M2 Max/Ultra, M3 Max (metal acceleration)
+- AMD Radeon (ROCm support)
+
+---
+
+## Limitations
+
+### Technical Limitations
+
+- **Lean4 Specific**: Optimized for Lean4 syntax; may not generalize to other proof assistants (Coq, Isabelle)
+- **Context Limits**: While 131K context is large, very complex proofs may exceed limits
+- **Quantization Effects**: Lower quantizations (Q4) may reduce proof quality for complex theorems
+- **Inference Speed**: 32B model requires significant compute; expect slower inference than smaller models
+
+### Mathematical Limitations
+
+- **Proof Correctness**: Generated proofs must be verified by Lean4 compiler
+- **Novel Mathematics**: May struggle with cutting-edge research not in training data
+- **Proof Strategies**: Sometimes generates valid but non-optimal proof paths
+- **Notation**: Assumes standard Lean4 notation and libraries
+
+### Practical Considerations
+
+- **Not a Proof Checker**: Always verify generated proofs with Lean4
+- **Requires Domain Knowledge**: Best used by those familiar with formal mathematics
+- **Training Cutoff**: Knowledge limited to training data cutoff date
+- **Computational Cost**: Real-time interactive proving may require GPU acceleration
+
+---
+
+## Performance
+
+### Benchmarks
+
+*Note: Benchmarks are for the base BFS-Prover-V2-32B model. Quantized versions may show minor variations.*
+
+- **MiniF2F**: Strong performance on undergraduate-level math problems
+- **ProofNet**: Effective on formal proof generation tasks
+- **Lean4 Mathlib**: Can leverage and extend mathlib proofs
+
+### Speed Estimates
+
+| Hardware | Variant | Tokens/sec | Use Case |
+|----------|---------|------------|----------|
+| Apple M2 Ultra (192GB) | Q5_K_M | ~15-20 | Interactive proving |
+| RTX 4090 (24GB) | Q5_K_M | ~25-35 | Fast proof generation |
+| CPU Only (32GB RAM) | Q4_K_M | ~5-10 | Batch processing |
+
+---
+
+## Ethical Considerations
+
+### Intended Use
+
+- ✅ Mathematical research and formalization
+- ✅ Educational tools for learning formal methods
+- ✅ Proof automation for routine theorems
+- ✅ Assistance in large formalization projects
+- ✅ Development of formal verification tools
+
+### Out-of-Scope Use
+
+- ❌ Critical system verification without human review
+- ❌ Automated proof generation without verification
+- ❌ Replacing formal proof checkers
+- ❌ Use outside formal mathematics domain
+
+### Responsible Use
+
+- **Always verify proofs** with Lean4 type checker
+- **Human oversight** required for important theorems
+- **Understand limitations** of AI-generated proofs
+- **Credit appropriately** when using in research
+
+---
+
+## Citation
+
+If you use this model in your research, please cite:
+
+```bibtex
+@misc{bfs-prover-v2-32b,
+  title={BFS-Prover-V2-32B: Formal Mathematical Proof Generation},
+  author={ByteDance-Seed Team},
+  year={2024},
+  publisher={Hugging Face},
+  howpublished={\url{https://huggingface.co/ByteDance-Seed/BFS-Prover-V2-32B}}
+}
+
+@misc{bfs-prover-v2-gguf,
+  title={BFS-Prover-V2-32B GGUF Quantization},
+  author={richardyoung},
+  year={2025},
+  publisher={Hugging Face},
+  howpublished={\url{https://huggingface.co/richardyoung/bfs-prover-v2-32b}}
+}
+
+@article{qwen2.5,
+  title={Qwen2.5: A Party of Foundation Models},
+  author={Qwen Team},
+  year={2024}
+}
+```
+
+---
+
+## License
+
+This model is released under the **Apache 2.0 License**, inherited from the base model.
+
+**Permissions:**
+- ✅ Commercial use
+- ✅ Modification
+- ✅ Distribution
+- ✅ Private use
+
+**Conditions:**
+- Include license and copyright notice
+- State changes made to the model
+- Document modifications
+
+**Full License:** [Apache License 2.0](https://www.apache.org/licenses/LICENSE-2.0)
+
+---
+
+## Acknowledgements
+
+### Model Development
+
+- **Original Model**: [ByteDance-Seed Team](https://huggingface.co/ByteDance-Seed) - BFS-Prover-V2-32B
+- **Base Architecture**: [Qwen Team](https://qwenlm.github.io/) - Qwen2.5-32B
+- **Quantization**: richardyoung - GGUF conversions and optimization
+
+### Tools and Frameworks
+
+- **[llama.cpp](https://github.com/ggerganov/llama.cpp)** - GGUF format and inference engine
+- **[Ollama](https://ollama.ai/)** - Easy model deployment and management
+- **[Lean4](https://lean-lang.org/)** - Formal verification language
+- **[Mathlib](https://github.com/leanprover-community/mathlib4)** - Lean4 mathematics library
+
+---
+
+## Additional Resources
+
+### Documentation
+
+- 📖 [Original Model Card](https://huggingface.co/ByteDance-Seed/BFS-Prover-V2-32B)
+- 📚 [Lean4 Documentation](https://lean-lang.org/documentation/)
+- 🔧 [llama.cpp Guide](https://github.com/ggerganov/llama.cpp/blob/master/docs/build.md)
+- 🐋 [Ollama Documentation](https://github.com/ollama/ollama/tree/main/docs)
+
+### Community
+
+- [Lean4 Zulip Chat](https://leanprover.zulipchat.com/)
+- [llama.cpp Discussions](https://github.com/ggerganov/llama.cpp/discussions)
+- [Report Issues](https://huggingface.co/richardyoung/bfs-prover-v2-32b/discussions)
+
+### Related Models
+
+- [ByteDance BFS-Prover-V2-32B (Original)](https://huggingface.co/ByteDance-Seed/BFS-Prover-V2-32B)
+- [Qwen2.5-32B-Instruct](https://huggingface.co/Qwen/Qwen2.5-32B-Instruct)
+- [Other Formal Verification Models](https://huggingface.co/models?other=formal-verification)
+
+---
+
+## Model Card Authors
+
+- **Quantization & Documentation**: richardyoung
+- **Base Model**: ByteDance-Seed Team
+- **Last Updated**: October 2025
+
+---
+
+## Changelog
+
+### Version 1.0 (October 2025)
+- Initial GGUF quantization release
+- Three variants: F16, Q5_K_M, Q4_K_M
+- Ollama Modelfile configurations
+- Comprehensive documentation
+- Lean4-specific prompt format
+
+---
+
+<div align="center">
+
+**Questions or Issues?** [Open a discussion](https://huggingface.co/richardyoung/bfs-prover-v2-32b/discussions)
+
+*Quantized with llama.cpp · Optimized for Formal Mathematics*
+
+</div>