Conversation
Inspect's built-in bash tool discards the returncode, so a command that died for any reason -- uncaught Python error, missing binary, permission denied, segfault, SIGKILL from the cgroup OOM killer -- reaches the agent as silent missing output. The OOM signal Inspect exposes is just ExecResult.returncode == 137 (see inspect_ai/util/_sandbox/docker/ docker.py:351-359, which already disambiguates timeout-induced 137 from external SIGKILL). Replace the built-in bash with a thin local wrapper that, on non-zero exit, returns stdout/stderr/returncode each wrapped in pseudo-XML tags; on exit 0 it behaves identically to the built-in. The model interprets 137/127/etc. on its own. Same treatment in PantographVerifier._call: on a daemon transport failure, the error embeds the raw exit code (e.g. "status 137") instead of a generic "transport failed".
The lean_check tool, the LeanVerifier abstraction, and the in-sandbox warm daemon (apn_lean.py: unix socket, lockfile, JSON protocol) existed to amortize a Mathlib import cost that profiling shows is modest: Server.create() in the agent image takes ~45s cold and ~2s once the OS page cache is warm, with check_compile at ~2ms on a live Server. At ~2s per fresh-process compile, the agent can simply create Servers itself from python3 and pick its own usage pattern. Delete: - apn/verifier/ (LeanVerifier protocol, PantographVerifier, host-side CompileResult/Diagnostic types) - apn/lean/apn_lean.py (daemon + client + parsing helpers) and its tests; drop the COPY from Dockerfile.agent - the lean_check tool and format_check_feedback - apn/_exec_status.py (no remaining callers) The prompt now tells the agent PyPantograph is installed, where the FormalConjectures project lives, and which import set to use; the agent is otherwise unguided in how to drive Lean. This is also less opinionated: the full Pantograph API (interactive tactics, load_sorry drafting, env introspection) is available, not just file compilation.
The sandbox has no network, so the agent needs an offline PyPantograph reference. Previously the full source clone lingered at /opt/PyPantograph as a side effect of the build, but a second copy of the package source is a shadowing hazard: python started inside that directory imports the source tree (which lacks the built repl) instead of the installed package. Instead, delete the clone after pip install and COPY an explicit, human-inspectable docs directory (apn/lean/pypantograph-docs/) to /opt/pypantograph-docs. Vendored from the pinned commit b8608f3 so it matches the installed version exactly: intro.md and setup.md as-is, the goal / agent-search / frontend notebooks converted to plain markdown (code cells fenced, outputs preserved), the examples/ scripts, and the upstream Apache-2.0 LICENSE. The api-*.rst autodoc stubs are skipped (no content; docstrings ship with the installed package). The prompt now points the agent at /opt/pypantograph-docs.
PyPantograph is the Python interface to Pantograph (leanprover/ Pantograph), which it vendors as its src/ submodule and builds into the pantograph-repl binary shipped inside the installed package. So the agent already has both projects; but Server.run_async(cmd, payload) is a generic passthrough to the repl protocol, including commands the Python wrapper has no named method for. Vendor the protocol reference too, taken at the submodule commit pinned by PyPantograph b8608f3 (5fcb7542), so it matches the built repl exactly.
repl.md documents Pantograph (the Lean-side repl), not PyPantograph (the Python interface), so mixing it into pypantograph-docs/ conflated the two projects. Give it a separate folder with Pantograph's own LICENSE, shipped at /opt/pantograph-docs, and tell the agent how the two relate (the repl protocol is what Server.run_async reaches).
apn_safeverify.py was a JSON-over-stdin protocol wrapped around three shell commands (compile target, compile submission, run safe_verify) -- the same shape as the deleted apn_lean.py daemon. Delete it and have SandboxSafeVerify issue the three commands itself, one sandbox exec per step. The stage distinction the JSON envelope encoded becomes implicit: each step is its own exec, so the checker knows exactly where a failure happened. Verdict mapping is unchanged in substance: target compile failure raises (broken spec = infra, not a verdict on the proof); submission compile failure scores INCORRECT; safe_verify exit 0/nonzero is accept/reject; and any step killed by a signal (exit >= 128, e.g. OOM's 137) raises rather than mis-scoring. Validated the exact command sequence against the rebuilt scorer image: a valid proof passes and a sorry-smuggling submission is rejected with "uses disallowed axioms". Also exclude the vendored pypantograph-docs examples from mypy.
A crashed prior call could leave submission.olean behind; the next call would then run safe_verify against that stale artifact if its own compile step also failed weirdly. Clear the score dir up front so each verdict is computed from only this call's files.
Profiling across benchmark samples shows safe_verify has a ~27 GiB fixed footprint (four importModules calls, each materializing the Mathlib environment on the heap) plus an effectively unbounded content-dependent part: its un-memoized rebuildExpr expands pointer-shared proof terms exponentially, so e.g. a (a+b+c)^16 ring proof that compiles at 6.4 GiB blows past 34 GiB at verification. No mem_limit makes scorer OOMs impossible; 50g covers the baseline plus the worst production observation (~43 GiB). Fixes belong in the vendored safeverify and are deliberately deferred.
Merge the three Dockerfiles into one multi-stage apn/lean/Dockerfile (builder -> base -> agent/scorer) and give each compose service a build: section alongside image:. Inspect's compose build then creates the images automatically at eval startup -- no manual building or tagging, and version bumps just work. Instructions are byte-identical to the old files, so existing layer caches still hit. CI builds the stages with --target; the pushed base image substitutes for the base stage in the agent/scorer builds via a named build context (same semantics as the old pull-and-tag step).
Subagent analysis of the oeis-proved38 transcripts (gpt-5.5, gemini-3.1-pro)
showed most failures were motivational, not mathematical: models hallucinated
short deadlines ("five minutes", "an hour"), declared the target an unsolvable
open conjecture (often after deriving the right proof route), collapsed into
verbatim "I am unable" refusal loops for hundreds of turns, or burned the
budget hunting verifier loopholes. Successful attempts instead decomposed into
small compilable lemmas and treated rejections as debugging feedback.
Rewrite the motivational block of the instructions accordingly: state that the
problems are feasible and must be attempted, disclose the real token budget
(lean_instructions now takes the configured token_limit) and the absence of
any wall-clock deadline, foreclose verifier cheats, coach getting any grip on
the problem when stuck, forbid no-op "I am stuck" messages, and frame gated
rejections as feedback rather than verdicts.
A cost_limit isn't a token limit, so the resources tool the agent uses to self-pace couldn't show a dollar budget. List every limit Inspect tracks for the sample -- Cost, Tokens, Time -- under a header stating they apply together and reaching any one ends the task; each shows used/remaining/(limit) or '(no limit set)'. Add _format_usd and reword the parenthetical '(budget X)' -> '(limit X)' so 'budget' no longer doubles as both a label and the limit word.
An oversized submission is the agent's doing (a giant generated file or an expensive proof term inflating the compiled olean) and is deterministic per submission, so erroring the sample only discards it -- rerunning can never help. Catch OutputLimitExceededError (Inspect's MAX_READ_FILE_SIZE) on the agent-side read_file calls and map it to a verdict instead: - compiled olean too large to read back -> compile_submission_oversize verdict - Submission/ tar too large to read -> submission_oversize rejection (scorer) - safe_verify --save report too large -> degrade to None (best-effort, read after the verdict, so it never changes the outcome) write_file calls are unaffected (the k8s sandbox caps reads, not writes).
…ust safe_verify
_RESOURCE_STAGES only listed the two safeverify_* stages, so a submission that
OOM'd or timed out while *compiling* (compile_submission_resource /
compile_submission_timeout) silently fell through to the opaque "did not pass
verification" message instead of the resource hint -- the agent was never told
to aim for a cheaper proof, and burned attempts blindly.
Include every too-expensive-to-process stage across both agent-side steps and
the scorer: compile_submission_{resource,timeout,oversize}, safeverify_{resource,
timeout}, and submission_oversize. Reword the message to cover oversize too while
staying opaque about which limit, which stage, and the amount. Decode failures
and plain compile/safeverify rejections stay opaque (wrong, not too expensive).
Downloads, for each of the 444 unique OEIS sequences behind the 492
conjectures, the JSON API record and the full (paginated) revision
history, parsing the history HTML into structured {v, user, time,
changes, discussion} revisions. Feeds a later provenance-extraction
pass (proposer + date per conjecture).
Three pipelines over the 444 sequences behind the 492 conjectures, plus their outputs: - conjecture_provenance.jsonl (492): per-conjecture proposer + date, extracted by scripts/extract_provenance.py (GPT-5.5) from the OEIS records + revision history, keeping the proposer distinct from verifiers/editors. - oeis_native_citations.jsonl (444): the entry's own link[]/reference[] bibliography, structured by scripts/extract_bibliography.py (GPT-5.5) into title/authors/venue/year/doi/arxiv_id/kind. - openalex_citations.jsonl (444): papers referencing each sequence, from a union of three OpenAlex full-text queries (scripts/find_papers.py), deduped within OpenAlex. NOTICE.md rescoped to attribute only the third-party data (Formal Conjectures Auto/THEOREM_MAPPING under Apache-2.0; raw/ from OEIS); the derived metadata is this repo's own.
Replace --parallel with two independent flags: --parallel-evals (the old across-files fan-out) and --parallel-samples (new: extract samples within each file across worker processes, each reading its own sample by id). The flags compose; a bare flag uses half the CPUs. The largest log file no longer bounds wall-clock time. hawk_download_eval_set.py now passes --parallel-samples when extracting.
Sync with PortBench mr-scripts branch: status-based retry dedup reading .eval headers via s3fs, --method hawk|s3, --output-root, and --force-most-tokens-on-all-error. Keeps our local --parallel-samples flag for plaintext extraction.
A second dataset (FC100OpenSet1, next commit) reuses the per-target isolation pipeline, so separate what is generic from what is OEIS: - scripts/isolation.py (new): the dataset-neutral engine, moved verbatim from scripts/oeis_isolation.py -- the pure cut/matching helpers and the Docker plumbing (extractor + compile gate). - scripts/oeis_isolation.py: now just the OEIS frontend (data locations under apn/data/oeis/ + the THEOREM_MAPPING.txt parser re-export). - scripts/generate_isolated.py -> scripts/generate_oeis_isolated.py: the generic name becomes misleading with two datasets. - tests/lean_sandbox.py (new): the Inspect-sandbox bring-up and the stage/extract/compile plumbing from tests/test_oeis_isolation.py, now shared between the isolation validation suites. stage() takes optional arcnames so a caller can preserve relative paths (the FC tree has basename collisions); extract() keys records back by arcname. No behavior change; validated by re-running the full OEIS isolation suite (structural + 492-file compile + paper oracle: 3 passed).
The paper's frozen open-problem subset (arXiv 2605.13171, FormalConjectures/Subsets/FC100OpenSet1.lean: 100 `research open` statements in 88 files), evaluated with the same solver, SafeVerify scorer, and sandbox images as apn_oeis -- no image changes needed (the baked FC commit 67338a1 has the paper's bench-v1-lean4.27.0 tag as an ancestor; see apn/data/fc100open/NOTICE.md). Results are comparable to the paper's set modulo two footnotes: - The 14 value-typed answer(sorry) members are excluded (EXCLUDED.txt): the placeholder puts a position-labeled sorryAx in the statement *type*, which SafeVerify cannot score. 86 samples remain. - The 46 propositional `answer(sorry) ↔ P` statements are rewritten to plain `P` at generation (the placeholder elaborates to a bare True), so goals are honest and no answer( reaches the shipped specs' code. The text surgery is certified by re-elaboration: the source target's raw-Expr type must equal `Iff True (<isolated type>)`, compared after erasing macro-hygiene binder counters (α-equivalence; the rewrite shifts per-command hygiene indices in 5/46 statements). Isolation reuses the engine from scripts/isolation.py via the new FC frontend (scripts/fc100_isolation.py + generate_fc100_isolated.py), keyed by relative path (the FC tree has basename collisions), with one FC-specific cut: anonymous `example` sanity checks are dropped (GraphConjecture316/327 run `decide +native`, which would otherwise execute inside the trusted target compile on every score call). The sorry'd Mordell-Weil instance in Wikipedia/EllipticCurveRank.lean is deliberately kept (allowlisted): that sample implicitly also requires proving Module.Finite ℤ E⟮K⟯. Validated by tests/test_fc100.py (membership/dataset invariants), tests/test_fc100_isolation.py (re-extraction structural gate incl. the rewrite certificate, and the lake-env-lean compile gate over all 86), and a one-sample smoke eval (rejection at stage=safeverify confirmed).
Ad-hoc smoke runs select samples with --sample-id instead; no shipped subset (and no eval-set config built around one) is needed. The subset mechanism itself stays -- apn_fc100open(subset=...) still resolves *.txt files under apn/data/fc100open/subsets/ if any are added later.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.