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