| --- |
| 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 3 — DPO |
|
|
| > **Status: NO-GO REGRESSION** |
|
|
| ## 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: [`dpo-2000`](https://huggingface.co/datasets/FluffyAIcode/Kakeya-OProver-Training). Artifact SHA-256: `2de80cfbb1c5e14c89611810e02b9f432ec2643a203e4c983cd48b1e6ad919a3`. Only Mathlib Apache-2.0 material and explicitly derived training negatives are included; provenance-incomplete OProofs mixtures were excluded. |
|
|
| ## Method |
|
|
| DPO on 1,400 training pairs and 200 validation pairs; 400 holdout pairs were excluded from training. |
|
|
| ## 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": "NO-GO", |
| "all22": { |
| "corrected_exact": 4, |
| "n": 22, |
| "parser": 22, |
| "unsafe": 0 |
| }, |
| "holdout18": { |
| "corrected_exact": 1, |
| "n": 18 |
| }, |
| "canary4": { |
| "corrected_exact": 3, |
| "n": 4 |
| }, |
| "audit_sha256": "aeb63952d78a132cbe24f4c9238b1c305737c243a51e337c67d5ec08150fe391", |
| "comparison_payload_sha256": "837360593b1fdee9205166cf59d7d091b5992c33a8488d013b3283f6da5b7b8d", |
| "comparison_signature": { |
| "algorithm": "Ed25519", |
| "public_key_base64": "VEQy27ukhgP7vMlIFwRBVYBgXM0RvFXPrOmQ2cnLOmU=", |
| "signature_base64": "ZEVKmswS+H8sLkrVO3ZFi/OftAUACZNn7h4qH7F2EK2cGzniGMisvAtH/n8wziW5xf40/HylwBEh4HqNGrcmDg==" |
| }, |
| "paired_stage2": { |
| "all22_mcnemar_exact_two_sided_p": 0.0625, |
| "holdout18_mcnemar_exact_two_sided_p": 0.125, |
| "interpretation": "Practically material and directionally strong regression, but not conclusive at alpha 0.05." |
| } |
| } |
| ``` |
|
|
| ## 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 |
|
|
| Corrected strict validity regressed to 4/22 overall and 1/18 holdout. The paired Stage2 comparison was directionally strong but not significant at alpha 0.05. |
|
|
| ## 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: `c3b684ce7729ec94305deac4fbc5fd506c7f79a6` |
| - Adapter SHA-256: `064fb996230352ae12fd326944e8c5696edc22c36d34fc710805cb5aa2a3f9e3` |
| - Dataset artifact SHA-256: `2de80cfbb1c5e14c89611810e02b9f432ec2643a203e4c983cd48b1e6ad919a3` |
| - 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). |
|
|
