Blame for README.md

---
language:
- en
tags:
- lean
- theorem-proving
- graph-neural-network
- actor-critic
- reinforcement-learning
- mcts
- mathlib
---

# Lean Proof Search — Actor–Critic Checkpoints and Deployment Bundles

This repository hosts versioned checkpoints and matched serving artifacts for
Lean theorem proving with a source-aware graph neural network policy and an
actor–critic reinforcement-learning pipeline.

The application supports PUCT Monte Carlo tree search and best-first search.
Optional Probabilistic Logic Networks (PLN) provide additional search guidance.
Candidate proofs must pass the application's replay and Lean kernel-certification
process before being reported as certified successes.

Application source:
https://github.com/iCog-Labs-Dev/Mathematics-ai-atp/tree/MCTS-AC-branch

## Model architecture

The source-aware policy combines:

- A graph encoder for normalized Lean proof-state expressions.
- A tactic-prediction head.
- An explicit argument-count head.
- A GRU argument decoder.
- A source-selection head that chooses local context or external library
  arguments.
- Local-declaration selection and retrieved-library candidate scoring.
- A critic that estimates proof-state value for reinforcement learning.

External premises are retrieved through a matched text encoder and lemma index.
The policy checkpoint, graph vocabularies, query encoder, lemma vectors, and
declaration inventory must be used as a compatible deployment set.

These checkpoints are used through the project's custom inference and search
code. They are not standalone Transformers text-generation models.

## Training and checkpoint provenance

The supervised initialization supplied for this work used a joint source-aware
policy followed by local-selection refinement. Its matched retrieval artifacts
come from the epoch-5 retriever and index.

Published RL releases may differ in:

- Starting checkpoint and selected final checkpoint.
- Search algorithm: PUCT or best-first.
- Whether PLN guidance was enabled.
- Training rounds, search budgets, and evaluation settings.
- Checkpoint selection: periodic-evaluation best or final saved checkpoint.

Consult each release manifest and accompanying release notes for its identity.
The serving configuration records search settings but is not a complete
training experiment report.

A checkpoint trained using PUCT can also be searched using best-first, provided
the model and runtime interfaces remain compatible. The search algorithm is a
runtime configuration rather than a separate neural-network architecture.

## Repository organization

`main` contains the repository overview. Published serving bundles live on
versioned branches such as `v1.0.0`.

Each release uses this directory structure:

```text
deployments/mcts/<version>/
├── release.json
├── README.md
├── artifacts/
│   ├── checkpoint.pt
│   ├── prepared/
│   ├── query/
│   ├── index/
│   ├── lemmas.jsonl
│   └── declarations.json
└── config/
    ├── rl.json
    └── service.json
```

The `mcts` directory is the deployment format's fixed namespace. It can contain
a release configured for either PUCT or best-first search.

The bundle includes:

| Component | Purpose |
| --- | --- |
| Actor–critic checkpoint | Trained policy and critic parameters, with any retained checkpoint metadata |
| Prepared metadata | Matching graph representation and node/tactic vocabularies |
| Query artifact | Exported query encoder, tokenizer, and configuration |
| Lemma index | FAISS index, vectors, lemma IDs/names, and identity manifests |
| Lemma corpus | Matched external-premise records |
| Declaration inventory | Available Lean declarations, exclusions, and environment identity |
| Serving configuration | Container paths and service/search configuration |
| Release manifest | File sizes, SHA-256 checksums, artifact bindings, and recorded provenance |

Compiled Lean/Mathlib, the custom REPL, Python dependencies, and the PLN runtime
are supplied separately by the compatible application runtime or Docker image.

## Download and verify a release

Use the downloader from the compatible application checkout:

```bash
python -m maths_ai.gnn_inference.scripts.fetch_mcts_deployment \
  --repo iCogLabs-Dev/Lean-Proof-Search-Checkpoints \
  --revision FULL_HUGGING_FACE_RELEASE_COMMIT \
  --version v1.0.0 \
  --manifest-sha256 RELEASE_JSON_SHA256 \
  --output "$HOME/mcts-deployments/v1.0.0"
```

Replace the commit, version, and manifest checksum with the identifiers provided
by the release publisher. Pin the full immutable Hugging Face commit for
reproducible deployment.

The downloader verifies file hashes and model/retrieval bindings. The application
also checks Lean environment compatibility at startup.

A private repository requires Hugging Face authentication with read access.

The downloaded output is a symlink to a persistent sibling backing directory.
Retain both; deleting the backing directory breaks the deployment.

## Serving and evaluation

The application's FastAPI service exposes single-goal proving, dataset
evaluation jobs, and health/readiness checks.

Search profiles select PUCT or best-first search and may enable PLN. Proposal
generation supports greedy or sampled modes where configured.

Docker deployment mounts the verified bundle's `artifacts/` directory at
`/artifacts` and its `config/` directory at `/config`.

See the application deployment guides:

- https://github.com/iCog-Labs-Dev/Mathematics-ai-atp/blob/MCTS-AC-branch/docker/HUGGING_FACE_DEPLOYMENT.md
- https://github.com/iCog-Labs-Dev/Mathematics-ai-atp/blob/MCTS-AC-branch/maths_ai/gnn_inference/docs/mcts_hugging_face_deployment.md

PLN-enabled profiles additionally require the provisioned PeTTa/SWI-Prolog
runtime. PLN scores guide search; they do not replace Lean proof checking.

## Evaluation and interpretation

No aggregate proof-rate improvement is asserted by this model card.

Meaningful comparisons should report:

- Evaluation dataset and exact theorem cohort.
- Base and RL checkpoint identities.
- Search algorithm and proposal mode.
- PLN setting.
- Time, node, depth, simulation, and memory budgets.
- Random seeds.
- Kernel-certified successes and operational failures.

Results from different theorem cohorts or search budgets do not establish a
controlled comparison. Training solve rates should be distinguished from
held-out evaluation results.

## Limitations

- Search is bounded and may fail to find an existing proof.
- Dataset starting states require sufficient Lean context for reconstruction.
- Tactic and argument proposals can be invalid or unsupported.
- Retrieval depends on the supplied corpus and deployed Lean environment.
- A model prediction or graph-level solved candidate is not itself a certified
  proof.
- Certification establishes a proof of the admitted Lean starting statement;
  it does not independently establish that dataset reconstruction preserved the
  intended original theorem.
- Matching runtime artifacts are required; arbitrary REPL or Mathlib replacements
  may invalidate the deployment binding.
- The serving bundle is not a complete training-resume archive.
- Checkpoints may contain optimizer state and other retained training metadata.
  PyTorch checkpoint loading can execute pickle content; load only trusted files.