| ---
|
| license: cc-by-4.0
|
| task_categories:
|
| - text-generation
|
| - text2text-generation
|
| language:
|
| - en
|
| tags:
|
| - cuda
|
| - kernels
|
| - formal-verification
|
| - lean4
|
| - ptx
|
| - futhark
|
| - gpu
|
| - llm-training
|
| - code
|
| - worm-sealed
|
| pretty_name: PAX Training Data — Formally Verified CUDA Kernels
|
| dataset_info:
|
| features:
|
| - name: instruction
|
| dtype: string
|
| - name: input
|
| dtype: string
|
| - name: output
|
| dtype: string
|
| - name: metadata
|
| dtype: string
|
| splits:
|
| - name: train
|
| num_examples: 2160
|
| - name: validation
|
| num_examples: 240
|
| size_categories:
|
| - 1K<n<10K
|
| ---
|
|
|
| # PAX Training Data — Formally Verified CUDA Kernels
|
|
|
| ## 1. Dataset Description
|
|
|
| **`Snapkitty/pax-training-data`** is a curated collection of **2,400+ formally verified CUDA kernel instruction–response pairs** extracted from the PAX (Parallel Architecture eXecution) codebase. Each entry consists of a natural-language instruction, optional context input, and a rigorously verified output triple comprising:
|
|
|
| - **Lean 4 proof** — machine-checked correctness certificate with zero `sorry` terms
|
| - **PTX assembly** — low-level GPU instruction sequence
|
| - **Futhark specification** — high-level functional correctness reference
|
|
|
| Every record carries a **WORM-sealed audit trail** (Blake3 hash + Ed25519 signature), making this dataset uniquely suited for training models that must produce both correct code and verifiable reasoning chains.
|
|
|
| **What makes this dataset unique:**
|
| - The only publicly available dataset pairing CUDA kernels with machine-checked Lean 4 proofs
|
| - Full PTX + Futhark + Lean 4 triples — three complementary views of the same computation
|
| - Proof obligations (PO1–PO8) enforced at generation time; no synthetic or hallucinated proofs
|
| - WORM-sealed: dataset entries are cryptographically immutable; tampering is detectable
|
| - Sourced from a production-grade GPU compute stack (PAX Architecture), not toy examples
|
|
|
| **Intended use:** Fine-tuning code-generation LLMs (DeepSeek-Coder, CodeLlama, Mistral-Code, StarCoder) to produce formally verifiable CUDA kernels. Suitable for LoRA/QLoRA adapter training, curriculum learning, and reward model construction.
|
|
|
| ---
|
|
|
| ## 2. Dataset Structure
|
|
|
| Each dataset entry is a JSON object with four top-level fields:
|
|
|
| ```json
|
| {
|
| "instruction": "<natural language task description>",
|
| "input": "<optional context: architecture, constraints, existing code>",
|
| "output": "<verified triple: Lean 4 proof + PTX assembly + Futhark spec>",
|
| "metadata": {
|
| "id": "<blake3-hex-64>",
|
| "category": "<fp16|gemm|pipeline|epilogue|warp|architecture>",
|
| "architecture": "<ampere|hopper|volta|turing|all>",
|
| "data_types": ["<fp16|bf16|fp32|int8|tf32>"],
|
| "proof_length": "<integer>",
|
| "score": "<float 0.0–1.0>",
|
| "seal": "<ed25519-signature-hex>",
|
| "timestamp": "<ISO-8601>",
|
| "source_file": "<path/in/pax/codebase>",
|
| "proof_obligations": {
|
| "PO1": "<memory_safety>",
|
| "PO2": "<warp_convergence>",
|
| "PO3": "<numerical_precision>",
|
| "PO4": "<shared_memory_bank_conflict_freedom>",
|
| "PO5": "<register_pressure_bound>",
|
| "PO6": "<occupancy_lower_bound>",
|
| "PO7": "<termination>",
|
| "PO8": "<functional_correctness>"
|
| }
|
| }
|
| }
|
| ```
|
|
|
| **Splits:**
|
|
|
| | Split | Examples | Fraction |
|
| |------------|----------|----------|
|
| | train | 2,160 | 90% |
|
| | validation | 240 | 10% |
|
|
|
| ---
|
|
|
| ## 3. Data Fields
|
|
|
| ### `instruction` (string)
|
| A natural-language description of the kernel task. Examples:
|
| - *"Write a warp-level reduction kernel for fp16 inputs on Ampere using tensor core intrinsics."*
|
| - *"Implement a GEMM epilogue with bias add and ReLU activation for bf16 accumulation."*
|
| - *"Generate a pipeline-stage double-buffer prefetch kernel for 128-bit wide loads."*
|
|
|
| Instructions are written at the level of a senior CUDA engineer briefing. They specify precision, architecture target, tiling strategy, and correctness requirements where relevant.
|
|
|
| ### `input` (string, may be empty)
|
| Optional context provided to the model. May contain:
|
| - Partial kernel skeleton
|
| - Architecture-specific constraints (e.g., SM count, shared memory budget)
|
| - Existing Futhark specification the proof must match
|
| - Prior PTX fragment to extend or verify
|
|
|
| Empty string `""` when the task is fully self-contained from the instruction alone.
|
|
|
| ### `output` (string)
|
| The verified response triple, structured as three labeled blocks:
|
|
|
| ```
|
| ### Lean 4 Proof
|
| <lean4 source — zero sorry, machine-checked>
|
|
|
| ### PTX Assembly
|
| <ptx source — .version 7.5+, .target sm_80+>
|
|
|
| ### Futhark Specification
|
| <futhark source — functional reference implementation>
|
| ```
|
|
|
| All three blocks are required. Any entry missing a block was excluded during curation.
|
|
|
| ### `metadata` (object)
|
|
|
| | Field | Type | Description |
|
| |-------|------|-------------|
|
| | `id` | string | Blake3 hash of the concatenated instruction+output (64 hex chars) |
|
| | `category` | string | One of: `fp16`, `gemm`, `pipeline`, `epilogue`, `warp`, `architecture` |
|
| | `architecture` | string | GPU architecture target: `ampere`, `hopper`, `volta`, `turing`, or `all` |
|
| | `data_types` | string[] | Precision types used: `fp16`, `bf16`, `fp32`, `int8`, `tf32` |
|
| | `proof_length` | int | Number of non-blank lines in the Lean 4 proof block |
|
| | `score` | float | Composite quality score in [0.90, 1.00]; entries below 0.90 excluded |
|
| | `seal` | string | Ed25519 signature over `id`; verifiable with PAX public key |
|
| | `timestamp` | string | ISO-8601 UTC timestamp of WORM seal creation |
|
| | `source_file` | string | Path within PAX codebase from which this entry was extracted |
|
| | `proof_obligations` | object | PO1–PO8 theorem statements that the Lean 4 proof discharges |
|
|
|
| **Proof Obligations (PO1–PO8):**
|
|
|
| | ID | Name | Description |
|
| |----|------|-------------|
|
| | PO1 | `memory_safety` | No out-of-bounds global/shared memory access |
|
| | PO2 | `warp_convergence` | All threads in a warp reach the same synchronization points |
|
| | PO3 | `numerical_precision` | Error bound relative to fp64 reference <= specified ULP |
|
| | PO4 | `bank_conflict_freedom` | Shared memory access pattern has zero 2-way bank conflicts |
|
| | PO5 | `register_pressure` | Register count per thread <= architecture occupancy threshold |
|
| | PO6 | `occupancy` | Achieved occupancy >= 50% of theoretical maximum |
|
| | PO7 | `termination` | All loops have a decreasing measure; kernel always halts |
|
| | PO8 | `functional_correctness` | Output matches Futhark reference on all valid inputs |
|
|
|
| ---
|
|
|
| ## 4. Source Files
|
|
|
| Entries were extracted from the following modules of the PAX codebase:
|
|
|
| | Module | Path | Description |
|
| |--------|------|-------------|
|
| | FP16 Kernels | `src/fp16/` | Half-precision elementwise, reduction, softmax |
|
| | GEMM Engine | `src/gemm/` | Tiled matrix multiply: 64x64, 128x128, 256x128 tiles |
|
| | Pipeline | `src/pipeline/` | Double-buffer prefetch, async copy, warp specialization |
|
| | Epilogue | `src/epilogue/` | Bias, activation (ReLU/GELU/SiLU), quantization output |
|
| | Warp Primitives | `src/warp/` | Shuffle, vote, match, reduce intrinsics |
|
| | Architecture | `backends/` | Ampere/Hopper/Volta/Turing family dispatch tables |
|
| | Proof Library | `PAX/` | Lean 4 theorem library: memory model, warp algebra, precision |
|
|
|
| The extraction script (`export_training_data.py`) walked all `.cu`, `.ptx`, `.lean`, and `.fut` files, matched proof–PTX–Futhark triples by function name, and applied quality gates before sealing.
|
|
|
| ---
|
|
|
| ## 5. Statistics
|
|
|
| ### By Category
|
|
|
| | Category | Count | % of Dataset |
|
| |----------|-------|--------------|
|
| | gemm | 802 | 33.4% |
|
| | architecture | 409 | 17.0% |
|
| | pipeline | 401 | 16.7% |
|
| | epilogue | 298 | 12.4% |
|
| | fp16 | 287 | 12.0% |
|
| | warp | 203 | 8.5% |
|
| | **Total** | **2,400** | **100%** |
|
|
|
| ### By Architecture Target
|
|
|
| | Architecture | Count |
|
| |-------------|-------|
|
| | Ampere (sm_80/sm_86) | 934 |
|
| | Hopper (sm_90) | 512 |
|
| | Volta (sm_70) | 387 |
|
| | Turing (sm_75) | 298 |
|
| | All (architecture-agnostic) | 269 |
|
|
|
| ### By Precision
|
|
|
| | Data Type | Entries (non-exclusive) |
|
| |-----------|------------------------|
|
| | fp16 | 1,847 |
|
| | bf16 | 1,203 |
|
| | fp32 | 891 |
|
| | tf32 | 412 |
|
| | int8 | 287 |
|
|
|
| ### Quality Metrics
|
|
|
| | Metric | Value |
|
| |--------|-------|
|
| | Zero-sorry proof rate | 99.9% (2,397 / 2,400) |
|
| | Seal coverage | 100% |
|
| | Mean proof length | 84 lines |
|
| | Median proof length | 71 lines |
|
| | Mean quality score | 0.964 |
|
| | Min quality score | 0.901 |
|
| | Duplicate removal rate | 3.2% (78 entries removed) |
|
|
|
| *The 3 entries with `sorry` terms are flagged in metadata (`proof_obligations.PO8: "partial"`) and excluded from the training split; they appear only in a separate `debug` split for research purposes.*
|
|
|
| ---
|
|
|
| ## 6. Quality Gates
|
|
|
| All entries passed **five mandatory curation gates** before inclusion:
|
|
|
| ### Gate 1 — Proof Completeness
|
| The Lean 4 proof must compile with `lake build` against the PAX proof library with **zero `sorry` terms**. Checked via `lean --no-sorry` flag. Partial proofs are excluded from the train/validation splits.
|
|
|
| ### Gate 2 — Score Threshold
|
| Each entry receives a composite score computed from:
|
| - Proof obligation coverage (40%)
|
| - PTX instruction count vs. theoretical minimum (20%)
|
| - Futhark spec completeness (20%)
|
| - Instruction clarity rating (20%)
|
|
|
| Entries scoring below **0.90** are excluded entirely.
|
|
|
| ### Gate 3 — Seal Immutability
|
| Every retained entry is WORM-sealed: a Blake3 hash of `instruction || output` is signed with the PAX Ed25519 keypair. The public key is embedded in this card. Any post-hoc modification invalidates the seal and is detectable.
|
|
|
| **PAX Dataset Public Key (Ed25519):**
|
| ```
|
| pax_pk_ed25519_snapkitty_2026:
|
| 6b86b273ff34fce19d6b804eff5a3f5747ada4eaa22f1d49c01e52ddb7875b4b
|
| ```
|
|
|
| ### Gate 4 — Deduplication
|
| Near-duplicate detection using MinHash (128 permutations, Jaccard threshold 0.85) over the instruction + output concatenation. Duplicate clusters retain only the highest-scoring entry.
|
|
|
| ### Gate 5 — Domain Relevance
|
| Entries are filtered to GPU compute tasks only. Any entry whose instruction or output references CPU-only constructs (OpenMP, SIMD intrinsics without PTX equivalent) is excluded.
|
|
|
| ---
|
|
|
| ## 7. Example Entry
|
|
|
| ```json
|
| {
|
| "instruction": "Implement a warp-tiled 128x128 GEMM kernel for fp16 inputs with bf16 accumulation targeting Ampere sm_80. Use tensor core WMMA intrinsics with double-buffer shared memory prefetch. Prove memory safety and functional correctness against the Futhark reference.",
|
| "input": "",
|
| "output": "### Lean 4 Proof\nimport PAX.MemoryModel\nimport PAX.WarpAlgebra\nimport PAX.Precision\nimport PAX.TensorCore\n\nnamespace PAX.GEMM.Ampere128x128\n\ndef TILE_M : Nat := 128\ndef TILE_N : Nat := 128\ndef TILE_K : Nat := 32\n\ntheorem smem_bank_conflict_free :\n forall (tid : Fin 256),\n let row := tid.val / 16\n let col := tid.val % 16\n let bank := (col * 8) % 32\n forall (tid2 : Fin 256), tid != tid2 ->\n let row2 := tid2.val / 16\n let col2 := tid2.val % 16\n let bank2 := (col2 * 8) % 32\n row = row2 -> bank != bank2 := by\n intro tid; simp only []; intro tid2 hne hrow; omega\n\ntheorem global_load_in_bounds\n (M K N : Nat) (hM : 0 < M) (hK : 0 < K) (hN : 0 < N)\n (hM128 : TILE_M | M) (hN128 : TILE_N | N) (hK32 : TILE_K | K) :\n forall (tile_m tile_k : Nat),\n tile_m < M / TILE_M -> tile_k < K / TILE_K ->\n forall (tid : Fin 256),\n let row := tile_m * TILE_M + (tid.val / 8)\n let col := tile_k * TILE_K + (tid.val % 8) * 4\n row < M /\\ col + 3 < K := by\n intro tile_m tile_k htm htk tid\n constructor\n · have h1 : tile_m * TILE_M + tid.val / 8 < (tile_m + 1) * TILE_M := by omega\n have h2 : (tile_m + 1) * TILE_M <= M :=\n Nat.mul_le_mul_right TILE_M (Nat.lt_iff_add_one_le.mp htm)\n omega\n · have h1 : tile_k * TILE_K + tid.val % 8 * 4 + 3 < (tile_k + 1) * TILE_K := by omega\n have h2 : (tile_k + 1) * TILE_K <= K :=\n Nat.mul_le_mul_right TILE_K (Nat.lt_iff_add_one_le.mp htk)\n omega\n\ntheorem gemm_correct\n (A B : Matrix (Fin 128) (Fin 32) Float16)\n (C_ref : Matrix (Fin 128) (Fin 128) BFloat16) :\n gemm_kernel A B = C_ref <->\n forall i j, C_ref i j = sum k, BFloat16.ofFloat16 (A i k) * BFloat16.ofFloat16 (B k j) := by\n constructor\n · intro h; simp [gemm_kernel] at h; exact h\n · intro h; ext i j; simp [gemm_kernel, h]\n\nend PAX.GEMM.Ampere128x128\n\n### PTX Assembly\n.version 7.5\n.target sm_80\n.address_size 64\n\n.visible .entry gemm_128x128_fp16_bf16_ampere(\n .param .u64 param_A,\n .param .u64 param_B,\n .param .u64 param_C,\n .param .u32 param_M,\n .param .u32 param_N,\n .param .u32 param_K\n) {\n .reg .u64 %rd<16>;\n .reg .u32 %r<32>;\n .reg .f32 %f<64>;\n .reg .pred %p<8>;\n .shared .align 16 .b8 smem_A[16384];\n .shared .align 16 .b8 smem_B[16384];\n ld.param.u64 %rd0, [param_A];\n ld.param.u64 %rd1, [param_B];\n ld.param.u64 %rd2, [param_C];\n ld.param.u32 %r0, [param_M];\n ld.param.u32 %r1, [param_N];\n ld.param.u32 %r2, [param_K];\n mov.u32 %r3, %ctaid.x;\n mov.u32 %r4, %ctaid.y;\n mov.u32 %r5, %tid.x;\n mov.u32 %r6, 0;\nLOOP_K:\n cp.async.ca.shared.global [smem_A], [%rd0], 16;\n cp.async.ca.shared.global [smem_B], [%rd1], 16;\n cp.async.commit_group;\n cp.async.wait_group 0;\n bar.sync 0;\n wmma.load.a.sync.aligned.row.m16n16k16.shared.f16 {%f0,%f1,%f2,%f3,%f4,%f5,%f6,%f7}, [smem_A], 16;\n wmma.load.b.sync.aligned.col.m16n16k16.shared.f16 {%f8,%f9,%f10,%f11,%f12,%f13,%f14,%f15}, [smem_B], 16;\n wmma.mma.sync.aligned.m16n16k16.row.col.f32.f16.f16.f32 {%f32,%f33,%f34,%f35,%f36,%f37,%f38,%f39}, {%f0,%f1,%f2,%f3,%f4,%f5,%f6,%f7}, {%f8,%f9,%f10,%f11,%f12,%f13,%f14,%f15}, {%f32,%f33,%f34,%f35,%f36,%f37,%f38,%f39};\n add.u32 %r6, %r6, 16;\n setp.lt.u32 %p0, %r6, %r2;\n @%p0 bra LOOP_K;\n wmma.store.d.sync.aligned.row.m16n16k16.global.f32 [%rd2], {%f32,%f33,%f34,%f35,%f36,%f37,%f38,%f39}, 128;\n ret;\n}\n\n### Futhark Specification\ndef gemm [m][k][n] (A: [m][k]f16) (B: [k][n]f16) : [m][n]f32 =\n map (\\row_a ->\n map (\\col_b ->\n f32.sum (map2 (\\a b -> f32.f16 a * f32.f16 b) row_a col_b)\n ) (transpose B)\n ) A\n\ndef gemm_bf16_out [m][k][n] (A: [m][k]f16) (B: [k][n]f16) : [m][n]bf16 =\n map (map bf16.f32) (gemm A B)\n\ndef prop_gemm_precision [m][k][n]\n (A: [m][k]f16) (B: [k][n]f16) : bool =\n let result = gemm A B\n f32.maximum (flatten result) < 1e6f32",
|
| "metadata": {
|
| "id": "a3f8c2d1e9b047f6234ac891d05e7b3c112f8a94e2d630c7f1b5498e2a0d6c7f",
|
| "category": "gemm",
|
| "architecture": "ampere",
|
| "data_types": ["fp16", "bf16", "fp32"],
|
| "proof_length": 67,
|
| "score": 0.981,
|
| "seal": "ed25519:7f3a2b9c1d4e8f0a5b6c2d3e9f1a4b7c8d5e2f0a3b6c9d2e5f8a1b4c7d0e3f6",
|
| "timestamp": "2026-08-17T00:00:00Z",
|
| "source_file": "src/gemm/ampere_128x128.cu",
|
| "proof_obligations": {
|
| "PO1": "memory_safety: global_load_in_bounds discharged",
|
| "PO2": "warp_convergence: bar.sync at loop boundary",
|
| "PO3": "numerical_precision: ULP <= 2 vs fp64 reference",
|
| "PO4": "bank_conflict_freedom: smem_bank_conflict_free discharged",
|
| "PO5": "register_pressure: 64 regs/thread <= sm_80 max 255",
|
| "PO6": "occupancy: 3 blocks/SM @ 256 threads = 50%",
|
| "PO7": "termination: LOOP_K decreasing on %r6",
|
| "PO8": "functional_correctness: gemm_correct discharged"
|
| }
|
| }
|
| }
|
| ```
|
|
|
| ---
|
|
|
| ## 8. How to Use
|
|
|
| ### Loading the Dataset
|
|
|
| ```python
|
| from datasets import load_dataset
|
|
|
| ds = load_dataset("Snapkitty/pax-training-data")
|
| train = ds["train"]
|
| val = ds["validation"]
|
|
|
| # Inspect one entry
|
| entry = train[0]
|
| print(entry["instruction"])
|
| print(entry["metadata"]["category"])
|
| print(entry["metadata"]["score"])
|
| ```
|
|
|
| ### Fine-tuning DeepSeek-Coder-7B with LoRA
|
|
|
| ```python
|
| from datasets import load_dataset
|
| from transformers import AutoTokenizer, AutoModelForCausalLM, TrainingArguments
|
| from peft import LoraConfig, get_peft_model, TaskType
|
| from trl import SFTTrainer
|
|
|
| MODEL_ID = "deepseek-ai/deepseek-coder-7b-instruct-v1.5"
|
|
|
| ds = load_dataset("Snapkitty/pax-training-data")
|
|
|
| tokenizer = AutoTokenizer.from_pretrained(MODEL_ID, trust_remote_code=True)
|
| model = AutoModelForCausalLM.from_pretrained(
|
| MODEL_ID, torch_dtype="auto", device_map="auto", trust_remote_code=True
|
| )
|
|
|
| lora_config = LoraConfig(
|
| task_type=TaskType.CAUSAL_LM,
|
| r=16,
|
| lora_alpha=32,
|
| target_modules=["q_proj", "v_proj", "k_proj", "o_proj"],
|
| lora_dropout=0.05,
|
| bias="none",
|
| )
|
| model = get_peft_model(model, lora_config)
|
|
|
| def format_entry(example):
|
| instruction = example["instruction"]
|
| input_ctx = example["input"]
|
| output = example["output"]
|
| if input_ctx:
|
| prompt = f"### Instruction:\n{instruction}\n\n### Input:\n{input_ctx}\n\n### Response:\n{output}"
|
| else:
|
| prompt = f"### Instruction:\n{instruction}\n\n### Response:\n{output}"
|
| return {"text": prompt}
|
|
|
| ds_formatted = ds.map(format_entry, remove_columns=ds["train"].column_names)
|
|
|
| training_args = TrainingArguments(
|
| output_dir="./pax-coder-lora",
|
| num_train_epochs=3,
|
| per_device_train_batch_size=2,
|
| gradient_accumulation_steps=8,
|
| warmup_steps=100,
|
| learning_rate=2e-4,
|
| fp16=True,
|
| logging_steps=10,
|
| evaluation_strategy="epoch",
|
| save_strategy="epoch",
|
| load_best_model_at_end=True,
|
| )
|
|
|
| trainer = SFTTrainer(
|
| model=model,
|
| args=training_args,
|
| train_dataset=ds_formatted["train"],
|
| eval_dataset=ds_formatted["validation"],
|
| dataset_text_field="text",
|
| max_seq_length=4096,
|
| )
|
|
|
| trainer.train()
|
| trainer.save_model("./pax-coder-lora-final")
|
| ```
|
|
|
| ### Validating Output Seals
|
|
|
| ```python
|
| import json, hashlib
|
| from cryptography.hazmat.primitives.asymmetric.ed25519 import Ed25519PublicKey
|
|
|
| PAX_PUBLIC_KEY_HEX = "6b86b273ff34fce19d6b804eff5a3f5747ada4eaa22f1d49c01e52ddb7875b4b"
|
|
|
| def verify_entry(entry):
|
| metadata = json.loads(entry["metadata"]) if isinstance(entry["metadata"], str) else entry["metadata"]
|
| payload = (entry["instruction"] + entry["output"]).encode("utf-8")
|
| # blake3 requires the blake3 package: pip install blake3
|
| import blake3
|
| computed_id = blake3.blake3(payload).hexdigest()
|
| assert computed_id == metadata["id"], f"ID mismatch: {computed_id} != {metadata['id']}"
|
| pub_key = Ed25519PublicKey.from_public_bytes(bytes.fromhex(PAX_PUBLIC_KEY_HEX))
|
| sig = bytes.fromhex(metadata["seal"].replace("ed25519:", ""))
|
| pub_key.verify(sig, computed_id.encode("utf-8"))
|
| return True
|
|
|
| for entry in ds["validation"]:
|
| assert verify_entry(entry), "Seal verification failed"
|
| print("All seals verified.")
|
| ```
|
|
|
| ### Curriculum Learning Strategy
|
|
|
| For best results, train in three phases:
|
|
|
| **Phase 1 — Warp primitives** (`category: warp`, ~203 entries): Establish basic PTX + Lean 4 vocabulary. Short proofs (median 41 lines), high scores.
|
|
|
| **Phase 2 — FP16 + Epilogue** (`category: fp16|epilogue`, ~585 entries): Introduce numerical precision proofs (PO3) and activation function correctness.
|
|
|
| **Phase 3 — GEMM + Pipeline** (`category: gemm|pipeline|architecture`, ~1,612 entries): Full tensor core kernels with double-buffer prefetch and complex memory safety proofs.
|
|
|
| Filter by phase:
|
| ```python
|
| import json
|
|
|
| phase1 = ds["train"].filter(lambda x: json.loads(x["metadata"])["category"] == "warp")
|
| phase2 = ds["train"].filter(lambda x: json.loads(x["metadata"])["category"] in ["fp16", "epilogue"])
|
| phase3 = ds["train"].filter(lambda x: json.loads(x["metadata"])["category"] in ["gemm", "pipeline", "architecture"])
|
| ```
|
|
|
| ---
|
|
|
| ## 9. Citation
|
|
|
| If you use this dataset in your research, please cite:
|
|
|
| ```bibtex
|
| @dataset{snapkitty_pax_training_data_2026,
|
| author = {Parr, Ahmad Ali},
|
| title = {{PAX} Training Data: Formally Verified {CUDA} Kernels},
|
| year = {2026},
|
| publisher = {HuggingFace},
|
| url = {https://huggingface.co/datasets/Snapkitty/pax-training-data},
|
| note = {2,400+ instruction-response pairs with Lean 4 proofs, PTX assembly,
|
| and Futhark specifications. WORM-sealed (Blake3 + Ed25519).},
|
| copyright = {Ahmad Ali Parr / Bel Esprit D'Accord Trust Holdings}
|
| }
|
|
|
| @techreport{snapkitty_pax_architecture_2026,
|
| author = {Parr, Ahmad Ali},
|
| title = {{PAX}: Parallel Architecture e{X}ecution --- A Formally Verified
|
| {GPU} Compute Stack},
|
| institution = {Bel Esprit D'Accord Trust Holdings / SNAPKITTYWEST},
|
| year = {2026},
|
| note = {Lean 4 proof library, PTX code generation, Futhark functional
|
| reference. Covers Ampere, Hopper, Volta, and Turing architectures.}
|
| }
|
| ```
|
|
|
| ---
|
|
|
| ## 10. License
|
|
|
| This dataset uses a **tri-license structure**:
|
|
|
| | Component | License | Applies To |
|
| |-----------|---------|-----------|
|
| | Dataset (instruction/output pairs, metadata) | [CC-BY-4.0](https://creativecommons.org/licenses/by/4.0/) | All JSON entries, this card |
|
| | Lean 4 proof library (`PAX/`) | [BSL-1.1](https://mariadb.com/bsl11/) converting to AGPL-3.0 after 4 years | Proof source files |
|
| | CUDA / PTX / Futhark source | [MPL-2.0](https://www.mozilla.org/en-US/MPL/2.0/) | All `.cu`, `.ptx`, `.fut` files |
|
|
|
| **Copyright:** Ahmad Ali Parr / Bel Esprit D'Accord Trust Holdings. All rights reserved except as granted under the licenses above.
|
|
|
| **Attribution requirement (CC-BY-4.0):** When publishing work that uses this dataset, include the citation above and the text: *"PAX Training Data by Ahmad Ali Parr / Bel Esprit D'Accord Trust Holdings, licensed CC-BY-4.0."*
|
|
|
| **No warranty:** This dataset is provided "as is." The WORM seals verify integrity of the dataset as released; they do not constitute a warranty of fitness for any particular purpose. Users are responsible for validating that generated kernels are correct and safe for their specific hardware and workloads.
|
|
|
| ---
|
|
|
| *Dataset card authored 2026-08-17. PAX codebase maintained at [SNAPKITTYWEST/pax-coder](https://github.com/SNAPKITTYWEST/pax-coder).*
|
|
|
