Spaces:
Running
Running
File size: 3,253 Bytes
e9eed22 | 1 | <!doctype html><html lang="en"><head><meta charset="utf-8"><meta name="viewport" content="width=device-width,initial-scale=1"><title>Kakeya OProver Lab</title><link rel="stylesheet" href="styles.css"></head><body><main class="wrap"><header class="hero"><p class="status">PUBLIC SANITIZED RELEASE</p><h1>Kakeya OProver Lab</h1><p>Lean proof training from SFT90 to repair SFT, with matched strict evaluation and explicit non-claims.</p></header><nav class="tabs" aria-label="Report sections"><button data-tab='overview' aria-selected='true'>Overview</button><button data-tab='journey' aria-selected='false'>Training Journey</button><button data-tab='strict' aria-selected='false'>Strict Evaluation</button><button data-tab='metrics' aria-selected='false'>Training Metrics</button><button data-tab='failures' aria-selected='false'>Failure Taxonomy</button><button data-tab='production' aria-selected='false'>Production Qualification</button><button data-tab='jensen' aria-selected='false'>Jensen Result</button><button data-tab='repro' aria-selected='false'>Reproducibility</button><button data-tab='artifacts-panel' aria-selected='false'>Artifacts</button></nav><section class='panel card' id='overview' ><h2>Overview</h2><p id='hero'></p><label for='stage'>Stage selector</label> <select class='select' id='stage'></select><div id='stagecard' class='metric'></div></section><section class='panel card' id='journey' hidden><h2>Training Journey</h2><div class='timeline'><p>SFT90 — establish a small-data baseline.</p><p>SFT1000 — matched validity baseline.</p><p>DPO — preference optimization reduced strict validity.</p><p>Repair SFT — compiler-feedback repair restored quality gates.</p><p>Production alignment — 504/504 converted; 12/12 canary passed.</p></div></section><section class='panel card' id='strict' hidden><h2>Strict Evaluation</h2><ul id='stats'></ul><p class='muted'>Paired comparisons use exact McNemar tests; intervals are exact 95% confidence intervals on rates or discordant-pair win probability.</p></section><section class='panel card' id='metrics' hidden><h2>Training Metrics</h2><p>Loss curves and complete sanitized JSONL metrics are stored in each model repository. Stage selector above links to the source assets.</p></section><section class='panel card' id='failures' hidden><h2>Failure Taxonomy</h2><ul id='taxonomy'></ul><p>Repair SFT targeted executable-proof failures while rehearsing clean Mathlib examples.</p></section><section class='panel card' id='production' hidden><h2>Production Qualification</h2><p id='prod'></p><p>This is a proof-advisor qualification, not authorization for autonomous deployment.</p></section><section class='panel card' id='jensen' hidden><h2>Jensen Result</h2><p id='jensen'></p><p>No candidate proof bodies or production prompts are published.</p></section><section class='panel card' id='repro' hidden><h2>Reproducibility</h2><p>Immutable revisions, adapter hashes, dataset artifact hashes, protocol roots, audit digests, and public/private boundaries are in the bundled release manifest.</p><p id='cost'></p></section><section class='panel card' id='artifacts-panel' hidden><h2>Artifacts</h2><ul id='artifacts'></ul></section></main><script src="app.js"></script></body></html> |