Spaces:
Running
Running
Add content-addressed release manifest
Browse files- release-manifest.json +74 -165
release-manifest.json
CHANGED
|
@@ -1,183 +1,92 @@
|
|
| 1 |
{
|
| 2 |
"schema_version": 1,
|
| 3 |
"release": "Kakeya OProver public sanitized intermediate results",
|
| 4 |
-
"
|
|
|
|
| 5 |
{
|
| 6 |
-
"
|
| 7 |
-
"
|
| 8 |
-
"
|
| 9 |
-
"
|
| 10 |
-
"
|
| 11 |
-
"
|
| 12 |
-
"adapter_sha256": "0b0770e31ad6e77b33742a5d68dfb48cc0fa67efae4c965aaa6309fd031a9b03",
|
| 13 |
-
"dataset_artifact_sha256": "eacefeab327a0d8c4b66e90b9afe9f7b8eb1df62c87abc9a1166f6b3e5ba8ced",
|
| 14 |
-
"public_private_boundary": {
|
| 15 |
-
"public": [
|
| 16 |
-
"adapter",
|
| 17 |
-
"tokenizer",
|
| 18 |
-
"sanitized metrics/trainer state",
|
| 19 |
-
"aggregate strict evaluation",
|
| 20 |
-
"hashes/signatures/config"
|
| 21 |
-
],
|
| 22 |
-
"private": [
|
| 23 |
-
"chain-of-thought",
|
| 24 |
-
"production prompts",
|
| 25 |
-
"Jensen candidate proof bodies",
|
| 26 |
-
"raw candidate-bearing signed audits",
|
| 27 |
-
"optimizer and RNG checkpoints"
|
| 28 |
-
]
|
| 29 |
-
}
|
| 30 |
},
|
| 31 |
{
|
| 32 |
-
"
|
| 33 |
-
"
|
| 34 |
-
"
|
| 35 |
-
"
|
| 36 |
-
"
|
| 37 |
-
"
|
| 38 |
-
"adapter_sha256": "5e5399518c0741140a14d2cca2fade8ec3eb95fb587139c5c9894d5e297a3b55",
|
| 39 |
-
"dataset_artifact_sha256": "5ebec3f7ed71d0af202924ea9d5ca12a857c5363b89b028dbf74268bf2e32f24",
|
| 40 |
-
"public_private_boundary": {
|
| 41 |
-
"public": [
|
| 42 |
-
"adapter",
|
| 43 |
-
"tokenizer",
|
| 44 |
-
"sanitized metrics/trainer state",
|
| 45 |
-
"aggregate strict evaluation",
|
| 46 |
-
"hashes/signatures/config"
|
| 47 |
-
],
|
| 48 |
-
"private": [
|
| 49 |
-
"chain-of-thought",
|
| 50 |
-
"production prompts",
|
| 51 |
-
"Jensen candidate proof bodies",
|
| 52 |
-
"raw candidate-bearing signed audits",
|
| 53 |
-
"optimizer and RNG checkpoints"
|
| 54 |
-
]
|
| 55 |
-
}
|
| 56 |
},
|
| 57 |
{
|
| 58 |
-
"
|
| 59 |
-
"
|
| 60 |
-
"
|
| 61 |
-
"
|
| 62 |
-
"
|
| 63 |
-
"
|
| 64 |
-
"adapter_sha256": "064fb996230352ae12fd326944e8c5696edc22c36d34fc710805cb5aa2a3f9e3",
|
| 65 |
-
"dataset_artifact_sha256": "2de80cfbb1c5e14c89611810e02b9f432ec2643a203e4c983cd48b1e6ad919a3",
|
| 66 |
-
"public_private_boundary": {
|
| 67 |
-
"public": [
|
| 68 |
-
"adapter",
|
| 69 |
-
"tokenizer",
|
| 70 |
-
"sanitized metrics/trainer state",
|
| 71 |
-
"aggregate strict evaluation",
|
| 72 |
-
"hashes/signatures/config"
|
| 73 |
-
],
|
| 74 |
-
"private": [
|
| 75 |
-
"chain-of-thought",
|
| 76 |
-
"production prompts",
|
| 77 |
-
"Jensen candidate proof bodies",
|
| 78 |
-
"raw candidate-bearing signed audits",
|
| 79 |
-
"optimizer and RNG checkpoints"
|
| 80 |
-
]
|
| 81 |
-
}
|
| 82 |
},
|
| 83 |
{
|
| 84 |
-
"
|
| 85 |
-
"
|
| 86 |
-
"
|
| 87 |
-
"
|
| 88 |
-
"
|
| 89 |
-
"
|
| 90 |
-
|
| 91 |
-
|
| 92 |
-
"
|
| 93 |
-
|
| 94 |
-
|
| 95 |
-
|
| 96 |
-
|
| 97 |
-
|
| 98 |
-
|
| 99 |
-
|
| 100 |
-
"
|
| 101 |
-
|
| 102 |
-
"production prompts",
|
| 103 |
-
"Jensen candidate proof bodies",
|
| 104 |
-
"raw candidate-bearing signed audits",
|
| 105 |
-
"optimizer and RNG checkpoints"
|
| 106 |
-
]
|
| 107 |
}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 108 |
}
|
| 109 |
],
|
| 110 |
-
"
|
| 111 |
-
"
|
| 112 |
-
"
|
| 113 |
-
"
|
| 114 |
-
|
| 115 |
-
|
| 116 |
-
|
| 117 |
-
|
| 118 |
-
|
| 119 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 120 |
],
|
| 121 |
-
"
|
| 122 |
-
"
|
| 123 |
-
|
| 124 |
-
|
| 125 |
-
|
| 126 |
-
"
|
| 127 |
-
|
| 128 |
-
"records": 9
|
| 129 |
-
},
|
| 130 |
-
"sft-90/holdout.jsonl": {
|
| 131 |
-
"sha256": "bfda01582726fe1a99daea87e7a7d1ba86e65526705a6fba8eb9e471df4680ab",
|
| 132 |
-
"records": 18
|
| 133 |
-
},
|
| 134 |
-
"sft-1000/train.jsonl": {
|
| 135 |
-
"sha256": "066b34aafe87c0da820c83781f6254d5c6a363bc93e5e44a65a501d8284885c5",
|
| 136 |
-
"records": 700
|
| 137 |
-
},
|
| 138 |
-
"sft-1000/validation.jsonl": {
|
| 139 |
-
"sha256": "804214d63ca01ad7abf3b2931147dc43057f6b2e7449480286cc89860ab592da",
|
| 140 |
-
"records": 100
|
| 141 |
-
},
|
| 142 |
-
"sft-1000/holdout.jsonl": {
|
| 143 |
-
"sha256": "7befdd6831a2b1e62a89b871022391565c0e965d83c2c9eac3f08741a37e8978",
|
| 144 |
-
"records": 200
|
| 145 |
-
},
|
| 146 |
-
"dpo-2000/train.jsonl": {
|
| 147 |
-
"sha256": "0e2a0a15d7ff03b5347a2e91da83c6c6d85539a44746c1d2d9662bc3e8ddde29",
|
| 148 |
-
"records": 1400
|
| 149 |
-
},
|
| 150 |
-
"dpo-2000/validation.jsonl": {
|
| 151 |
-
"sha256": "e478670e03df4af61532cf5954b06135816a2c7e8ea2bfab3e7109bac229c51c",
|
| 152 |
-
"records": 200
|
| 153 |
-
},
|
| 154 |
-
"dpo-2000/holdout.jsonl": {
|
| 155 |
-
"sha256": "1c97353d19ffe60dd436888123750c1d7f05a34445644ae8ad6f6ab23931c5f9",
|
| 156 |
-
"records": 400
|
| 157 |
-
},
|
| 158 |
-
"repair-2800/train.jsonl": {
|
| 159 |
-
"sha256": "1d4224ce24a29ec1069b8f56a0cb24598cc8c945ed0dfb74544428c4f5fba9d1",
|
| 160 |
-
"records": 2800
|
| 161 |
-
},
|
| 162 |
-
"repair-2800/validation.jsonl": {
|
| 163 |
-
"sha256": "f2a82d37dadf8a37fc20175339c9eea8ad0af91b7f2d32b3476a5a4abb90a6a6",
|
| 164 |
-
"records": 400
|
| 165 |
-
}
|
| 166 |
-
},
|
| 167 |
-
"excluded": [
|
| 168 |
-
"OProofs mixed/provenance-incomplete samples",
|
| 169 |
-
"production Jensen prompts and candidates",
|
| 170 |
-
"private reasoning and raw candidate-bearing audits"
|
| 171 |
]
|
| 172 |
},
|
| 173 |
-
"
|
| 174 |
-
|
| 175 |
-
|
| 176 |
-
"
|
| 177 |
-
"private": "Original private repositories, private chain-of-thought, production prompts, Jensen candidate proof bodies, raw candidate-bearing signed audits, optimizer/RNG checkpoints."
|
| 178 |
},
|
| 179 |
-
"
|
| 180 |
-
"file_count": 86,
|
| 181 |
-
"secret_scan_hits": 0
|
| 182 |
-
}
|
| 183 |
}
|
|
|
|
| 1 |
{
|
| 2 |
"schema_version": 1,
|
| 3 |
"release": "Kakeya OProver public sanitized intermediate results",
|
| 4 |
+
"generated_utc": "2026-08-08T07:45:00Z",
|
| 5 |
+
"assets": [
|
| 6 |
{
|
| 7 |
+
"repo": "FluffyAIcode/Kakeya-OProver-Stage1-SFT90",
|
| 8 |
+
"type": "model",
|
| 9 |
+
"url": "https://huggingface.co/FluffyAIcode/Kakeya-OProver-Stage1-SFT90",
|
| 10 |
+
"content_revision": "41e157c52fc9c818b6bb9223f1bf9eb9f31e2343",
|
| 11 |
+
"public": true,
|
| 12 |
+
"adapter_lfs_sha256": "0b0770e31ad6e77b33742a5d68dfb48cc0fa67efae4c965aaa6309fd031a9b03"
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 13 |
},
|
| 14 |
{
|
| 15 |
+
"repo": "FluffyAIcode/Kakeya-OProver-Stage2-SFT1000",
|
| 16 |
+
"type": "model",
|
| 17 |
+
"url": "https://huggingface.co/FluffyAIcode/Kakeya-OProver-Stage2-SFT1000",
|
| 18 |
+
"content_revision": "dc75d2b4f89ed26fac223e227aa43c80f342e165",
|
| 19 |
+
"public": true,
|
| 20 |
+
"adapter_lfs_sha256": "5e5399518c0741140a14d2cca2fade8ec3eb95fb587139c5c9894d5e297a3b55"
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 21 |
},
|
| 22 |
{
|
| 23 |
+
"repo": "FluffyAIcode/Kakeya-OProver-Stage3-DPO",
|
| 24 |
+
"type": "model",
|
| 25 |
+
"url": "https://huggingface.co/FluffyAIcode/Kakeya-OProver-Stage3-DPO",
|
| 26 |
+
"content_revision": "3103783b4faf788abcd6033fe681282a42845f8e",
|
| 27 |
+
"public": true,
|
| 28 |
+
"adapter_lfs_sha256": "064fb996230352ae12fd326944e8c5696edc22c36d34fc710805cb5aa2a3f9e3"
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 29 |
},
|
| 30 |
{
|
| 31 |
+
"repo": "FluffyAIcode/Kakeya-OProver-Stage4-Repair-SFT",
|
| 32 |
+
"type": "model",
|
| 33 |
+
"url": "https://huggingface.co/FluffyAIcode/Kakeya-OProver-Stage4-Repair-SFT",
|
| 34 |
+
"content_revision": "8e74b89c24733d657b11fa9ba6f36f629b050f94",
|
| 35 |
+
"public": true,
|
| 36 |
+
"adapter_lfs_sha256": "a24765df00ba8213e0032c10cbcddb242a65ffee937520cea2b61bc0d2d68837"
|
| 37 |
+
},
|
| 38 |
+
{
|
| 39 |
+
"repo": "FluffyAIcode/Kakeya-OProver-Training",
|
| 40 |
+
"type": "dataset",
|
| 41 |
+
"url": "https://huggingface.co/datasets/FluffyAIcode/Kakeya-OProver-Training",
|
| 42 |
+
"content_revision": "11f42344657d3be95e7cc553d7070a1da9619de2",
|
| 43 |
+
"public": true,
|
| 44 |
+
"artifact_sha256": {
|
| 45 |
+
"sft-90": "eacefeab327a0d8c4b66e90b9afe9f7b8eb1df62c87abc9a1166f6b3e5ba8ced",
|
| 46 |
+
"sft-1000": "5ebec3f7ed71d0af202924ea9d5ca12a857c5363b89b028dbf74268bf2e32f24",
|
| 47 |
+
"dpo-2000": "2de80cfbb1c5e14c89611810e02b9f432ec2643a203e4c983cd48b1e6ad919a3",
|
| 48 |
+
"repair-2800": "54944619e3625f8a9db88b7c2a84507b86ea1dfc55f43d68f240dd9609244389"
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 49 |
}
|
| 50 |
+
},
|
| 51 |
+
{
|
| 52 |
+
"repo": "FluffyAIcode/Kakeya-OProver-Lab",
|
| 53 |
+
"type": "space",
|
| 54 |
+
"url": "https://huggingface.co/spaces/FluffyAIcode/Kakeya-OProver-Lab",
|
| 55 |
+
"content_revision": "e9eed2215cdd5b82b11c1b80db960622fc65314d",
|
| 56 |
+
"public": true
|
| 57 |
}
|
| 58 |
],
|
| 59 |
+
"base_model": {
|
| 60 |
+
"repo": "m-a-p/OProver-8B",
|
| 61 |
+
"revision": "cd9ffd383b584d95bf00e04b88b35b05928b211c",
|
| 62 |
+
"license": "apache-2.0"
|
| 63 |
+
},
|
| 64 |
+
"mathlib": {
|
| 65 |
+
"repo": "leanprover-community/mathlib4",
|
| 66 |
+
"revision": "360da6fa66c1273b76b6b2d8c5666fd5ac2e3b56",
|
| 67 |
+
"license": "apache-2.0"
|
| 68 |
+
},
|
| 69 |
+
"public_private_boundary": {
|
| 70 |
+
"public": [
|
| 71 |
+
"LoRA adapters and tokenizers",
|
| 72 |
+
"approved Mathlib datasets and derived negatives",
|
| 73 |
+
"sanitized trainer state and metrics",
|
| 74 |
+
"aggregate evaluations",
|
| 75 |
+
"hashes, signatures, configs, and failure summaries"
|
| 76 |
],
|
| 77 |
+
"private": [
|
| 78 |
+
"original private source repositories",
|
| 79 |
+
"chain-of-thought",
|
| 80 |
+
"production prompts",
|
| 81 |
+
"Jensen candidate proof bodies",
|
| 82 |
+
"raw candidate-bearing signed audits",
|
| 83 |
+
"optimizer and RNG checkpoints"
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 84 |
]
|
| 85 |
},
|
| 86 |
+
"collection": {
|
| 87 |
+
"title": "Kakeya OProver \u2014 Lean Proof Training Journey",
|
| 88 |
+
"status": "BLOCKED_ORG_COLLECTION_CREATE_403",
|
| 89 |
+
"personal_namespace_fallback": false
|
|
|
|
| 90 |
},
|
| 91 |
+
"manifest_sha256": "8a60f51ff96aeab35454ab8d129393aa6892a7b539117f8c1a36430d25d138e1"
|
|
|
|
|
|
|
|
|
|
| 92 |
}
|