File size: 4,607 Bytes
ef6eb55 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 | # About PAX-Coder
## What PAX-Coder Does
PAX-Coder is a fine-tuned AI model (based on DeepSeek-Coder-7B) that generates GPU kernels paired with formal proofs. You ask it to write a kernel, and it gives you:
1. **Lean 4 proof** — A mathematical proof that your kernel is correct
2. **PTX assembly** — The actual GPU code that runs on NVIDIA sm_86 hardware (RTX 3080, RTX 4090)
3. **Futhark reference** — A high-level functional specification to verify against
4. **PAX certificate** — Which safety guarantees this kernel provides
## For Whom
- **GPU engineers** who want to ship kernels with formal guarantees
- **CUDA developers** who want to skip manual proof-writing
- **Research labs** building verified AI infrastructure
- **Companies** shipping safety-critical ML models where "trust me bro" is not acceptable
## What Makes It Different
Most GPU kernel generators output code you hope is correct. PAX-Coder outputs code + a machine-checked proof that it IS correct. The proof can be read by any Lean 4 compiler and verified independently—no human judgment required.
## Key Topics
### 🎯 Getting Started
- **No prerequisites needed** — Read [User Guide](#user-guide) in the README
- **30 seconds**: Run via Ollama (pre-installed model)
- **3 minutes**: Run via Python (HuggingFace transformers)
- **30 minutes**: Train your own version locally
### 🔧 What You Can Ask For
- IEEE-754 floating-point proofs (rounding error bounds)
- GEMM kernels (matrix multiply)
- Async copy pipelines (3-stage, double-buffer)
- Epilogue fusion (Bias+GeLU, Residual+GeLU)
- Warp reductions (shfl.sync)
- Architecture mappings (axioms → proof obligations)
### 📋 What You Get
Every output includes:
- **Lean 4**: Machine-checked theorem (zero `sorry` placeholders)
- **PTX**: sm_86 assembly for RTX 3080 / RTX 4090
- **Futhark**: Functional spec (compiler-verified semantics)
- **Certificate**: Which of 8 proof obligations this satisfies
### 🏗️ The Five Axioms (Math Foundation)
1. **Index Space Primacy** — Each thread owns one element; proven partition
2. **Permission Necessity** — Every memory access has a fractional permission; sum ≤ 1
3. **Synchronization as State** — Barriers are happens-before edges
4. **Warp Distinctness** — SIMT reconvergence proven before barriers
5. **Verification Non-Negotiability** — No kernel ships without proof
These map to 8 proof obligations (PO1–PO8) that codify GPU safety.
### 🎓 Training
You can train your own version:
```bash
python3 export_training_data.py # Extract proofs + code
./run_training.sh # QLoRA fine-tune (4-6h on RTX 3080)
ollama create pax-coder -f Modelfile
```
### 📜 License
Tri-licensed (BSL-1.1, AGPL-3.0, MPL-2.0). Use the Prolog reasoner to determine which license applies to your use case.
### 🔑 Sovereign Node Key
Production use requires a Sovereign Node Key — proof you've contributed to the stack. Not DRM; community membership. See [`SOVEREIGN_NODE_KEY.md`](SOVEREIGN_NODE_KEY.md).
## The Repository
| Folder | Purpose |
|--------|---------|
| `PAX/` | Lean 4 formal proofs (ConstraintDAG, PipelineDAG, Float16_Rounding, WMMA, IR_DAG) |
| `src/` | GPU kernel templates (PTX + Futhark specs) |
| `backends/` | License policy reasoner (Prolog) |
| `docs/` | Documentation (architecture, user guide, GTM) |
| `demo/` | Interactive examples |
## Key Files
- **[README.md](README.md)** — This document + quickstart + user guide
- **[USER_GUIDE.md](docs/USER_GUIDE.md)** — Step-by-step usage examples
- **[PAX_ARCHITECTURE.md](docs/PAX_ARCHITECTURE.md)** — 5 axioms → 8 proof obligations
- **[PAX_CODER_README.md](PAX_CODER_README.md)** — Commercial integration (GGUF, CUDA, PTX, GEMM bridge)
- **[SOVEREIGN_NODE_KEY.md](SOVEREIGN_NODE_KEY.md)** — How to get a node key
- **[LICENSE.tri](LICENSE.tri)** — Full tri-license text
## Hardware Support
| GPU | Architecture | Status |
|-----|--------------|--------|
| RTX 3080 | Ampere (sm_86) | Primary target ✅ |
| RTX 4090 | Ada (sm_90) | Secondary (TMA support planned) |
## Quick Links
- **Use it now**: [User Guide](#user-guide) in README
- **Examples**: `demo/` folder
- **Architecture details**: [PAX_ARCHITECTURE.md](docs/PAX_ARCHITECTURE.md)
- **Commercial integration**: [PAX_CODER_README.md](PAX_CODER_README.md)
- **Contribute**: [CONTRIBUTING.md](CONTRIBUTING.md)
---
**TL;DR**: Write English prose asking for a GPU kernel. PAX-Coder generates proof + code. Ship with confidence.
|