Add serving release v1.0.1

.gitattributes

@@ -33,3 +33,7 @@ saved_model/**/* filter=lfs diff=lfs merge=lfs -text
 *.zip filter=lfs diff=lfs merge=lfs -text
 *.zst filter=lfs diff=lfs merge=lfs -text
 *tfevents* filter=lfs diff=lfs merge=lfs -text
+deployments/mcts/v1.0.1/artifacts/declarations.json filter=lfs diff=lfs merge=lfs -text
+deployments/mcts/v1.0.1/artifacts/index/faiss.index filter=lfs diff=lfs merge=lfs -text
+deployments/mcts/v1.0.1/artifacts/index/lemma_names.json filter=lfs diff=lfs merge=lfs -text
+deployments/mcts/v1.0.1/artifacts/lemmas.jsonl filter=lfs diff=lfs merge=lfs -text

deployments/mcts/v1.0.1/README.md

@@ -0,0 +1,7 @@
+# MCTS serving release v1.0.1
+
+Mount artifacts/ at /artifacts and config/ at /config.
+The exact REPL binary and compiled Mathlib must match declarations.json.
+Lean, Python, the custom client and PLN runtimes are supplied by the image.
+Checkpoint loading uses pickle; use only releases from trusted publishers.
+This is a serving bundle, not a complete training-resume archive.

deployments/mcts/v1.0.1/artifacts/checkpoint.pt

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:61b218f60bf03678f84b4f00891a592cea46c9e689fe915454b4db2a3595dd21
+size 15746933

deployments/mcts/v1.0.1/artifacts/declarations.json

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:6d7e1c1ee94833a5142b3eacbdfe9119a8b4c658a15a0e2f564fd1381386add2
+size 60345840

deployments/mcts/v1.0.1/artifacts/index/deployment_manifest.json

@@ -0,0 +1,24 @@
+{
+  "corpus_sha256": "e418af465e7d07af48cb64fa6533d8370f386e75f78ae278b1c39aa9ed4d57e9",
+  "environment_identity": "73901041f16e8b5c28da6db5334ad985556b6dd6a06ece77623f9190aec6e8c4",
+  "files": {
+    "faiss.index": "48027f9cd8dbe1b705b3ec21ae2b2d1752d933e7bf5bdf78c88fb410fe2d61ca",
+    "lemma_ids.json": "2c7764a082d0062f6b5dde65efbfef2e1867b90dfe5080339ceb7305b80fc0cd",
+    "lemma_names.json": "196cab04618821d79f937167995cbe0dd8696313390926734b46ecc9062024cc",
+    "lemma_vectors.npy": "05a6ef64c252cb542ad069f58cec40860300374a44bb0dc2828f7ac6c3f0a60e",
+    "manifest.json": "78f668e3ee4e37738192dea1a7bae02ca5c135a753a59e88e97a680e7f718701"
+  },
+  "query_encoder_sha256": "3f5a62b9f49423be4d2ae29030fe68b4ea71ccadf7229ad82ecc3771ef47c0a3",
+  "schema": "lemma_serving_v1",
+  "source_manifest": {
+    "corpus_sha256": "e418af465e7d07af48cb64fa6533d8370f386e75f78ae278b1c39aa9ed4d57e9",
+    "lemma_encoder_sha256": "58a5278d01f2b438e8beba05e38dd50d8af10e25539e84a4706e015953c3319a",
+    "max_length": 192,
+    "model_name": "sentence-transformers/all-MiniLM-L6-v2",
+    "model_type": "pretrained_text_dual_encoder_index_v1",
+    "normalize": true,
+    "state_text_policy": "goal_first_v1",
+    "tokenizer_sha256": "4d340ba6df0d188a0bc2fdae2f8f4279427ea92d4c2457be7ae8fa149027d0b4"
+  },
+  "text_checkpoint_sha256": "777e1c91ca3a0baa567df805ddf73c236450bc9d6623f15067efcc5ad669dae8"
+}

deployments/mcts/v1.0.1/artifacts/index/faiss.index

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:48027f9cd8dbe1b705b3ec21ae2b2d1752d933e7bf5bdf78c88fb410fe2d61ca
+size 489911853

