File size: 3,345 Bytes
c59450c | 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 | ---
license: apache-2.0
base_model:
- FrenzyMath/REAL-Prover
tags:
- lean4
- theorem-proving
- alphaproof
- reap
- lora
- value-head
- research-artifact
---
# AlphaProof / REAP Full-v3 Value Head
Private research artifact for reproducing an AlphaProof-related REAP experiment.
This repository contains the accepted `full-v3` release snapshot from experience
`exp-e24fc3c0a20c-01`.
## What this repository contains
The snapshot transfers two trained components:
- a LoRA adapter for the policy model;
- a categorical 64-bin value head (`linear-3584-silu-256-linear-64`).
The artifact is stored in the REAP snapshot format. It is **not** a standalone
Transformers checkpoint and cannot be loaded directly with
`AutoModelForCausalLM.from_pretrained(...)`.
## Base-model chain
- REAP policy/runtime base: [`FrenzyMath/REAL-Prover`](https://huggingface.co/FrenzyMath/REAL-Prover)
- Pinned REAL-Prover revision: `fe76f68d9a88f342cb7b546307c20292fea9cced`
- REAL-Prover's upstream language-model base: [`Qwen/Qwen2.5-Math-7B`](https://huggingface.co/Qwen/Qwen2.5-Math-7B)
- Model class: 7B-class causal language model (the Hugging Face page reports approximately 8B parameters)
- Hidden size: `3584`
In this repository, “REAP 7B base” refers to the pinned REAL-Prover policy base
used by the REAP experiment. REAP itself is the experiment/search runtime, not a
separate full 7B checkpoint bundled in this snapshot. The upstream model and its
declared base model are published under Apache-2.0. Keep the upstream attribution
when redistributing or publishing derivatives.
## Files
| File | Purpose | Bytes | SHA-256 |
|---|---|---:|---|
| `backend.json` | REAP snapshot containing serialized adapter and value-head weights | 220,477,868 | `becf7c4c6650fca4b11b1087ddd86f4c5dfb69f9b21913bc3f8c81c8f1c37479` |
| `manifest.json` | File sizes, checksums, schema version and snapshot identity | 324 | included in the manifest |
| `session.json` | Acceptance evidence and experiment provenance | 983 | `5449e19916008d9d7451d07ef870cb149ddd71693233fdfa3ff1463abf174094` |
## Snapshot identity
- Schema: `reap.gpu.snapshot.v1`
- Session / experience: `exp-e24fc3c0a20c-01`
- Snapshot: `release`
- Acceptance: completed and passed using independent Lean verification
- Transferred components: `adapter`, `value_head`
## Integrity verification
After downloading, verify the main artifact before use:
```powershell
Get-FileHash -Algorithm SHA256 .\backend.json
```
Expected result:
```text
becf7c4c6650fca4b11b1087ddd86f4c5dfb69f9b21913bc3f8c81c8f1c37479
```
## Usage notes
Loading requires the matching REAP runtime and the exact upstream model revision.
The runtime must decode the `torch-save-base64` payload in `backend.json`, attach
the LoRA adapter to the expected target modules, and restore the categorical
value head according to the snapshot contract.
Do not treat this artifact as a general-purpose chat model or as a complete copy
of REAL-Prover. The upstream base weights are not bundled here.
## Sharing status
This repository is intentionally private while experiment provenance, training
data redistribution conditions, and a clean public loading interface are still
being reviewed. Organization members should not republish the artifact without
reviewing those items and preserving upstream attribution.
|