Upload verified REAP full-v3 adapter and value-head snapshot
Browse files- .gitattributes +1 -0
- README.md +91 -0
- backend.json +3 -0
- manifest.json +1 -0
- session.json +1 -0
.gitattributes
CHANGED
|
@@ -33,3 +33,4 @@ saved_model/**/* filter=lfs diff=lfs merge=lfs -text
|
|
| 33 |
*.zip filter=lfs diff=lfs merge=lfs -text
|
| 34 |
*.zst filter=lfs diff=lfs merge=lfs -text
|
| 35 |
*tfevents* filter=lfs diff=lfs merge=lfs -text
|
|
|
|
|
|
| 33 |
*.zip filter=lfs diff=lfs merge=lfs -text
|
| 34 |
*.zst filter=lfs diff=lfs merge=lfs -text
|
| 35 |
*tfevents* filter=lfs diff=lfs merge=lfs -text
|
| 36 |
+
backend.json filter=lfs diff=lfs merge=lfs -text
|
README.md
ADDED
|
@@ -0,0 +1,91 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
---
|
| 2 |
+
license: apache-2.0
|
| 3 |
+
base_model:
|
| 4 |
+
- FrenzyMath/REAL-Prover
|
| 5 |
+
tags:
|
| 6 |
+
- lean4
|
| 7 |
+
- theorem-proving
|
| 8 |
+
- alphaproof
|
| 9 |
+
- reap
|
| 10 |
+
- lora
|
| 11 |
+
- value-head
|
| 12 |
+
- research-artifact
|
| 13 |
+
---
|
| 14 |
+
|
| 15 |
+
# AlphaProof / REAP Full-v3 Value Head
|
| 16 |
+
|
| 17 |
+
Private research artifact for reproducing an AlphaProof-related REAP experiment.
|
| 18 |
+
This repository contains the accepted `full-v3` release snapshot from experience
|
| 19 |
+
`exp-e24fc3c0a20c-01`.
|
| 20 |
+
|
| 21 |
+
## What this repository contains
|
| 22 |
+
|
| 23 |
+
The snapshot transfers two trained components:
|
| 24 |
+
|
| 25 |
+
- a LoRA adapter for the policy model;
|
| 26 |
+
- a categorical 64-bin value head (`linear-3584-silu-256-linear-64`).
|
| 27 |
+
|
| 28 |
+
The artifact is stored in the REAP snapshot format. It is **not** a standalone
|
| 29 |
+
Transformers checkpoint and cannot be loaded directly with
|
| 30 |
+
`AutoModelForCausalLM.from_pretrained(...)`.
|
| 31 |
+
|
| 32 |
+
## Base-model chain
|
| 33 |
+
|
| 34 |
+
- REAP policy/runtime base: [`FrenzyMath/REAL-Prover`](https://huggingface.co/FrenzyMath/REAL-Prover)
|
| 35 |
+
- Pinned REAL-Prover revision: `fe76f68d9a88f342cb7b546307c20292fea9cced`
|
| 36 |
+
- REAL-Prover's upstream language-model base: [`Qwen/Qwen2.5-Math-7B`](https://huggingface.co/Qwen/Qwen2.5-Math-7B)
|
| 37 |
+
- Model class: 7B-class causal language model (the Hugging Face page reports approximately 8B parameters)
|
| 38 |
+
- Hidden size: `3584`
|
| 39 |
+
|
| 40 |
+
In this repository, “REAP 7B base” refers to the pinned REAL-Prover policy base
|
| 41 |
+
used by the REAP experiment. REAP itself is the experiment/search runtime, not a
|
| 42 |
+
separate full 7B checkpoint bundled in this snapshot. The upstream model and its
|
| 43 |
+
declared base model are published under Apache-2.0. Keep the upstream attribution
|
| 44 |
+
when redistributing or publishing derivatives.
|
| 45 |
+
|
| 46 |
+
## Files
|
| 47 |
+
|
| 48 |
+
| File | Purpose | Bytes | SHA-256 |
|
| 49 |
+
|---|---|---:|---|
|
| 50 |
+
| `backend.json` | REAP snapshot containing serialized adapter and value-head weights | 220,477,868 | `becf7c4c6650fca4b11b1087ddd86f4c5dfb69f9b21913bc3f8c81c8f1c37479` |
|
| 51 |
+
| `manifest.json` | File sizes, checksums, schema version and snapshot identity | 324 | included in the manifest |
|
| 52 |
+
| `session.json` | Acceptance evidence and experiment provenance | 983 | `5449e19916008d9d7451d07ef870cb149ddd71693233fdfa3ff1463abf174094` |
|
| 53 |
+
|
| 54 |
+
## Snapshot identity
|
| 55 |
+
|
| 56 |
+
- Schema: `reap.gpu.snapshot.v1`
|
| 57 |
+
- Session / experience: `exp-e24fc3c0a20c-01`
|
| 58 |
+
- Snapshot: `release`
|
| 59 |
+
- Acceptance: completed and passed using independent Lean verification
|
| 60 |
+
- Transferred components: `adapter`, `value_head`
|
| 61 |
+
|
| 62 |
+
## Integrity verification
|
| 63 |
+
|
| 64 |
+
After downloading, verify the main artifact before use:
|
| 65 |
+
|
| 66 |
+
```powershell
|
| 67 |
+
Get-FileHash -Algorithm SHA256 .\backend.json
|
| 68 |
+
```
|
| 69 |
+
|
| 70 |
+
Expected result:
|
| 71 |
+
|
| 72 |
+
```text
|
| 73 |
+
becf7c4c6650fca4b11b1087ddd86f4c5dfb69f9b21913bc3f8c81c8f1c37479
|
| 74 |
+
```
|
| 75 |
+
|
| 76 |
+
## Usage notes
|
| 77 |
+
|
| 78 |
+
Loading requires the matching REAP runtime and the exact upstream model revision.
|
| 79 |
+
The runtime must decode the `torch-save-base64` payload in `backend.json`, attach
|
| 80 |
+
the LoRA adapter to the expected target modules, and restore the categorical
|
| 81 |
+
value head according to the snapshot contract.
|
| 82 |
+
|
| 83 |
+
Do not treat this artifact as a general-purpose chat model or as a complete copy
|
| 84 |
+
of REAL-Prover. The upstream base weights are not bundled here.
|
| 85 |
+
|
| 86 |
+
## Sharing status
|
| 87 |
+
|
| 88 |
+
This repository is intentionally private while experiment provenance, training
|
| 89 |
+
data redistribution conditions, and a clean public loading interface are still
|
| 90 |
+
being reviewed. Organization members should not republish the artifact without
|
| 91 |
+
reviewing those items and preserving upstream attribution.
|
backend.json
ADDED
|
@@ -0,0 +1,3 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
version https://git-lfs.github.com/spec/v1
|
| 2 |
+
oid sha256:becf7c4c6650fca4b11b1087ddd86f4c5dfb69f9b21913bc3f8c81c8f1c37479
|
| 3 |
+
size 220477868
|
manifest.json
ADDED
|
@@ -0,0 +1 @@
|
|
|
|
|
|
|
| 1 |
+
{"files":{"backend.json":{"bytes":220477868,"sha256":"becf7c4c6650fca4b11b1087ddd86f4c5dfb69f9b21913bc3f8c81c8f1c37479"},"session.json":{"bytes":983,"sha256":"5449e19916008d9d7451d07ef870cb149ddd71693233fdfa3ff1463abf174094"}},"schema_version":"reap.gpu.snapshot.v1","session_id":"exp-e24fc3c0a20c-01","snapshot":"release"}
|
session.json
ADDED
|
@@ -0,0 +1 @@
|
|
|
|
|
|
|
| 1 |
+
{"acceptance":{"completed":true,"evidence_sha256":"943821193c38a7a81146dac47c70de2803d567fd573b9f3f964ebe6360f7f5e4","kind":"independent-lean","passed":true,"source":{"parent_experience_id":"exp-c7e2a91d5b40-01","policy_version":1,"session_id":"course-e24fc3c0a20c-01","snapshot":"experience-candidate","snapshot_sha256":"c38054b1641f27c1bde54e5cef633db8f69eda07bd978a6034a9b9e1bc19e72a","theorem_id":"1650a90fbc6f63e2a434c22069cbf33ec87a71a71871832314642b83760205b0"}},"experience_id":"exp-e24fc3c0a20c-01","schema_version":"reap.gpu.experience.v1","source":{"parent_experience_id":"exp-c7e2a91d5b40-01","policy_version":1,"session_id":"course-e24fc3c0a20c-01","snapshot":"experience-candidate","snapshot_sha256":"c38054b1641f27c1bde54e5cef633db8f69eda07bd978a6034a9b9e1bc19e72a","theorem_id":"1650a90fbc6f63e2a434c22069cbf33ec87a71a71871832314642b83760205b0"},"transfer":["adapter","value_head"],"weights_sha256":"becf7c4c6650fca4b11b1087ddd86f4c5dfb69f9b21913bc3f8c81c8f1c37479"}
|