deployments/mcts/v1.0.1/artifacts/index/lemma_names.json

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:196cab04618821d79f937167995cbe0dd8696313390926734b46ecc9062024cc
+size 11807120

deployments/mcts/v1.0.1/artifacts/index/lemma_vectors.npy

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:05a6ef64c252cb542ad069f58cec40860300374a44bb0dc2828f7ac6c3f0a60e
+size 489911936

deployments/mcts/v1.0.1/artifacts/index/manifest.json

@@ -0,0 +1,10 @@
+{
+  "corpus_sha256": "e418af465e7d07af48cb64fa6533d8370f386e75f78ae278b1c39aa9ed4d57e9",
+  "lemma_encoder_sha256": "58a5278d01f2b438e8beba05e38dd50d8af10e25539e84a4706e015953c3319a",
+  "max_length": 192,
+  "model_name": "sentence-transformers/all-MiniLM-L6-v2",
+  "model_type": "pretrained_text_dual_encoder_index_v1",
+  "normalize": true,
+  "state_text_policy": "goal_first_v1",
+  "tokenizer_sha256": "4d340ba6df0d188a0bc2fdae2f8f4279427ea92d4c2457be7ae8fa149027d0b4"
+}

deployments/mcts/v1.0.1/artifacts/lemmas.jsonl

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:e418af465e7d07af48cb64fa6533d8370f386e75f78ae278b1c39aa9ed4d57e9
+size 137254943

deployments/mcts/v1.0.1/artifacts/prepared/metadata/graph_representation.json

@@ -0,0 +1,6 @@
+{
+  "representation": "lean-model-sexp-v2",
+  "model_sexp_version": 1,
+  "graph_schema_version": 1,
+  "hypothesis_schema": "fv-name-role-type-v1"
+}

deployments/mcts/v1.0.1/artifacts/prepared/vocab/tactic_vocab.json

