{"data":{"kind":"file","path":"README.md","version_id":"w139dmpyx1jcvdqb5pnra23n","entry":{"name":"README.md","path":"README.md","is_directory":false,"size":4093,"modified_at":"2026-10-04T07:36:05.853000","content_hash":"69f85f135757d6c2a267d7b312e0e3caa25c0a04dd58eac382254142d5448eb3"},"entries":[],"content":"# MathCheck RL\r\n\r\nMathCheck RL is an answer-key-free reinforcement-learning and evaluation\r\nenvironment for bounded integer mathematics. It generates each prompt and its\r\ntrusted checker from one frozen bounded specification. A model submits an\r\ninteger candidate or a complete pair certificate in fenced JSON; it does not\r\nsubmit a Lean proof or replace the specification.\r\n\r\nReward is binary. A reward of `1` means the submission satisfied the complete\r\nencoded bounded specification. Scalar tasks establish the exact bounded\r\nevaluation, sum, count, or minimum. Pair-certificate tasks establish equality\r\nwith the entire satisfying relation in the declared rectangle and the claimed\r\ncardinality. The claim is limited to the encoded bounds; this environment does\r\nnot claim to prove arbitrary mathematical prose or facts outside those bounds.\r\n\r\nThe environment does not store an expected candidate. In the compatibility\r\nAPI, the framework column named `answer` carries only the frozen checker\r\nspecification and is never rendered into the model prompt. Train and evaluation\r\ntasks are generated deterministically and are disjoint by specification digest.\r\n\r\n## Task configuration\r\n\r\n- `families`: `all` or a comma-separated subset of supported bounded families.\r\n- `num_per_family`: number of generated training tasks per family.\r\n- `seed`: deterministic training-generation seed.\r\n- `eval_num_per_family`: compatibility-API evaluation tasks per family.\r\n- `eval_seed`: deterministic compatibility-API evaluation seed.\r\n- `task.verify_timeout`: Verifiers v1 native-check timeout in seconds.\r\n- `task.lean_bin`: optional explicit path to the isolated Lean launcher.\r\n\r\n## Submission format\r\n\r\nThe prompt states the exact JSON schema. A scalar task uses a fenced object such\r\nas:\r\n\r\n```json\r\n{\"answer\": 17}\r\n```\r\n\r\nScalar candidates must be nonnegative integers smaller than `10**1000`.\r\nBooleans and JSON floating-point values do not satisfy this schema. Negative\r\nintermediate arithmetic is supported, but negative final answers and “no\r\nsolution” for a minimum are not representable submissions. The procedural\r\nminimum generator creates satisfiable instances.\r\n\r\nPair tasks require the complete bounded relation and its cardinality in the\r\nschema shown by that task. Pairs must be sorted lexicographically with no\r\nduplicates. Extra prose, replacement specifications, malformed JSON,\r\nincomplete relations and out-of-bounds pairs are rejected.\r\n\r\n## Reward and metrics\r\n\r\n- `nv_specification_pass`: reward `1.0` only for an accepted complete result;\r\n  otherwise `0.0`.\r\n- `nv_stage_rank`: zero-weight diagnostic metric for checker progress.\r\n- `nv_verify_seconds`: zero-weight native verification wall-time metric.\r\n- Trace metadata records status, stage, reason, specification and submission\r\n  digests, duration, backend, scope, checker invocation count, and diagnostics.\r\n- Concurrent reward and metric requests share one verification. The v1 cache\r\n  includes resolved launcher and toolchain settings, keeps immutable verdicts,\r\n  and retries operational failures on later requests.\r\n\r\nTimeouts and backend failures fail closed with zero reward and an operational\r\nstatus. They are not reported as mathematical counterexamples.\r\n\r\n## Runtime requirements\r\n\r\nExecution requires Linux, MathCheck Engine's `lean-isolated` launcher, and a\r\nstandalone Lean 4.23.0 distribution. Configure:\r\n\r\n```bash\r\nexport NATIVE_VERIFY_LEAN=/absolute/path/to/lean-isolated\r\nexport LKV_SANDBOX_TOOLCHAIN=/absolute/path/to/lean-4.23.0-linux\r\n```\r\n\r\nThe launcher requires bubblewrap and a kernel that permits its isolation mode.\r\nMissing isolation fails closed; MathCheck RL does not fall back to executing\r\nuntrusted model code with an arbitrary host Lean installation.\r\n\r\n## Source and scope\r\n\r\n- MathCheck RL: https://github.com/stanleyngugi/mathcheck-rl\r\n- MathCheck Engine: https://github.com/stanleyngugi/mathcheck-engine\r\n\r\nThe older finite-observation sequence adapter remains in the repository as a\r\nlegacy experimental baseline. It is not the contract published by this Hub\r\nenvironment.\r\n","encoding":"utf-8","truncated":false,"total_bytes":4093},"status":null}