{"data":{"kind":"file","path":"README.md","version_id":"gwopv88lld5ynueaqvpo9xm3","entry":{"name":"README.md","path":"README.md","is_directory":false,"size":9245,"modified_at":"2026-10-16T16:19:56.247000","content_hash":"b405a66957c781b600e8ebf2d188390034fa2f2ff0756385ded3af293512fd86"},"entries":[],"content":"# lean-mod-add-proof\n\nA verifiers v1 taskset (an environment for the Prime Intellect Environments Hub) in which the\nmodel has to prove, in Lean 4, that a frozen integer neural network adds modulo p on every\ninput pair. The reward is whether Lean's kernel accepts the proof. There is no model judge and\nno partial credit, so the reward cannot be argued with.\n\n## The task\n\nEach task is one frozen network for addition mod p (p in 5, 7, 11, 13, 17, 19, 23; 8, 16 or\n32 neurons; three seeds). The networks were trained with `train.py` from\nhttps://github.com/teal-sea/lean-checked-network (two layers: embed, add, square, read out;\nweights rounded to whole numbers in [-127, 127]) and only networks that are right on all p*p\npairs, checked in numpy exactly as the Lean definition evaluates, were kept. 13 of the 52 were\ntrained on 90% of the pairs and generalize to the rest; 39 saw every pair during training\n(`train_fraction` in `tasks/tasks.jsonl` says which). 11 of the 63 (p, H, seed) combinations\nnever froze to a fully correct network at these settings and are absent (all the 8-neuron\nnetworks for p >= 17, and two of the 8-neuron ones for p = 13).\n\nThe prompt contains:\n\n- the task statement,\n- `LeanCheckedNetwork/Network.lean` from the repository above, verbatim (the network defined\n  in plain integer arithmetic: `nth`, `hidden`, `dot`, `scores`, `argmax`, `answer`),\n- `LeanCheckedNetwork/Weights.lean` for this network, verbatim: `E1`, `E2`, `W2` as Lean\n  lists of `Int` constructors, `answer a b`, and `Spec`, the proposition to prove,\n- the required theorem name and signature:\n  `theorem LeanCheckedNetwork.Net.adds_mod_<p> : ∀ a, a < p → ∀ b, b < p → LeanCheckedNetwork.Net.answer a b = (a + b) % p`,\n- the rules (allowed imports, forbidden tokens, the time limit).\n\nThe model answers with one ```lean code block, which is the whole file\n`LeanCheckedNetwork/Submission.lean`. The repository's `Fast.lean` (the packed big-number\nevaluator) is not given. For small p a plain `decide +kernel` works; the kernel's cost grows\nwith p squared times the number of neurons, so the larger tasks push towards a faster route.\n\nSplits: seeds 0 and 1 are `train` (35 tasks), seed 2 is `eval` (17 tasks).\n\n## The reward\n\n`kernel_accepts` is 1.0 only if all of the following hold, in this order, and 0.0 otherwise:\n\n1. Text guard (a first filter, before Lean runs): the file contains none of `sorry`, `admit`,\n   `native_decide`, `decide +native`, `ofReduceBool`, `axiom`, `opaque`, `implemented_by`,\n   `extern`, `unsafe`, `partial`, `set_option debug.*`, `macro`, `macro_rules`, `elab`,\n   `elab_rules`, `syntax`, `notation`, `infix`/`infixl`/`infixr`/`prefix`/`postfix`,\n   `initialize`, `#eval`, `run_cmd`, `run_tac`, `run_elab`, `run_meta`, `IO`, `init`,\n   `evalExpr`, imports only `LeanCheckedNetwork.Network` and `LeanCheckedNetwork.Weights`,\n   and does import `LeanCheckedNetwork.Weights`. The match is on whole words anywhere in the\n   file, comments included. (The `#eval` family, `IO` and the required import were added on\n   2026-10-16 after a review found three submissions that got reward 1.0 with a trivial\n   theorem: one skipped the Weights import and defined its own `Spec := True`; one used\n   `#eval IO.FS.writeFile` at build time to overwrite `Check.lean`; one defined\n   `LeanModAddProofCheck.LeanCheckedNetwork.Net.Spec`, which the old dotted check theorem\n   name resolved to. See tests ix_a, ix_b, ix_c.)\n2. A fresh Lake package (toolchain `leanprover/lean4:v4.35.0-rc2`, no dependencies) with\n   `Network.lean`, `Weights.lean` and the submission: `lake build LeanCheckedNetwork.Submission`\n   succeeds within the time limit.\n3. `lake env leanchecker LeanCheckedNetwork.Submission` accepts the module. This replays every\n   declaration through the kernel from the compiled file, so `set_option debug.skipKernelTC`\n   cannot hide a bad proof (tested below).\n4. A file written by the grader after the build and the leanchecker run, `Check.lean`,\n   elaborates: `import LeanCheckedNetwork.Weights`, `import LeanCheckedNetwork.Submission`,\n   `theorem leanModAddProofCheck_statement_matches : _root_.LeanCheckedNetwork.Net.Spec := _root_.LeanCheckedNetwork.Net.adds_mod_<p>`.\n   The check theorem's name has no dots (a dotted name opens its namespace while the\n   statement is elaborated) and both constants are written with `_root_.`.\n   `Spec` is defined in `Weights.lean`, so its meaning is fixed before any submitted text is\n   read; a theorem with the required name but a weaker or different statement fails here.\n5. `#print axioms LeanCheckedNetwork.Net.adds_mod_<p>` lists nothing outside\n   `propext`, `Classical.choice`, `Quot.sound`. By default (`axioms_mode = \"subset\"`) a proof\n   that uses fewer of them passes too (a `decide` proof typically depends on `propext` only);\n   `axioms_mode = \"exact\"` demands all three and nothing else.\n\nThe reason a submission failed, the stage it reached, the axiom list, the timings and the\ntail of each command's output are stored on the trace under `trace.info[\"lean_grader\"]`, and\nthe metric `lean_stages` records `guard_passed`, `build_passed`, `leanchecker_passed`,\n`statement_passed`, `axioms_passed` and `grader_seconds` per rollout.\n\nThe time limit covers build, replay and check together: `--env.taskset.task.timeout-s`,\ndefault 300 seconds. On timeout the whole process group is killed and the reward is 0.0.\n\nGrading runs on the machine that runs the taskset (the verifiers worker), not inside the\nmodel's sandbox. That machine needs elan with the pinned toolchain at `~/.elan/bin`\n(`leanchecker` ships with the toolchain). Each grade uses its own throwaway package directory\n(`--env.taskset.task.work-root`, default the system temp dir) and `LEAN_NUM_THREADS=1`, so\nconcurrent rollouts do not interfere, but each costs one core and up to about 2 GB while the\nkernel runs.\n\n## Layout\n\n```\nlean_mod_add_proof/\n  taskset.py      the TaskData / Task / Taskset classes, the prompt, the reward and metric\n  grader.py       the pipeline above; no verifiers dependency, testable on its own\n  gen_dataset.py  turns train.py .npz files into tasks/<id>/Weights.lean + tasks.jsonl\n  Network.lean    copied from the repository\n  tasks/          52 tasks: tasks.jsonl plus one folder per task\n```\n\n## Running\n\n```bash\nuv venv && uv pip install verifiers          # verifiers 0.4.0 was used\nuv pip install -e .                          # this package\nuv run vf-eval lean-mod-add-proof --dry-run -n 2 --no-push    # resolves and prints the config, runs nothing\nuv run vf-eval lean-mod-add-proof -n 5 --no-push              # needs a model endpoint, see below\nuv run vf-eval lean-mod-add-proof --env.taskset.split eval --env.taskset.max-p 11 --env.taskset.task.timeout-s 600\n```\n\nConfigurable from the command line or a TOML file: `env.taskset.split` (train, eval, all),\n`env.taskset.max_p`, `env.taskset.tasks_dir`, `env.taskset.task.timeout_s`,\n`env.taskset.task.axioms_mode`, `env.taskset.task.work_root`, `env.taskset.task.keep_packages`.\n\nRebuilding the dataset: train networks with the repository's `train.py`, then\n`python3 gen_dataset.py tasks RUN1.npz RUN2.npz ...` (networks that are wrong on any pair or\nhave a tie are skipped).\n\n## What `vf-eval` and `prime env push` need that was not available here\n\n- A model endpoint. `vf-eval` sends the prompts to an OpenAI-compatible endpoint; by default\n  that is Prime Inference (`https://api.pinference.ai/api/v1`) with the key in `PRIME_API_KEY`\n  (or from `prime login`), model `deepseek/deepseek-v4-flash` unless `-m` says otherwise.\n  Another endpoint is set with `--client.base-url` and `--client.api-key-var`.\n- A runtime for the model's harness. The default runtime type is `prime` (a Prime sandbox,\n  which needs the same account and key). Locally, `--env.agent.runtime.type subprocess` or\n  `docker` avoids that; the harness is `bash` by default and `--env.agent.harness.id null` is\n  the plain chat loop.\n- `--push` (on by default) uploads the run to the platform and needs `PRIME_API_KEY`;\n  `--no-push` keeps it local.\n- `prime env push` needs the Prime CLI (`uv tool install prime`), `prime login`, a username\n  set on the account profile, and is run inside this directory. `--visibility PRIVATE` keeps\n  it private, `--team <team>` pushes to a team.\n\nNone of these were run: this container has no Prime Intellect account, key or model endpoint.\nThe taskset was exercised with its own classes (`Task.score` on hand-built traces) and with\n`vf-eval --dry-run`.\n\n## Limits\n\n- The text guard is coarse on purpose and also rejects the banned words in comments.\n- The statement check accepts any theorem whose type is definitionally equal to `Spec`.\n- Axioms are read from the text output of `#print axioms`; the parser expects Lean 4.35's\n  wording.\n- The tasks are all small (p <= 23); brute force by `decide +kernel` is feasible on every\n  task, slower on the bigger ones (measured times are in `../tests/logs/`). The difficulty gradient is time, not possibility.\n- Grading needs a Lean toolchain on the grading machine; nothing installs it. Running the\n  grader in a container through `IsolatedVerifierEnv` (a `@vf.reward` taking `runtime`) was\n  not done.\n- No memory limit is set on the Lean processes.\n","encoding":"utf-8","truncated":false,"total_bytes":9245},"status":null}