@@ -0,0 +1,217 @@
+{
+  ".": 1,
+  "<UNK_TACTIC>": 0,
+  "C_simp": 2,
+  "abel": 3,
+  "abel_nf": 4,
+  "ac_rfl": 5,
+  "aesop": 6,
+  "aesop_cat": 7,
+  "aesop_mat": 8,
+  "all_goals": 9,
+  "apply": 10,
+  "apply_assumption": 11,
+  "apply_fun": 12,
+  "apply_mod_cast": 13,
+  "apply_rules": 14,
+  "assumption": 15,
+  "assumption_mod_cast": 16,
+  "beta_reduce": 17,
+  "bitwise_assoc_tac": 18,
+  "borelize": 19,
+  "by_cases": 20,
+  "by_contra": 21,
+  "by_contra!": 22,
+  "calc": 23,
+  "cancel_denoms": 24,
+  "case": 25,
+  "cases": 26,
+  "cases'": 27,
+  "change": 28,
+  "choose": 29,
+  "choose!": 30,
+  "classical": 31,
+  "clear": 32,
+  "clear!": 33,
+  "clear_value": 34,
+  "coherence": 35,
+  "compute_degree": 36,
+  "compute_degree!": 37,
+  "congr": 38,
+  "congr!": 39,
+  "congrm": 40,
+  "constructor": 41,
+  "continuity": 42,
+  "contradiction": 43,
+  "contrapose": 44,
+  "contrapose!": 45,
+  "conv": 46,
+  "conv_lhs": 47,
+  "conv_rhs": 48,
+  "convert": 49,
+  "convert_to": 50,
+  "decide": 51,
+  "delta": 52,
+  "derivative_simp": 53,
+  "done": 54,
+  "dsimp": 55,
+  "erw": 56,
+  "eta_expand": 57,
+  "eval_simp": 58,
+  "exact": 59,
+  "exact_mod_cast": 60,
+  "exacts": 61,
+  "exfalso": 62,
+  "exists": 63,
+  "existsi": 64,
+  "ext": 65,
+  "ext1": 66,
+  "fapply": 67,
+  "fconstructor": 68,
+  "field_simp": 69,
+  "filter_upwards": 70,
+  "fin_cases": 71,
+  "first": 72,
+  "fun_prop": 73,
+  "funext": 74,
+  "gcongr": 75,
+  "generalize": 76,
+  "generalize_proofs": 77,
+  "ghost_calc": 78,
+  "ghost_fun_tac": 79,
+  "ghost_simp": 80,
+  "group": 81,
+  "have": 82,
+  "have'": 83,
+  "haveI": 84,
+  "if": 85,
+  "induction": 86,
+  "induction'": 87,
+  "infer_instance": 88,
+  "infer_param": 89,
+  "inhabit": 90,
+  "init_ring": 91,
+  "injection": 92,
+  "injections": 93,
+  "interval_cases": 94,
+  "intro": 95,
+  "intros": 96,
+  "introv": 97,
+  "isBoundedDefault": 98,
+  "iterate": 99,
+  "left": 100,
+  "let": 101,
+  "letI": 102,
+  "lift": 103,
+  "lift_lets": 104,
+  "linarith": 105,
+  "linear_combination": 106,
+  "map_fun_tac": 107,
+  "map_simp": 108,
+  "match": 109,
+  "matrix_simp": 110,
+  "measurability": 111,
+  "mfld_set_tac": 112,
+  "mono": 113,
+  "move_mul": 114,
+  "mv_bisim": 115,
+  "next": 116,
+  "nlinarith": 117,
+  "nofun": 118,
+  "nomatch": 119,
+  "noncomm_ring": 120,
+  "nontriviality": 121,
+  "norm_cast": 122,
+  "norm_cast0": 123,
+  "norm_num": 124,
+  "norm_num1": 125,
+  "nth_rewrite": 126,
+  "nth_rw": 127,
+  "obtain": 128,
+  "omega": 129,
+  "open": 130,
+  "pderiv_simp": 131,
+  "peel": 132,
+  "pgame_wf_tac": 133,
+  "pi_lower_bound": 134,
+  "pi_upper_bound": 135,
+  "positivity": 136,
+  "push_cast": 137,
+  "push_neg": 138,
+  "qify": 139,
+  "rcases": 140,
+  "rcongr": 141,
+  "refine": 142,
+  "refine'": 143,
+  "rel": 144,
+  "rename": 145,
+  "rename'": 146,
+  "rename_i": 147,
+  "repeat": 148,
+  "repeat'": 149,
+  "replace": 150,
+  "revert": 151,
+  "rewrite": 152,
+  "rfl": 153,
+  "rify": 154,
+  "right": 155,
+  "ring": 156,
+  "ring!": 157,
+  "ring1": 158,
+  "ring_nf": 159,
+  "rintro": 160,
+  "rsuffices": 161,
+  "run_tac": 162,
+  "rw": 163,
+  "rw_mod_cast": 164,
+  "rwa": 165,
+  "set": 166,
+  "set!": 167,
+  "set_option": 168,
+  "show": 169,
+  "simp": 170,
+  "simp!": 171,
+  "simp?": 172,
+  "simp_all": 173,
+  "simp_all!": 174,
+  "simp_arith": 175,
+  "simp_intro": 176,
+  "simp_rw": 177,
+  "simp_wf": 178,
+  "simpa": 179,
+  "simpa!": 180,
+  "simpa?": 181,
+  "slice_lhs": 182,
+  "slice_rhs": 183,
+  "solve_by_elim": 184,
+  "specialize": 185,
+  "split": 186,
+  "split_ifs": 187,
+  "subst": 188,
+  "subst_hom_lift": 189,
+  "subst_vars": 190,
+  "substs": 191,
+  "suffices": 192,
+  "swap_var": 193,
+  "symm": 194,
+  "sz_positivity": 195,
+  "tauto": 196,
+  "tfae_finish": 197,
+  "tfae_have": 198,
+  "to_encard_tac": 199,
+  "trans": 200,
+  "transitivity": 201,
+  "trivial": 202,
+  "try": 203,
+  "unfold": 204,
+  "unfold_let": 205,
+  "unfold_projs": 206,
+  "unit_interval": 207,
+  "use": 208,
+  "use!": 209,
+  "valid": 210,
+  "with_unfolding_all": 211,
+  "witt_truncateFun_tac": 212,
+  "wlog": 213,
+  "zify": 214
+}

