docs/SOVEREIGN_NVIDIA_TRAINING_GUIDE.md

Sovereign NVIDIA Training Guide

How SnapKitty trains NVIDIA's own model on NVIDIA's own hardware to produce verified NVIDIA kernels.

---

Why Nemotron + NVIDIA Megatron

Most AI code generators are trained on GitHub scrapes and hope for the best. We took a different approach:

Decision	Why
NVIDIA Nemotron as base model	Nemotron was built by NVIDIA. Its internal weights already encode CUDA semantics, PTX instruction behavior, tensor core data paths, and memory hierarchy. We don't teach it NVIDIA — it already is NVIDIA.
NVIDIA Megatron as training framework	Megatron-LM is NVIDIA's own distributed training framework. Tensor parallelism, pipeline parallelism, sequence parallelism — all designed for NVIDIA hardware by NVIDIA engineers.
RTX 3080 / RTX 4090 as target hardware	We generate kernels for the same GPUs we train on. The model writes PTX for the machine it runs on.
PAX formal verification as training signal	Every training example is a proven-correct kernel. The model learns what correct GPU code looks like because it only ever sees correct GPU code.

The result: a model that writes NVIDIA GPU kernels with mathematical correctness proofs attached, trained by NVIDIA's framework on NVIDIA's hardware using NVIDIA's model.

No external dependencies. No cloud APIs. Sovereign compute.

---

The Stack (All NVIDIA, All the Way Down)

┌────────────────────────────────────────────────────────────────────┐
│                    SNAPKITTY SOVEREIGN COMPUTE                      │
├────────────────────────────────────────────────────────────────────┤
│                                                                    │
│   Model:      NVIDIA Nemotron 70B                                  │
│   Framework:  NVIDIA Megatron-LM (tensor + pipeline parallelism)   │
│   Hardware:   NVIDIA RTX 3080 (sm_86) / RTX 4090 (sm_89)          │
│   ISA:        NVIDIA PTX (mma.sync, cp.async, ldmatrix, TMA)       │
│   Proofs:     Lean 4 (verified against NVIDIA hardware model)      │
│   Inference:  Deterministic (temperature=0.0, top_k=1)             │
│                                                                    │
│   Every layer is NVIDIA.                                           │
│   Every kernel is proven.                                          │
│   Every output is deterministic.                                   │
│                                                                    │
└────────────────────────────────────────────────────────────────────┘

---

Hardware Targets

SnapKitty maintains verified kernel libraries for multiple NVIDIA architectures:

RTX 3080 — Ampere (sm_86)

Architecture:  Ampere
Compute:       sm_86
VRAM:          10 GB GDDR6X (760 GB/s)
Tensor Cores:  3rd gen
Key PTX:       mma.sync.aligned.m16n8k8.row.col.f32.f16.f16.f32
Async Copy:    cp.async.ca.shared.global + commit/wait groups
Pipeline:      3-stage (proven overlap bound: 1 - 1/3 = 66.7% utilization floor)

Verified kernels:

• rtx_gemm_wmma.cu — WMMA reference (128x128x32 CTA tiles)
• rtx_gemm_ptx.cu — Raw PTX mma.sync with ldmatrix
• rtx_gemm_pipeline.cu — 3-stage async pipeline with proven throughput
• rtx_gemm_epilogue.cu — Fused Bias+GeLU / Residual+GeLU epilogues

RTX 4090 — Ada Lovelace (sm_89)

Architecture:  Ada Lovelace
Compute:       sm_89
VRAM:          24 GB GDDR6X (1008 GB/s)
Tensor Cores:  4th gen
Key PTX:       cp.async.bulk.tensor (TMA — Tensor Memory Accelerator)
Cluster:       __cluster_dims__ + barrier.cluster.* + multicast TMA
Pipeline:      4+ stage (TMA enables deeper overlap)

Verified kernels:

