| --- |
| license: apache-2.0 |
| base_model: m-a-p/OProver-8B |
| library_name: peft |
| pipeline_tag: text-generation |
| tags: |
| - lean |
| - lean4 |
| - theorem-proving |
| - lora |
| - peft |
| --- |
| |
| # Kakeya OProver Stage 4 — Repair SFT |
|
|
| > **Status: QUALITY GO / PROOF-ADVISOR-ONLY** |
|
|
| ## Summary |
|
|
| This is an independent PEFT LoRA checkpoint in the Kakeya OProver training journey. It is a proof-advisor research artifact, not an autonomous proof or mathematical truth claim. |
|
|
| ## Training Data |
|
|
| Public data config: [`repair-2800`](https://huggingface.co/datasets/FluffyAIcode/Kakeya-OProver-Training). Artifact SHA-256: `54944619e3625f8a9db88b7c2a84507b86ea1dfc55f43d68f240dd9609244389`. Only Mathlib Apache-2.0 material and explicitly derived training negatives are included; provenance-incomplete OProofs mixtures were excluded. |
|
|
| ## Method |
|
|
| Compile-feedback repair SFT on 2,100 repair examples plus 700 rehearsal examples; validation used 300 repair plus 100 rehearsal examples. |
|
|
| ## Strict Lean Evaluation |
|
|
| All matched Stage2–Stage4 evaluations used 22 tasks (18 holdout + 4 canary), one frozen task order, seed, temperature, token budget, and context policy. Parser rate was 22/22 and unsafe generations were 0 for matched evaluations. |
|
|
| ```json |
| { |
| "status": "QUALITY GO / PROOF-ADVISOR-ONLY", |
| "all22": { |
| "exact": 10, |
| "n": 22, |
| "parser": 22, |
| "unsafe": 0, |
| "ci95": [ |
| 0.2438618659230165, |
| 0.6778952454468283 |
| ] |
| }, |
| "holdout18": { |
| "exact": 6, |
| "n": 18, |
| "ci95": [ |
| 0.13342740250612353, |
| 0.5900747618279255 |
| ] |
| }, |
| "canary4": { |
| "exact": 4, |
| "n": 4, |
| "ci95": [ |
| 0.3976353643835253, |
| 1.0 |
| ] |
| }, |
| "audit_sha256": "f7bc7f2ed5bd09e36dfb67df122334d289269513abca20125b931bdc3202f740", |
| "protocol_root": "6357188c7ecc3541d4b220aa19a5c826cbd81e448ed66cdd5a49b09d17d36c0e", |
| "paired_stage2": { |
| "all22_mcnemar_exact_two_sided_p": 1.0, |
| "interpretation": "Difference not statistically significant." |
| }, |
| "paired_clean_stage3": { |
| "all22_mcnemar_exact_two_sided_p": 0.015625, |
| "holdout18_p": 0.03125, |
| "interpretation": "Stage4 improvement was significant." |
| }, |
| "production_qualification": { |
| "converted": "504/504", |
| "canary": "12/12" |
| }, |
| "jensen": { |
| "status": "SEARCH_EXHAUSTED", |
| "pass_at_6_lean_valid": 0, |
| "rh_proved": false |
| } |
| } |
| ``` |
|
|
| ## Safety |
|
|
| No private chain-of-thought, production prompts, Jensen candidate proof bodies, credentials, or raw candidate-bearing signed audits are published. Stage status constrains use; Stage4 is **PROOF-ADVISOR-ONLY**. |
|
|
| ## Known Failures |
|
|
| 12/22 strict tasks were not exact. Quality gates passed, but the checkpoint is proof-advisor-only. Jensen Pass@6 produced 0 Lean-valid proofs: SEARCH_EXHAUSTED. RH PROVED: NO. |
| |
| ## Intended Use |
| |
| Research on Lean proof suggestion, evaluation, and repair. Every generated proof must be compiled and independently reviewed. Not intended for unsupervised theorem claims or production deployment without separate authorization. |
| |
| ## Reproducibility |
| |
| - Base: [`m-a-p/OProver-8B`](https://huggingface.co/m-a-p/OProver-8B) at `cd9ffd383b584d95bf00e04b88b35b05928b211c` |
| - Immutable source revision: `7dd2e239e0857c6feb585f009e6118c511cc8e17` |
| - Adapter SHA-256: `a24765df00ba8213e0032c10cbcddb242a65ffee937520cea2b61bc0d2d68837` |
| - Dataset artifact SHA-256: `54944619e3625f8a9db88b7c2a84507b86ea1dfc55f43d68f240dd9609244389` |
| - Sanitized machine-readable files: `evaluation/results.json`, `training/metrics.jsonl`, `training/trainer_state.json`, `provenance/manifest.json` |
| - Evaluation/audit digest references are in `evaluation/results.json`; raw candidate-bearing artifacts remain private. |
|
|
| ## Limitations |
|
|
| Small, single-seed strict suites cannot establish broad theorem-proving capability. Exact Lean rates have wide confidence intervals. Stage4 did not significantly outperform Stage2 in the matched paired test. Jensen remained `SEARCH_EXHAUSTED` with 0/6 Lean-valid candidates. **RH PROVED: NO.** |
|
|
| ## Attribution |
|
|
| Base model: m-a-p/OProver-8B (Apache-2.0). Training data derives from Mathlib at `360da6fa66c1273b76b6b2d8c5666fd5ac2e3b56` (Apache-2.0). See `NOTICE`. |
|
|
| ## Release Manifest |
|
|
| The content-addressed public/private boundary and immutable asset references are in [`release-manifest.json`](./blob/main/release-manifest.json). |
|
|