deployments/mcts/v1.0.1/artifacts/query/config.json

@@ -0,0 +1,29 @@
+{
+  "add_cross_attention": false,
+  "architectures": [
+    "BertModel"
+  ],
+  "attention_probs_dropout_prob": 0.1,
+  "bos_token_id": null,
+  "classifier_dropout": null,
+  "eos_token_id": null,
+  "gradient_checkpointing": false,
+  "hidden_act": "gelu",
+  "hidden_dropout_prob": 0.1,
+  "hidden_size": 384,
+  "initializer_range": 0.02,
+  "intermediate_size": 1536,
+  "is_decoder": false,
+  "layer_norm_eps": 1e-12,
+  "max_position_embeddings": 512,
+  "model_type": "bert",
+  "num_attention_heads": 12,
+  "num_hidden_layers": 6,
+  "pad_token_id": 0,
+  "position_embedding_type": "absolute",
+  "tie_word_embeddings": true,
+  "transformers_version": "5.18.0",
+  "type_vocab_size": 2,
+  "use_cache": true,
+  "vocab_size": 30522
+}

deployments/mcts/v1.0.1/artifacts/query/query.pt

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:8b8c72bfe9812bf735097e197f06050a33cd24b1d3dcf62c2535e2912a47fa0c
+size 90879127

deployments/mcts/v1.0.1/artifacts/query/query_manifest.json

@@ -0,0 +1,15 @@
+{
+  "files": {
+    "config.json": "58b4289a2722242139315e3a0239df7904fa432695dc1f2330ff5767cb0cfcf2",
+    "query.pt": "8b8c72bfe9812bf735097e197f06050a33cd24b1d3dcf62c2535e2912a47fa0c",
+    "tokenizer.json": "da0e79933b9ed51798a3ae27893d3c5fa4a201126cef75586296df9b4d2c62a0",
+    "tokenizer_config.json": "4b91f63e0ec01ae5112b4fab0027b301a38d94f6b1fd001abf2236390168b553"
+  },
+  "lemma_encoder_sha256": "58a5278d01f2b438e8beba05e38dd50d8af10e25539e84a4706e015953c3319a",
+  "max_length": 192,
+  "paired_index_fingerprint": "b42dee6199e4a1c7e764d5c1721c3dc11e99acb476b9ce76dc300be4de6f2a37",
+  "query_encoder_sha256": "3f5a62b9f49423be4d2ae29030fe68b4ea71ccadf7229ad82ecc3771ef47c0a3",
+  "schema": "query_only_v1",
+  "source_checkpoint_sha256": "777e1c91ca3a0baa567df805ddf73c236450bc9d6623f15067efcc5ad669dae8",
+  "text_policy": "goal_first_v1"
+}

deployments/mcts/v1.0.1/artifacts/query/tokenizer_config.json

@@ -0,0 +1,24 @@
+{
+  "backend": "tokenizers",
+  "cls_token": "[CLS]",
+  "do_basic_tokenize": true,
+  "do_lower_case": true,
+  "is_local": false,
+  "local_files_only": true,
+  "mask_token": "[MASK]",
+  "max_length": 128,
+  "model_max_length": 512,
+  "never_split": null,
+  "pad_to_multiple_of": null,
+  "pad_token": "[PAD]",
+  "pad_token_type_id": 0,
+  "padding_side": "right",
+  "sep_token": "[SEP]",
+  "stride": 0,
+  "strip_accents": null,
+  "tokenize_chinese_chars": true,
+  "tokenizer_class": "BertTokenizer",
+  "truncation_side": "right",
+  "truncation_strategy": "longest_first",
+  "unk_token": "[UNK]"
+}

deployments/mcts/v1.0.1/config/rl.json