• rtx_gemm_tma.cu — TMA cluster algebra with multicast
• Cluster coherence invariant: forall c in cluster. TMA_load(c) -> visible(c') within 1 cycle
• Multicast law: TMA_multicast(mask, T) = XOR_{c in mask} TMA_unicast(c, T)

What This Means for You

You tell PAX-Coder which GPU you have. It generates a kernel targeting exactly that architecture — not a generic CUDA kernel that might work, but a PTX-level implementation proven correct for your specific hardware.

# RTX 3080 (sm_86) — cp.async pipeline, no TMA
ollama run pax-coder "Write a verified GEMM for sm_86 with 3-stage pipeline"

# RTX 4090 (sm_89) — TMA cluster, deep pipeline
ollama run pax-coder "Write a verified GEMM for sm_89 with TMA multicast"

---

Training Nemotron with Megatron-LM

Why This Combination Works

Nemotron 70B already understands:

• CUDA memory hierarchy (global → L2 → shared → registers)
• PTX instruction semantics (what mma.sync actually computes)
• Tensor core data layouts (row-major A, column-major B, m16n8k8 fragments)
• Warp-level primitives (shfl.sync, vote.sync, match.sync)

We're not teaching a generic language model what CUDA is. We're taking NVIDIA's own model — which already has CUDA baked into its weights — and fine-tuning it to produce formally verified NVIDIA code.

The fine-tuning signal is the PAX corpus: ~2,400 verified triples of (Lean 4 proof, PTX kernel, Futhark spec). After training, the model doesn't just write CUDA — it writes proven-correct CUDA.

Training Configuration

# Megatron-LM config for Nemotron PAX fine-tuning
model:
  name: nvidia/nemotron-70b-instruct
  tensor_parallel_size: 4
  pipeline_parallel_size: 2
  sequence_length: 4096
  
training:
  micro_batch_size: 1
  global_batch_size: 64
  learning_rate: 1.5e-5
  min_learning_rate: 1.0e-6
  lr_warmup_steps: 100
  lr_decay_style: cosine
  weight_decay: 0.01
  clip_grad: 1.0
  bf16: true
  
data:
  dataset: pax-verified-corpus
  format: nemotron_chat_template
  categories:
    - fp16_rounding      # IEEE-754 binary16 proofs
    - gemm_kernels       # mma.sync implementations
    - pipeline_overlap   # cp.async throughput bounds
    - epilogue_fusion    # Bias+GeLU algebraic laws
    - warp_primitives    # shfl.sync reductions
    - architecture       # PAX axiom mappings

loss:
  type: po_weighted_cross_entropy
  weights:
    lean4_proof: 2.0     # Proof correctness is highest priority
    ptx_kernel: 1.5      # Implementation correctness
    futhark_spec: 1.0    # Spec adherence
    certificate: 0.5     # PO tagging

inference:
  temperature: 0.0       # Deterministic — proofs don't have "creative" answers
  top_k: 1
  repetition_penalty: 1.0

The PO-Weighted Loss Function

Standard cross-entropy treats every token equally. We weight proof tokens higher than comment tokens:

L = -sum_i w(category_i) * log P(token_i | context)

Where:
  w(lean4_proof)  = 2.0  — getting a theorem wrong is unacceptable
  w(ptx_kernel)   = 1.5  — implementation must match the proof
  w(futhark_spec) = 1.0  — spec is the reference
  w(certificate)  = 0.5  — tagging is secondary

This produces a model that prioritizes correctness over style.

Deterministic Generation

PAX-Coder runs at temperature 0.0 with top_k=1. There is no sampling, no creativity, no stochastic variation.

Why: A proof is either correct or it isn't. 2 + 2 = 4 every time. A model generating formal proofs must be deterministic.

# Inference — zero entropy
output = model.generate(
    input_ids,
    temperature=0.0,
    top_k=1,
    top_p=1.0,
    repetition_penalty=1.0,
    do_sample=False,
    max_new_tokens=2048
)

Same input → same kernel → same proof. Every time.

---

Training on RTX 3080 (Single GPU)

For the public PAX-Coder (7B, based on DeepSeek-Coder), single-GPU training fits on the RTX 3080:

# VRAM budget — RTX 3080 10GB:
#   Base model (4-bit QLoRA)  ~4.2 GB
#   LoRA adapters (r=32)     ~0.1 GB
#   Gradients (8-bit paged)  ~1.5 GB
#   Activations (GC)         ~1.8 GB
#   Dataset buffer           ~0.5 GB
#   Total                    ~8.1 GB (1.9 GB headroom)

# One command:
./run_training.sh

# What it does:
#   1. Checks free VRAM (needs ~8GB)
#   2. Extracts training data from PAX corpus → JSONL
#   3. Fine-tunes DeepSeek-Coder-7B with QLoRA
#   4. Exports to GGUF for Ollama
#   5. ~4-6 hours on RTX 3080

Full Nemotron 70B (Multi-GPU)

The full sovereign Nemotron model requires distributed training via Megatron-LM:

# Multi-node launch (4× A100 80GB or 8× RTX 4090 24GB)
torchrun \
  --nproc_per_node=4 \
  --nnodes=1 \
  --master_port=29500 \
  pretrain_gpt.py \
  --tensor-model-parallel-size 4 \
  --pipeline-model-parallel-size 1 \
  --num-layers 80 \
  --hidden-size 8192 \
  --num-attention-heads 64 \
  --seq-length 4096 \
  --micro-batch-size 1 \
  --global-batch-size 64 \
  --lr 1.5e-5 \
  --train-iters 2000 \
  --bf16 \
  --data-path pax-verified-corpus \
  --save checkpoints/nemotron-pax \
  --load nvidia/nemotron-70b-instruct

---

What Makes This Sovereign

Property	What it means
No cloud dependency	Runs on local NVIDIA hardware. No API keys, no rate limits, no vendor lock-in.
No trust dependency	Every output is machine-checked. You don't trust the model — you verify its proofs.
No data dependency	Training corpus is self-generated from the PAX codebase. Not GitHub scrapes.
Deterministic	Same prompt → same output. Auditable, reproducible, provable.
Hardware-native	Model writes for the GPU it runs on. No abstraction layers. Raw PTX.

This is what sovereign compute means: you own the hardware, you own the model, you own the training data, and you can verify every output.

---

Custom NVIDIA Builds

SnapKitty offers custom kernel builds targeting your specific NVIDIA hardware:

What You Get

┌──────────────────────────────────────────────────────┐
│  YOUR GPU → PAX-Coder generates:                     │
│                                                      │
│  1. Lean 4 correctness proof (zero sorry)            │
│  2. PTX kernel targeting YOUR sm_XX arch             │
│  3. Futhark functional spec (ground truth)           │
│  4. PAX certificate (which POs are satisfied)        │
│  5. NCU-ready binary (compile + profile)             │
│                                                      │
│  Not generic CUDA. YOUR hardware. PROVEN correct.    │
└──────────────────────────────────────────────────────┘

Supported Architectures

GPU	Architecture	Compute	Key Feature	Status
RTX 3080	Ampere	sm_86	cp.async 3-stage pipeline	Verified
RTX 3090	Ampere	sm_86	Same as 3080 + 24GB VRAM	Verified
RTX 4090	Ada Lovelace	sm_89	TMA + cluster multicast	Verified
A100	Ampere	sm_80	Async copy + large shared	Verified
H100	Hopper	sm_90	TMA + warp specialization	Spec complete

How to Order

# 1. Tell us your GPU
echo "RTX 4090" | pax-coder --target sm_89

# 2. Tell us your computation
echo "128x128 GEMM with Residual+GeLU epilogue, FP16 in, FP32 accum"

# 3. Get back:
#    - verified_gemm_sm89.ptx    (your kernel)
#    - verified_gemm_sm89.lean   (your proof)
#    - verified_gemm_sm89.fut    (your spec)
#    - CERTIFICATE.json          (PO1-PO8 status)

---

The Competitive Advantage

	Generic Code Models	cuBLAS	PAX-Coder
Correctness	Hope-based	Tested, not proven	Machine-checked proof
Hardware targeting	Generic CUDA	Black box	Architecture-specific PTX
Reproducibility	Temperature sampling	Deterministic	Deterministic + auditable
Verification	None	Benchmarks	Lean 4 formal proof
Customization	Prompt engineering	Library calls	Fine-tuned for YOUR arch
Sovereignty	Cloud API	Proprietary	Runs on YOUR GPU

---

Repo Structure (PAX-Coder)

pax-coder/
├── PAX/                        Lean 4 formal proofs (training source)
├── src/
│   ├── rtx_gemm_ptx.cu        sm_86 GEMM — raw mma.sync
│   ├── rtx_gemm_pipeline.cu   sm_86 3-stage async — proven overlap
│   ├── rtx_gemm_epilogue.cu   sm_86 Bias+GeLU fusion — proven bounds
│   └── pax_kernel.fut         Futhark functional spec
├── demo/
│   ├── demo.py                Live inference demo
│   └── showcase_examples.jsonl Example prompts + outputs
├── docs/
│   ├── PAX_ARCHITECTURE.md    5 axioms → 8 proof obligations
│   └── SOVEREIGN_NVIDIA_TRAINING_GUIDE.md   (this file)
├── train.py                   QLoRA fine-tuning (RTX 3080 single-GPU)
├── export_training_data.py    PAX corpus → JSONL extraction
├── run_training.sh            One-command training launcher
├── Modelfile                  Ollama deployment
├── LICENSE.tri                BSL-1.1 / AGPL-3.0 / MPL-2.0
└── SOVEREIGN_NODE_KEY.md      Production access

---

Getting Started

Option 1: Use PAX-Coder directly (pre-trained, public)

ollama pull Snapkitty/pax-coder
ollama run pax-coder "Write a verified GEMM for my RTX 3080"

Option 2: Train your own PAX model on your NVIDIA GPU

git clone https://github.com/SNAPKITTYWEST/pax-coder
cd pax-coder
./run_training.sh  # ~4-6h on RTX 3080

Option 3: Custom sovereign build (enterprise)

Contact licensing@snapkittywest.dev for:

• Architecture-specific kernel libraries
• On-premises Nemotron deployment
• Formal verification consulting
• Custom PO audits

---

License

Tri-licensed: BSL-1.1 / AGPL-3.0 / MPL-2.0

Copyright (C) 2026 Bel Esprit D'Accord Irrevocable Trust SnapKitty Collective Limited

Authors: Ahmad Ali Parr — Jessica Westerhoff