README.md

---
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.