@@ -0,0 +1,112 @@
+{
+  "arg_loss_weight": 0.5,
+  "bc_anneal_end": 0.05,
+  "bc_anneal_rounds": 200,
+  "bc_anneal_start": 0.5,
+  "certify_heartbeats": null,
+  "checkpoint_every": 20,
+  "collection_devices": [
+    "cpu"
+  ],
+  "collection_workers": 1,
+  "cpu_reserve": 2,
+  "critic_queue_size": 10000,
+  "critic_weight": 0.5,
+  "curriculum_growth_factor": 1.5,
+  "curriculum_solve_threshold": 0.3,
+  "curriculum_start_size": 200,
+  "curriculum_window_rounds": 10,
+  "device": "cpu",
+  "entropy_weight": 0.01,
+  "eval_every": 25,
+  "eval_proposal_mode": "sample",
+  "eval_repeats": 1,
+  "eval_seed": 42,
+  "evaluation_data": {
+    "admission_time_budget_s": 1800.0,
+    "data_source": "dataset",
+    "dataset_name": "jajostrains/Mathlib-Normalized-Sexpr",
+    "dataset_revision": "f44841f98193c09b20c6092198a22e98ff2cd7a8",
+    "max_pool_size": 200,
+    "max_replay_chars": 50000,
+    "max_scan_rows": 20000,
+    "max_state_chars": 400,
+    "seed_cache_path": "/state/eval-admission-cache.json",
+    "split": "train",
+    "theorem_file": null
+  },
+  "grad_clip": 1.0,
+  "htps_batch_size": 64,
+  "htps_learning_rate": 0.0001,
+  "htps_steps_per_round": 0,
+  "learning_rate": 0.0001,
+  "max_dead_rounds": 3,
+  "max_depth": 6,
+  "max_nodes": 32,
+  "max_update_candidate_bytes": 268435456,
+  "max_update_candidates": 100000,
+  "max_update_edges": 250000,
+  "max_update_nodes": 50000,
+  "mine_all_solved_nodes": true,
+  "num_rounds": 500,
+  "num_simulations": 64,
+  "pantograph_imports": [
+    "Init",
+    "Mathlib"
+  ],
+  "pantograph_repl": "/opt/pantograph/repl",
+  "prepared_root": "/artifacts/prepared",
+  "puct_c": 1.0,
+  "resource_check": "strict",
+  "retrieval": {
+    "cache_max_bytes": 8388608,
+    "cache_max_entries": 64,
+    "corpus_path": "/artifacts/lemmas.jsonl",
+    "declaration_inventory": "/artifacts/declarations.json",
+    "device": "cpu",
+    "faiss_threads": 1,
+    "lemma_index": "/artifacts/index",
+    "microbatch_max_size": 2,
+    "microbatch_wait_ms": 2.0,
+    "query_artifact": "/artifacts/query",
+    "queue_max_size": 4,
+    "top_k": 32
+  },
+  "reward_gamma": 0.99,
+  "reward_step_penalty": 0.01,
+  "reward_terminal_failure": 0.0,
+  "reward_terminal_success": 1.0,
+  "run_root": "/state/runs",
+  "seed": 42,
+  "selection_policy": "puct",
+  "server_start_timeout_s": 120.0,
+  "server_timeout_s": 120,
+  "sim_batch_size": 2,
+  "snapshot_retention": {
+    "max_collection_rss_growth_mb": 4096,
+    "max_repl_rss_growth_mb": 2048,
+    "max_replay_combinations": 16,
+    "max_replay_continuations": 2,
+    "max_replay_tactic_steps": 128,
+    "max_retained_snapshots": 128
+  },
+  "source_root": "/opt/mathlib4",
+  "tactic_queue_size": 10000,
+  "theorem_timeout_s": 60.0,
+  "theorems_per_round": 8,
+  "top_k_tactics": 4,
+  "training_data": null,
+  "update_device": "cpu",
+  "use_pln": false,
+  "visit_threshold": 4,
+  "w_critic_soft": 0.5,
+  "warmstart_checkpoint": "/artifacts/checkpoint.pt",
+  "weight_decay": 0.0001,
+  "widening_coefficient": 2.0,
+  "widening_exponent": 0.5,
+  "widening_initial_actions": 4,
+  "widening_max_actions": 16,
+  "widening_max_draws": 64,
+  "worker_queue_size": 0,
+  "worker_shutdown_timeout_s": 10.0
+}

