iCogLabs-Dev/Lean-Proof-Search-Checkpoints

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:

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:

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.