Hugging Face's logo

FluffyAIcode
/
Kakeya-OProver-Stage4-Repair-SFT

Text Generation
PEFT
Safetensors
lean
lean4
theorem-proving
lora
conversational
Model card Files
xet
 Community
Kakeya-OProver-Stage4-Repair-SFT
File size: 4,287 Bytes
8e74b89
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
f8a6cc9
 
 
 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
---
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).