deployments/mcts/v1.0.1/config/service.json

@@ -0,0 +1,89 @@
+{
+  "checkpoint": "/artifacts/checkpoint.pt",
+  "dataset_profiles": {
+    "mathlib-eval": {
+      "admission_time_budget_s": 1800.0,
+      "data_source": "dataset",
+      "dataset_name": "jajostrains/Mathlib-Normalized-Sexpr",
+      "dataset_revision": "f44841f98193c09b20c6092198a22e98ff2cd7a8",
+      "max_pool_size": 200,
+      "max_replay_chars": 50000,
+      "max_scan_rows": 20000,
+      "max_state_chars": 400,
+      "seed_cache_path": "/state/eval-admission-cache.json",
+      "split": "train",
+      "theorem_file": null
+    }
+  },
+  "default_search_profile": "puct",
+  "pln": {
+    "chainer_root": "/opt/pln/src/petta_chainer",
+    "petta_bin": "/opt/pln/bin/petta",
+    "petta_source_root": "/opt/pln/src/PeTTa",
+    "swipl_bin": "/opt/pln/bin/swipl"
+  },
+  "rl_config": "rl.json",
+  "search_profiles": {
+    "best_first": {
+      "max_depth": 6,
+      "max_nodes": 32,
+      "num_simulations": null,
+      "puct_c": null,
+      "selection_policy": "legacy",
+      "sim_batch_size": null,
+      "top_k_tactics": 4,
+      "use_pln": false,
+      "widening_coefficient": null,
+      "widening_exponent": null,
+      "widening_initial_actions": null,
+      "widening_max_actions": null,
+      "widening_max_draws": null
+    },
+    "best_first_pln": {
+      "max_depth": 6,
+      "max_nodes": 32,
+      "num_simulations": null,
+      "puct_c": null,
+      "selection_policy": "legacy",
+      "sim_batch_size": null,
+      "top_k_tactics": 4,
+      "use_pln": true,
+      "widening_coefficient": null,
+      "widening_exponent": null,
+      "widening_initial_actions": null,
+      "widening_max_actions": null,
+      "widening_max_draws": null
+    },
+    "puct": {
+      "max_depth": 6,
+      "max_nodes": 32,
+      "num_simulations": 64,
+      "puct_c": 1.0,
+      "selection_policy": "puct",
+      "sim_batch_size": 2,
+      "top_k_tactics": 4,
+      "use_pln": false,
+      "widening_coefficient": 2.0,
+      "widening_exponent": 0.5,
+      "widening_initial_actions": 4,
+      "widening_max_actions": 16,
+      "widening_max_draws": 64
+    },
+    "puct_pln": {
+      "max_depth": 6,
+      "max_nodes": 32,
+      "num_simulations": 64,
+      "puct_c": 1.0,
+      "selection_policy": "puct",
+      "sim_batch_size": 2,
+      "top_k_tactics": 4,
+      "use_pln": true,
+      "widening_coefficient": 2.0,
+      "widening_exponent": 0.5,
+      "widening_initial_actions": 4,
+      "widening_max_actions": 16,
+      "widening_max_draws": 64
+    }
+  },
+  "state_dir": "/state"
+}

deployments/mcts/v1.0.1/release.json

@@ -0,0 +1,163 @@
+{
+  "application": {
+    "commit": "d94115d683d94f7df33e4ca8ddfad7adbaaf7982",
+    "release_tool_sha256": "72022932d4cebb9861c9af57b4e12b16a337dfe5584252e494fe446688ceabf8",
+    "tracked_dirty": false,
+    "untracked_present": false
+  },
+  "bindings": {
+    "checkpoint_manifest": {
+      "architecture_version": 1,
+      "behavior_mode": "dropout-disabled-v1",
+      "checkpoint_format_version": 4,
+      "encoder_fingerprint": "50162eadb7b942dc3317888952794724dd56a849111e86f3c0ae64e4696269bf",
+      "graph_representation": {
+        "graph_schema_version": 1,
+        "hypothesis_schema": "fv-name-role-type-v1",
+        "model_sexp_version": 1,
+        "representation": "lean-model-sexp-v2"
+      },
+      "model_kind": "actor_critic_with_args",
+      "model_spec": {
+        "architecture": "gatv2",
+        "dropout": 0.2,
+        "encoder": {
+          "heads": 4,
+          "num_layers": 4,
+          "readout": "state_mean_attention"
+        },
+        "hidden_dim": 128,
+        "local_type_bonus_strength": 0.0,
+        "max_args": 3,
+        "retrieval_binding": "b42dee6199e4a1c7e764d5c1721c3dc11e99acb476b9ce76dc300be4de6f2a37",
+        "text_dim": 384,
+        "use_node_type": true
+      },
+      "node_vocab_fingerprint": "5c0a42b6db8b750c099ad3ccc9c819c7b27b543979da3a05e834fbbe70e76bea",
+      "policy_schema": "count-source-identity-gru-v1",
+      "tactic_vocab_fingerprint": "17505aab735227e10c7825f383105e6543b1c5f5e15fd24e69be272bf30af69d"
+    },
+    "environment_identity": "73901041f16e8b5c28da6db5334ad985556b6dd6a06ece77623f9190aec6e8c4",
+    "extra_checkpoint_fields": [
+      "deployment_migration"
+    ],
+    "retrieval_binding": "b42dee6199e4a1c7e764d5c1721c3dc11e99acb476b9ce76dc300be4de6f2a37"
+  },
+  "checkpoint_selection": "checkpoint.pt",
+  "client_companion": {
+    "base_commit": "0dd5d2225e2d093f66a4b6231c1aa35004f2c8f3",
+    "contract_revision": 6,
+    "mathlib_expected_pin": "29dcec074de168ac2bf835a77ef68bbe069194c5",
+    "patch_sha256": "0611ea2f9fe12c81bc788deda7f3300890bb9762d8df31cd6bf5db6b7306e0c6",
+    "source_commit": "fc740c26a1e832ecb571859af24a5c632a351bd9",
+    "source_url": "https://github.com/123nol/Pantograph.git",
+    "toolchain": "leanprover/lean4:v4.10.0-rc1"
+  },
+  "client_sources": {
+    "__init__.py": "cba343dd36c317bc466115210cb23c05ba2378d66fb3c9aa11755cb44ab4e53f",
+    "cli.py": "286c6a3f9c0ef173d618a48e5ed8291c0a1c7e4487b15d8cb2ce5f83289f67cb",
+    "client.py": "5923f92ca8d8f9c30a29be58aa580bbf2871f89fa806b71d84dc1cb75eeeb4aa",
+    "compatibility.py": "b19840f5df765f4e417866bc474f5d80df9524bb303c62428020a15cccd72283",
+    "diagnostics.py": "ea6e1eee93be0a1d20dc7790d25b809ad3b4cabdb542eb3237c9d89e835c1000",
+    "environment.py": "2b3ab222d89d033aed6e6a5fe08d24787ba9cc552f7f3a9603e2bad084aa1473",
+    "launch.py": "70b9df05bd79eccfe8f1827454c89c4b48497575c0876cbacce4fce317426241",
+    "probes.py": "dc84d395312054503432b8b3be15c6aaf543246297965c56a4b6e601229c4697",
+    "protocol.py": "15a914af21412efb970ceccf87e72177206b8c09642e1b77c0cc150a10d9c997"
+  },
+  "client_version": "0.5.0",
+  "files": {
+    "README.md": {
+      "sha256": "4e4022e722001bb11dc1dcf09749f911af0f8beae33fe225e6fb6c534ca286c7",
+      "size": 376
+    },
+    "artifacts/checkpoint.pt": {
+      "sha256": "61b218f60bf03678f84b4f00891a592cea46c9e689fe915454b4db2a3595dd21",
+      "size": 15746933
+    },
+    "artifacts/declarations.json": {
+      "sha256": "6d7e1c1ee94833a5142b3eacbdfe9119a8b4c658a15a0e2f564fd1381386add2",
+      "size": 60345840
+    },
+    "artifacts/index/deployment_manifest.json": {
+      "sha256": "f677d9f57150b9c2208f0523dee58e6a2de034f9df2a34ba49e8bf61cd0d0316",
+      "size": 1385
+    },
+    "artifacts/index/faiss.index": {
+      "sha256": "48027f9cd8dbe1b705b3ec21ae2b2d1752d933e7bf5bdf78c88fb410fe2d61ca",
+      "size": 489911853
+    },
+    "artifacts/index/lemma_ids.json": {
+      "sha256": "2c7764a082d0062f6b5dde65efbfef2e1867b90dfe5080339ceb7305b80fc0cd",
+      "size": 2440514
+    },
+    "artifacts/index/lemma_names.json": {
+      "sha256": "196cab04618821d79f937167995cbe0dd8696313390926734b46ecc9062024cc",
+      "size": 11807120
+    },
+    "artifacts/index/lemma_vectors.npy": {
+      "sha256": "05a6ef64c252cb542ad069f58cec40860300374a44bb0dc2828f7ac6c3f0a60e",
+      "size": 489911936
+    },
+    "artifacts/index/manifest.json": {
+      "sha256": "78f668e3ee4e37738192dea1a7bae02ca5c135a753a59e88e97a680e7f718701",
+      "size": 470
+    },
+    "artifacts/lemmas.jsonl": {
+      "sha256": "e418af465e7d07af48cb64fa6533d8370f386e75f78ae278b1c39aa9ed4d57e9",
+      "size": 137254943
+    },
+    "artifacts/prepared/metadata/graph_representation.json": {
+      "sha256": "f325cb3955068f961531ed6924d31373f21441a0c0b7992e20fda13dfb32e4c6",
+      "size": 148
+    },
+    "artifacts/prepared/vocab/node_vocab.json": {
+      "sha256": "9425af366ba020856416535e30ce1e7a36e0baf6cb5ba5dc67c2f4aabc080a7e",
+      "size": 772550
+    },
+    "artifacts/prepared/vocab/tactic_vocab.json": {
+      "sha256": "1712eac693f116c2b1fa2f9601b9878493d710f8ebb460f9dbb3b938aa4e641d",
+      "size": 3977
+    },
+    "artifacts/query/config.json": {
+      "sha256": "58b4289a2722242139315e3a0239df7904fa432695dc1f2330ff5767cb0cfcf2",
+      "size": 723
+    },
+    "artifacts/query/query.pt": {
+      "sha256": "8b8c72bfe9812bf735097e197f06050a33cd24b1d3dcf62c2535e2912a47fa0c",
+      "size": 90879127
+    },
+    "artifacts/query/query_manifest.json": {
+      "sha256": "fd2ba33fc7f48bbe21fe452d9e57b1085eb6bc3a56ff0e17fa3783653245aa36",
+      "size": 846
+    },
+    "artifacts/query/tokenizer.json": {
+      "sha256": "da0e79933b9ed51798a3ae27893d3c5fa4a201126cef75586296df9b4d2c62a0",
+      "size": 711661
+    },
+    "artifacts/query/tokenizer_config.json": {
+      "sha256": "4b91f63e0ec01ae5112b4fab0027b301a38d94f6b1fd001abf2236390168b553",
+      "size": 593
+    },
+    "config/rl.json": {
+      "sha256": "7e46b68048fbfea160624263d397e99274bee23705c94ac7e3ab9fee9ceacbf5",
+      "size": 3129
+    },
+    "config/service.json": {
+      "sha256": "ef7747741129c5ca210c3c2dae8709f3fcd4e92e0445d010cd5595a062f48409",
+      "size": 2482
+    }
+  },
+  "roles": {
+    "checkpoint": "artifacts/checkpoint.pt",
+    "corpus": "artifacts/lemmas.jsonl",
+    "index": "artifacts/index",
+    "inventory": "artifacts/declarations.json",
+    "prepared": "artifacts/prepared",
+    "query": "artifacts/query",
+    "rl_config": "config/rl.json",
+    "service_config": "config/service.json"
+  },
+  "runtime_requirement": "Exact REPL bytes and compiled Mathlib contents must match the inventory; startup verification is mandatory.",
+  "schema": "mcts-serving-release-v1",
+  "version": "v1.0.1"
+}