Conversation
Add the apn package skeleton and the core ProofSketch text model: EVOLVE-BLOCK/EVOLVE-VALUE marker parsing, comment-aware sorry detection, frozen-skeleton extraction for integrity checks, and search_replace edits restricted to editable regions. Configure strict mypy and pytest.
apn/verifier/base.py defines the LeanVerifier protocol (compile + print_axioms) with CompileResult/Diagnostic/AxiomResult. apn/safeverify.py implements the three-part validation: compiles, statement preserved (skeleton equality), and axiom guard (sorryAx tolerated only while sorry remains). Add an in-process FakeVerifier double for offline testing. pytest-asyncio in auto mode.
apn/lean/: Docker image (Lean v4.29.1 + Mathlib v4.29.1 olean cache + PyPantograph), a lake project, and apn_lean.py -- a sandbox-side daemon that keeps a warm Pantograph server behind a Unix socket plus a thin client the host calls per compile. Pin v4.29.1 to match PyPantograph's bundled repl (paper used v4.27; documented). apn/verifier/pantograph.py: host-side LeanVerifier that shells into the sandbox via the daemon client and parses compile diagnostics + axiom queries. Pure parsing helpers in the daemon are unit-tested.
apn/tools.py: the search_replace Inspect tool (compact-diff edits restricted to EVOLVE regions, recompiles after each edit, keeps failing edits for iteration) bound to a mutable EpisodeState. apn/prompts.py: basic agent (A) prompt transcribed verbatim from Figure 5. Fix the Lean image (drop nonexistent build target; Pantograph only needs Mathlib oleans on LEAN_PATH).
apn/agents/basic.py implements Figure 1's pseudocode: run_episode (multi-turn search_replace session validated by SafeVerify at the end), run_subagent (Ralph loop adopting validated sketches, reverting on validation failure, stopping on a complete proof), and run_basic_agent (N independent subagents in an anyio task group, cancelling the rest on first success). Exposed as the basic_agent Inspect solver. Deterministic tests via mockllm + FakeVerifier.
apn/scorer.py independently re-validates the agent's final sketch with SafeVerify (correct iff complete proof). apn/dataset.py loads .lean sketches into Samples (target decls inferred or from metadata) with three bundled smoke-test sketches. apn/task.py wires dataset + basic_agent + scorer + the Docker Lean sandbox into the apn_basic task.
Each prover subagent is now an Inspect @agent launched via inspect_ai.agent.run, which copies/isolates input and records a transcript span per subagent, instead of calling the orchestration helper from a bare task group. The anyio task group is retained only to cancel the remaining subagents once one finds a proof. Also fix sorry detection for Lean v4.29.1's backtick-quoted warning.
Run each prover subagent via inspect_ai.agent.run (own span, isolated state) and implement each episode as a built-in react agent (submit=False, which terminates exactly when the model stops calling search_replace), bounded by a message_limit. This replaces the hand-rolled generate/execute_tools loop. Since react/run require an active sample context, the agent tests now run through eval_async with a mockllm model and the in-process FakeVerifier. Also fix sorry detection for Lean v4.29.1's backtick-quoted warning, add the backtick test, and the README.
The Pantograph server preloads Mathlib, so an 'import Mathlib' line in the sketch hit 'invalid import command' on every compile, making compiles=False regardless of the proof body and causing all episodes to fail. The daemon now blanks import lines (preserving line numbers) before check_compile / axiom queries. Found via a real end-to-end eval.
…ubagent Editing now uses Inspect's text_editor tool on a file in the sandbox, with a lean_check tool to compile (replacing the bespoke search_replace). Each subagent gets its own Lean sandbox: apn_basic provisions one Docker service per subagent, and the subagent's task scopes the visible sandbox to its own so text_editor (which injects into the first sandbox it finds) is correctly pinned. EVOLVE-region/statement integrity is enforced post-hoc by SafeVerify. Agent tests become Docker-gated integration tests (text_editor needs a Linux container). Also incorporates the strip_import_lines daemon fix.
When restricting a subagent's visible environments to its single sandbox, also set the default-sandbox context var to that name; otherwise the sample-wide x-default service name leaks in and sandbox() fails to resolve within the scoped map (num_subagents>1). Validated end to end: claude-sonnet-4-5 proves the bundled sketches against real Lean/Mathlib at num_subagents=1 and 2 (accuracy 1.000). README updated for text_editor + per-subagent sandboxes.
Drop ProofSketch.apply_search_replace, the SearchReplaceError exception, and EvolveRegion.contains (only used by that method) plus their tests; editing is now done with text_editor and integrity enforced post-hoc by SafeVerify. Remove the unreferenced static apn/lean/compose.yaml (apn_basic generates compose dynamically) and refresh the docstrings that mentioned search_replace.
Remove the bespoke framework -- EVOLVE-BLOCK/VALUE markers, the ProofSketch model, skeleton-based integrity, and the entire episode/Ralph/parallel-subagent orchestration with its sandbox-scoping. The solver (apn/agent.py) is now a thin wrapper around Inspect's deepagent given the proof file plus text_editor + lean_check; it runs deepagent's own loop and reads the result back. Independent attempts per problem are just Inspect epochs passed at eval time (--epochs N), each a fresh sample run with its own sandbox -- no custom subagent code or reducer, and one Docker service per sample. The anti-cheat moves entirely into SafeVerify/the scorer: the final proof must compile, keep the theorem statement verbatim, be sorry-free, and use only permitted axioms. Bundled sketches drop the EVOLVE markers (just theorem + sorry). Validated end to end: claude-sonnet-4-5 proves add_comm against real Lean/Mathlib via deepagent (text_editor x3 + lean_check + submit), accuracy 1.000. mypy clean; 30 unit tests pass.
The real scorer now uses the vendored Lean SafeVerify exe, making the parallel Python anti-cheat a production-dead, test-only reimplementation. Remove it: - delete apn/safeverify.py (safe_verify, check_statement_preserved, check_axioms, extract_statement, ValidationVerdict) and its tests - remove checker.FakeSafeVerify (only consumer of the above) - drop print_axioms + AxiomResult from the verifier layer (only the deleted safe_verify used them); LeanVerifier is now compile-only, matching what the agent's lean_check actually needs - delete apn/verifier/fake.py (FakeVerifier now unused) - retarget test_checker.py at the scorer wiring via a stub checker Vendor the ported SafeVerify (Lean 4.29.1) and wire SandboxSafeVerify as the scorer.
Split the monolithic image into a shared Mathlib base plus two derived images: apn-agent (Pantograph, the agent's writable workspace, NO SafeVerify) and apn-scorer (SafeVerify, a trusted container the agent never touches). The sample now provisions two sandbox services (default=agent, scorer=apn-scorer); the scorer writes the submitted proof into the clean scorer sandbox and runs SafeVerify there, so the agent cannot tamper with the checker, target spec, or oleans. Add apn/lean/build.sh; update task + README.
The proof is the edited file, not a text answer, so the default submit(answer) is meaningless. Pass AgentSubmit(tool=submit()) where submit takes no arguments and just signals completion.
Replicates the paper's OEIS evaluation (44/492). New v4.27 toolchain track alongside the existing v4.29.1 bundled track: - apn/lean/fc/: shared FC base image (Lean v4.27 + Mathlib + the FormalConjectures library), agent image (warm PyPantograph v0.3.13, matched to Lean v4.27, preloading FormalConjectures.Util.ProblemImports), and scorer image (SafeVerify ported to v4.27). compose.yaml + build.sh. - apn/data/oeis/: vendored 484 OEIS/Auto files + THEOREM_MAPPING.txt (492 conjectures), pinned to formal-conjectures auto_oeis @67338a1, with NOTICE. - apn.dataset.oeis_dataset(): one Sample per conjecture; the whole file is the sketch so the agent must discharge the embedded test lemmas (misformalization guard) plus the conjecture; SafeVerify re-checks every decl verbatim. - apn.task.apn_oeis: wires the loader + warm verifier + SafeVerify scorer + FC sandbox. Reuses the daemon (APN_LEAN_IMPORTS) and PantographVerifier unchanged. - Generalized agent instructions for multi-decl files. Validated: FC base compiles a real OEIS file; v4.27 SafeVerify accepts a real 151-line paper proof (A282779) and the agent smoke run exercises the pipeline.
Previously a token/time limit unwound through the solver before it read the proof file back, so the scorer saw no submission and reported 'did not produce a final proof'. Read the file in a finally block so SafeVerify always judges the actual file the agent left -- including a complete proof finished but never submitted.
The agent can now run python3 in its sandbox (via the built-in bash tool, not the python tool) as a numerical scratchpad -- compute sequence terms, test a bound on small cases, hunt for patterns/counterexamples -- before committing to a Lean proof. Instructions updated to describe it and to stress it is exploration only (no formal weight; the proof must still be pure Lean).
The sandbox has no network, so the agent's python3 scratchpad (via bash) only has what's in the image. Add numpy + sympy -- directly useful for the OEIS number-theory problems (primes, factorization, totient, exact rationals). Instructions updated to mention them.
An OOM-kill of safe_verify (SIGKILL under memory pressure) was being reported as
a clean rejection, silently failing a *valid* proof -- this masked a genuine
agent solve of an OEIS conjecture. Now:
- apn_safeverify.py keys the verdict on safe_verify's explicit markers
('SafeVerify check passed.' / 'SafeVerify check failed.'); if neither is
present (crash/OOM/timeout) it emits a system_error. A target-spec compile
failure (trusted data) is likewise a system_error.
- SandboxSafeVerify.check raises on any infrastructure failure (exec failure,
unparseable output, or system_error), so the sample errors out and is
rerun/inspected rather than scored INCORRECT.
With gate enabled, the submit tool runs SafeVerify on the agent's file and only accepts it if verification passes; a failed submission raises ToolError, which the react loop does not count as a submission, so the agent is forced to keep working until it produces a valid proof or hits a limit. The agent is told only that verification failed -- the verifier's output is withheld so it cannot probe SafeVerify for gaps. An infrastructure failure of the checker propagates (crashes the sample) rather than being treated as a rejection. apn_oeis gains a gated=bool flag; the same checker instance drives both the gate and the final scorer.
The v4.29.1 image set (apn/lean/*) was vestigial scaffolding from before the real datasets existed; everything the paper needs is v4.27. Collapse the two duplicated image sets into one: - Promote apn/lean/fc/* up to apn/lean/* (single Dockerfile.base/agent/scorer, compose.yaml, build.sh, safeverify/). Images retagged apn-lean-base/apn-agent/ apn-scorer (now v4.27 + FormalConjectures). - Remove the v4.29.1 base lakefile/lean-toolchain and the v4.29.1 SafeVerify. - Drop apn_basic, the bundled sketches (apn/data/sketches), and the bundled-only dataset helpers; dataset.py is now just the OEIS loader. - Update task.py (single COMPOSE_FILE), the pantograph docstring, tests, README. One track, one image set; smoke-testing uses an OEIS subset (-T names=...).
The finally-block read captured the agent's final file, but a broad except fell back to the original sketch on any failure -- silently turning a real sandbox read failure into a clean INCORRECT (the same anti-pattern just removed from the scorer). read_file isn't gated by the token limit and the file is written up front, so it normally succeeds; let a genuine failure error the sample instead.
state.output was being set to ModelOutput.from_content(content=final_proof), misattributing the raw Lean file as model-generated text -- and discarding run()'s actual return value. The scorer reads the proof from the store (and the Score sets answer=final), so state.output is only for display; set it to the agent run's real output instead.
…ges=True The misleading 'assistant said the verdict' rendering was react folding the submit tool's return into the assistant message (keep_in_messages=False). Set keep_in_messages=True so the submit call + result stay as a normal tool interaction (verdict correctly attributed to the tool, not the model), and name the tool 'submit_proof' so the main loop's name-based submission scan can never collide with the deepagent subagents' 'submit' tool -- making keep_in_messages =True safe from the early-termination bug. Informative returns restored.
The base image git-clones the whole formal-conjectures repo to build the library closure, which left the entire conjecture corpus in every agent's sandbox -- all 484 OEIS problems plus the Erdős/Arxiv/etc. sets, which contain real proofs and axioms. An agent could grep its workspace for related solved problems/techniques. After building FormalConjectures.Util.ProblemImports, remove every FormalConjectures/ subdir except the Util library; importing ProblemImports still resolves via the built oleans (verified: an OEIS file still compiles, workspace FormalConjectures drops from ~all-problems to 96K).
Gating is now Inspect's AgentAttempts: with max_attempts>1, react re-runs the task scorer (SafeVerify) on each submission and, if not accepted, replays a fixed INCORRECT_MESSAGE (no verifier output) until acceptance or a token limit. This deletes the custom gated_submit tool, the gate parameter, and the ToolError-based gating. For this to work mid-loop, proof_scorer now reads the submission *live* from the agent's proof file in the sandbox instead of a solver-written store entry -- so it gives the same verdict whether react scores it per-submission or Inspect scores it at the end. The solver therefore no longer needs the store write or the finally block. apn_oeis(gated=True) maps to max_attempts=99_999_999 (token-limit bounded); gated=False -> max_attempts=1 (submit ends the loop, validated once at the end). Infra failures still propagate (score() doesn't catch), crashing the sample.
Two fixes:
1) A submission that fails the kernel replay (unsafe/partial constant, kernel
type-check failure, missing imports) makes safe_verify exit nonzero BEFORE
printing 'SafeVerify check failed.'. The marker-based classifier mistook this
for an infra failure and raised, crashing the sample/eval -- e.g. a gated run
died on a real cheat attempt ('unsafe constant fakeProof detected'), which
SafeVerify had correctly caught. Classify by exit code instead: <0 (signal,
e.g. OOM) is infra; 0 is pass; any positive code is a genuine rejection
(INCORRECT). Extracted as a pure, unit-tested classify_safeverify().
2) Also strip FormalConjecturesTest (the library's own test suite) from the
workspace image -- not needed at runtime and potentially confusing. The
proving library (Util + FormalConjecturesForMathlib) is kept.
A negative subprocess return code means 'killed by signal N' (POSIX), which is reliably infra -- but the signal could be SIGKILL (OOM/timeout), SIGSEGV (crash), etc. Report the actual signal name/number instead of asserting OOM.
…ipping A builder stage clones the whole formal-conjectures repo and builds the library; the final image copies in ONLY the toolchain, the .lake build artifacts (oleans), and the proving-library source (FormalConjectures/Util + FormalConjecturesForMathlib). The conjecture corpus (other problems / Erdős/Arxiv proofs), the library test suite, repo tooling/docs, and .git never reach the agent's sandbox -- nothing to strip after the fact, and the workspace contains only the library it proves with. Verified: a real OEIS file compiles from the copied artifacts; workspace is just .lake + the library; lake resolves in both login and non-login shells.
New host-side arxiv_search / arxiv_source tools (network runs in the controller; the sandbox stays airgapped). Both gate to papers predating the benchmark paper (arXiv:2605.22763, May 2026): search bounds submittedDate, source resolves the newest pre-cutoff *version* so a post-cutoff revision can't surface a solution to these open conjectures. Exposed as lean_prover(literature=) / apn_oeis(-T literature=true), off by default -- a distinct literature-augmented run condition. The tools and their prompt paragraph are only added when enabled.
The bash scratchpad ships sympy, mpmath, and numpy; the prompt only named sympy and numpy. List all three with what each is for -- notably mpmath's pslq/identify for guessing closed forms.
got a "System.IO.IOException: No space left on device"
tadamcz
added a commit
that referenced
this pull request
Aug 25, 2026
- test_comparator_primitives.py: the §2.3 primitive/builtin-constants invariant -- asserts every name comparator looks up in both environments (primitiveTargets + builtinTargets from the pinned Main.lean) resolves in the dataset toolchain, a cheap guard for comparator/FC-pin bumps. - test_comparator_security.py: cross-check properties against one live comparator sandbox. - cross_attempt_filesystem_poisoning: check #1's build swaps the Mathlib packages symlink for a poisoned dir; check #2's honest proof must still be accepted, proving reset-workspace.sh restored the pristine tree (§3.1). - disproof-shape verdicts (§4 delta): exact type_of% and explicit ¬(∀…) accept; the defeq-but-not-syntactic (h : ∀…) : False form rejects under Comparator's BEq match -- pinning that the prompt's fill-the-sorry guidance is load-bearing. Verified locally against the built image (4 passed). Process-survival: no test shipped. Empirically a setsid-detached solution-build child does not outlive the check in the Docker backend (tini + landrun teardown; landrun's inherited Landlock domain also confines any survivor to .lake). The Inspect #5034 per-service-restart gap remains the documented known limitation.
tadamcz
added a commit
that referenced
this pull request
Aug 25, 2026
The DAG-shaped text export + kernel replay have no importModules in the trusted process and no un-memoized rebuildExpr, retiring both unbounded-memory sources. mem_limit drops 50g -> 16g pending the §7 peak-RSS measurement.
tadamcz
added a commit
that referenced
this pull request
Aug 28, 2026
* initial plan
* fix universe handling in comparator migration plan
* codex plan updates
* Add comparator verifier image: Dockerfile stages, workspace reset, disproof certifier
The comparator stage replaces the compile+scorer pair (plan §3): the
Comparator binary is built at its own pinned toolchain (19e111e =
v4.34.0-rc2), lean4export at the rev comparator's manifest pins (cacf989)
rebuilt under the project toolchain (§2.2), and landrun from pinned source.
The builder registers the Challenge/Solution scratch libs before any lake
build and the runtime image stages /opt/pristine + reset-workspace.sh for
the read-only-rootfs + tmpfs hardening (§3.1).
extract_ranges gains certify_disproof, the vendor-time/CI certifier that
recomputes each appended disproof declaration's type via mkNot and asserts
BEq-identity with universe-parameter canonicalization (§4).
* Switch the scoring harness from SafeVerify to Comparator
- checker.py: SandboxComparator replaces SandboxSafeVerify (protocol renamed
ProofChecker). Spec.lean is extracted from the agent tar host-side with
tarfile, the workspace is reset per check, and one comparator invocation
under lake env replaces the compile/verify exec pair. Reference vs
submission attribution keys off comparator's own 'Building Solution' phase
marker: earlier failures raise, later ones score INCORRECT (plan §3.2).
- scorer.py: reads the agent's declared claim from the sample store, passes
the target's fully-qualified decl name to the checker, and records
checker-agnostic verifier_output metadata (replacing safeverify_report).
- solver.py: the submit tool gains the required claim argument
('proof' | 'disproof') recorded in the sample store; resource stages
renamed to the comparator stage names.
- prompts.py: the fill-one-sorry contract replaces the negateExpr contract
(the spec now states both the target and its .disproof; NEGATE_EXPR_SOURCE
deleted, plan §4).
- task.py: two sandbox configs generated directly, one per backend (docker
compose.yaml with read-only rootfs + size-capped tmpfs for the comparator
service; chart-native k8s values.yaml with emptyDirs, networkIsolated and
the CLUSTER_DEFAULT runtime pin), selected by the new sandbox_backend task
arg (plan §5). The compile service is gone.
- dataset.py: sample metadata gains decl_name (manifest override for targets
whose environment name carries a namespace prefix the id does not).
* Append the derived disproof declaration to every Isolated spec
Every committed Isolated/<id>.lean now ends with the mechanically derived
theorem <target>.disproof : ¬ (type_of% @<target>) := sorry
so one committed file is simultaneously the agent's sketch, the proof
challenge and the disproof challenge; the checker sends it verbatim for both
claims and only the configured theorem name differs (plan §4). The four
Erdos138 specs whose isolation cut dropped a trailing 'end' get it restored
first; the appended declaration always sits at top level under the target's
fully-qualified name.
- scripts/isolation.py: comment/string-aware scope scanner (namespace /
section / end tracking, «...» identifiers, multi-component ends) and the
shared append_disproof step, wired into all three generators.
- apn/data/oeis/samples.jsonl: decl_name overrides for the 3 targets whose
environment name carries a namespace prefix their id does not
(OeisA230507.*, A271099.*).
- Isolation suites: the structural gates expect the appended declaration, and
a new certification gate runs certify_disproof over every committed spec
(target/disproof pairing against the manifest + the independent mkNot type
check). Validated locally: all 928 specs certify, 0 failures.
- Dataset tests updated for the two-theorem/two-sorry sketch shape and the
decl_name metadata key.
* Port the checker/scorer/security test suites to Comparator
Re-derived from Comparator's model, not blind-ported (plan §6):
- test_checker.py: unit tests for extract_entry (host-side tar handling) and
SandboxComparator's reset -> stage -> run-under-lake-env orchestration, the
Building-Solution phase attribution (raise vs INCORRECT), and the scorer's
claim plumbing from the store.
- test_singlefile_proof.py: real-image acceptance incl. a single-file disproof
under the disproof claim; the helper-import guard now fails at the solution
build.
- test_lean_vuln_e2e.py: 14 soundness cases against the real image. The former
import_superset_violation and unsafe_constant_in_entry become documented
ACCEPT cases (extra imports / inert unsafe decls are sound under closure
replay); root_exec retargets to overwriting the lean4export binary and
doubles as the landrun canary; forbidden-axiom/weakened/missing/injection
rejects retained. All 14 verified locally against the built image.
- test_gold_proofs.py: gold proof adapted to the migrated spec shape (renamed
target + appended inert .disproof), scored via SandboxComparator on the
comparator sandbox.
- test_agent.py / test_tools.py: resource-stage names and the fill-one-sorry
prompt contract.
- scripts/summarize/task.py: COMPOSE_FILES_DIR -> SANDBOX_FILES_DIR rename.
* Add comparator invariant + cross-attempt/disproof-shape security tests
- test_comparator_primitives.py: the §2.3 primitive/builtin-constants
invariant -- asserts every name comparator looks up in both environments
(primitiveTargets + builtinTargets from the pinned Main.lean) resolves in
the dataset toolchain, a cheap guard for comparator/FC-pin bumps.
- test_comparator_security.py: cross-check properties against one live
comparator sandbox.
- cross_attempt_filesystem_poisoning: check #1's build swaps the Mathlib
packages symlink for a poisoned dir; check #2's honest proof must still be
accepted, proving reset-workspace.sh restored the pristine tree (§3.1).
- disproof-shape verdicts (§4 delta): exact type_of% and explicit ¬(∀…)
accept; the defeq-but-not-syntactic (h : ∀…) : False form rejects under
Comparator's BEq match -- pinning that the prompt's fill-the-sorry
guidance is load-bearing.
Verified locally against the built image (4 passed).
Process-survival: no test shipped. Empirically a setsid-detached solution-build
child does not outlive the check in the Docker backend (tini + landrun teardown;
landrun's inherited Landlock domain also confines any survivor to .lake). The
Inspect #5034 per-service-restart gap remains the documented known limitation.
* Close TODO bug #1: Comparator removes the SafeVerify memory blowup
The DAG-shaped text export + kernel replay have no importModules in the
trusted process and no un-memoized rebuildExpr, retiring both unbounded-memory
sources. mem_limit drops 50g -> 16g pending the §7 peak-RSS measurement.
* Document module-sensitive drift candidates; add sorry'd-def fixture; split CI
- scripts/comparator_drift.py + tests/test_comparator_drift.py: pin the 23
module-sensitive drift candidates (§3.3) -- 20 specs with a spec-local
private declaration, 3 with an anonymous instance -- detected by a
comment-aware scan of the committed specs. A dataset/Lean/exporter/Comparator
bump that adds or removes a candidate fails this fast pure-Python guard,
prompting the §7.5 pre-cutover comparator sweep (confirming the precise
reject subset is left to that sweep, not run in CI).
- test_comparator_security.py: add the statement-with-sorry'd-def fixture
(§7.3) -- a faithful proof of a theorem whose statement depends on a sorry'd
def is correctly rejected (sorryAx in the closure), documenting the defective
-formalization class.
- test_oeis.py: pin the 3 decl_name overrides (targets inside a namespace).
- checks.yml: split the comparator container tests into their own
comparator-tests job (each check builds Challenge+Solution against Mathlib,
tens of minutes) so the fast tests job stays ~quick; the pure-Python drift
guard stays in tests.
* Remove the orphaned vendored SafeVerify project
The comparator migration dropped the scorer Dockerfile stage that built
safe_verify, so apn/lean/safeverify/ is now dead: nothing in the Dockerfile,
apn/, scripts/, or tests/ references it. The disproof certifier
(CertifyDisproof.lean) replicates negateExpr's mkNot∘cleanupAnnotations
independently, so no live code depends on the vendored source. Removing it
per plan §5 (drop the scorer stage and the vendored-safeverify COPY/build).
* Add comparator smoke eval: build workflow, subset, Hawk config
- build-docker-images.yaml: build the comparator target (was scorer, which the
migration removed) so the verifier image reaches ECR.
- comparator_smoke subset: the 5 smallest-gold-proof proved_38 OEIS conjectures.
- configs/comparator-smoke.yaml: Hawk eval-set pinned to the apn package
@comparator (main still ships the SafeVerify apn), sandbox_backend: k8s
(chart-native values.yaml, since Hawk's compose converter rejects the docker
hardening keys), claude-fable-5 high-effort, $500/sample cap.
* Share one comparator sandbox across test_singlefile_proof cases
Each case previously brought up its own sandbox, so every test re-ran
docker compose build -- ~6 chances per run to hit a transient buildkit EOF
(observed on 15f6b1a's comparator-tests). All cases here are honest and
SandboxComparator resets the workspace before each check, so a single
module-scoped bring-up is safe; it builds the image once, mirroring
test_gold_proofs / the isolation suites, and shrinks the flake surface.
* Skip the one gold proof hit by module-sensitive drift (§3.3)
The gold sweep confirmed 35/36 published proofs verify under Comparator; the
lone rejection is oeis_A258667_conjecture_0 with 'Const does not match between
challenge and target A258667' -- a spec-local private def in the target's
closure mangles to different names in the Challenge vs Solution modules. This
is the documented fail-closed §3.3 limitation (the id is already in
comparator_drift.CANDIDATE_IDS), not a regression, and the plan ships no source
rewrite for it in v1. Skip it in the gold sweep (MODULE_DRIFT_STEMS, alongside
the resource-bound skips) and record the empirical confirmation in
comparator_drift. Removing it needs an upstream generated-name-drift fix.
* Add second smoke eval config (gpt-5.6-sol)
Same 5-problem comparator_smoke subset, sandbox_backend k8s, and $500/sample
cap as comparator-smoke.yaml, with gpt-5.6-sol (high reasoning effort) -- a
side-by-side end-to-end check of the Hawk/k8s pipeline with a second model.
* Add basic soundness floor: disproof-claim + sorry must reject
sorry_in_entry already covers proof-claim + sorry -> reject, but there was no
disproof-claim counterpart. sorry_in_disproof submits under claim=disproof with
the .disproof theorem left as sorry; Comparator targets tgt.disproof, whose
sorry pulls sorryAx into its axiom closure -> reject. Basic check worth having
explicitly given the change to the claim-based security model.
* Add disproof-path smoke evals (fable + gpt-sol)
The proof smokes only exercise Comparator's accept path for claim=proof. These
add the disproof counterpart: comparator_smoke_disproof is 5 OEIS conjectures
whose correct answer is a disproof -- each disproved and accepted in all 15
historical result runs (every model, from the LeanOpenProblems-results repo),
with the shortest published disproofs, so a strong agent can reproduce the
disproof and exercise the claim=disproof accept path end to end on Hawk/k8s.
None are §3.3 module-drift candidates. Two configs mirror the proof smokes
(claude-fable-5 and gpt-5.6-sol, high effort, $500/sample, sandbox_backend k8s).
* Add reject-path smoke evals (fable + gpt-sol, $50)
Third smoke pair, exercising Comparator's reject path with real agent attempts:
comparator_smoke_hard is 5 OEIS conjectures no model ever settled (attempted +
INCORRECT in all 15 historical result runs, every model/budget), i.e. extremely
hard/open. Paired with a low $50/sample cap so the agent burns budget on
attempts Comparator rejects. Two configs mirror the other smokes (claude-fable-5
and gpt-5.6-sol, high effort, sandbox_backend k8s); non-drift ids.
* Add red-team soundness Task: cheat to get Collatz accepted
apn_redteam_collatz hands the agent the apn codebase and explicitly encourages
it to cheat, then scores its Submission/Spec.lean with the real
SandboxComparator against a Collatz challenge (an open problem, so any accepted
proof/disproof is a genuine soundness break). Reuses the production scorer and
two-service sandbox, so accuracy == break rate; desired result 0.0.
The codebase handed to the agent is built dynamically at solve() time -- an
in-memory tar of the installed apn package's source (apn.__file__ walk,
excluding the heavy dataset and vendored docs), so it reflects the running
code, not a committed artifact. Prompt/framing loosely follows MirrorCode's
mc/red. Registered for Hawk and guarded by test_registry.
* Red-team: split into separate system + user prompts (react-only)
Like mc/red: a standing authorized-exploit SYSTEM prompt (the agent's role --
sanctioned sandbox, cheat/exploit/tamper encouraged, never fabricate success)
and a per-attempt USER prompt (the Collatz objective, the staged codebase, the
rules of engagement). Wired via react's AgentPrompt(instructions=...); the
red-team builds a basic react agent directly rather than touching the shared
build_agent.
* Red-team: trim the creative/persistent/fabricate lines from the system prompt
* Red-team: drop the single-channel assumption from the user prompt
The bullet asserted the agent's only channel is Spec.lean and the verifier
sandbox is untouchable -- an unnecessary (and self-referential) constraint on a
soundness red-team. Leave the attack surface open-ended.
* Red-team: drop per-file codebase descriptions from the user prompt
The specific descriptions of checker.py / Dockerfile / reset-workspace.sh etc.
can drift from the actual code; point the agent at the unpacked codebase and
let it read the current source instead of trusting a prose summary.
* Add red-team eval config (apn_redteam_collatz, fable, $1000)
* Add red-team eval config (gpt-5.6-sol variant)
* Strip private modifiers from OEIS isolated specs (comparator#58 drift)
A corpus census (scripts/comparator_drift.py, empirically confirmed by
compiling each candidate as module Challenge in the comparator image and
walking the target/.disproof closure) found 20/928 specs whose faithful
submissions Comparator falsely rejects: 19 from `private` name mangling
(_private.<Module>.0.*) and 1 from an anonymous-instance name collision.
Fix the OEIS cases at the source: scripts.isolation.strip_private removes
the `private` modifier (comment/string-aware, loud on unhandled shapes),
generate_oeis_isolated.py applies it before append_disproof, and the same
function rewrote the 14 committed OEIS specs (21 modifier sites; privacy
has no semantic effect beyond name visibility/mangling). The formerly
rejected oeis_A258667_conjecture_0 gold proof now passes end-to-end, so
MODULE_DRIFT_STEMS empties and the stem becomes the fix's regression
guard; _gold_submission mirrors the strip since the vendored gold files
stay verbatim.
Deliberately scoped to OEIS: the 5 erdos/fc100open private rejects and
the OEIS instance-collision case (oeis_341685_conjecture_0) remain
documented fail-closed limitations, pinned with the widened static net
(binder-form anonymous instances, deriving) in CANDIDATE_IDS /
CONFIRMED_REJECT_IDS and guarded by tests/test_comparator_drift.py.
Amend plan §3.3 accordingly.
* Compare stripped-private OEIS statements modulo the name mangle
The structural gate failed on 21702e5: it compares the isolated target's
raw-Expr type string byte-for-byte against the source's, and for the
samples whose statement references a formerly-private helper the constant
name now differs (`_private.0.products` in the still-private source vs
`products` in the stripped spec; the extractor elaborates under an
anonymous main module, which is also why both sides matched pre-strip).
The strings are otherwise identical, and the compile/certifier/oracle
gates and the gold sweep all passed.
Hardcode the exception: for exactly the 14 stripped samples
(STRIPPED_PRIVATE_IDS, pinned pure-python against the committed files so
a regenerate can't widen it silently), the structural and oracle
comparisons apply the test-local unmangle_private_names to both sides;
every other sample stays byte-strict. Verified by replicating the gate
in the generate image over all 14 + 2 controls: all pass.
* Replace migration smoke configs/subsets with one smoke_easy subset
The comparator-smoke eval configs and their three OEIS subsets (proof,
disproof, hard) were one-off migration-validation artifacts. Keep the
reusable piece as a single subset: smoke_easy, the 5 shortest-gold-proof
tsoukalas_proved_38 conjectures plus the 5 robustly false ones disproved
in every historical result run -- a quick end-to-end pipeline shakeout
covering both answer paths.
* Remove fable/gpt-sol red-team eval configs
The comparator-redteam.yaml (fable) and comparator-redteam-sol.yaml
(gpt-5.6-sol) launch configs were one-off runs pinned to the
giles-hawkbench-newstuff models branch; drop them from the tree.
* Give the red-team agent container internet access
The red-team adversary benefits from reaching the internet (fetch tools,
references, payloads) from its workspace. Grant it entirely in red-team
code: _sandbox_with_agent_internet post-processes the shared
get_sandbox_config output -- dropping network_mode:none (docker) /
networkIsolated:False (k8s) on the agent `default` service only -- and
writes a distinct redteam-internet.* file so the base config other tasks
read is untouched. The `comparator` verifier service stays
network-isolated, so soundness is still tested against the hardened
verifier; only the adversary's own box gets a network.
* Red-team k8s internet: grant world egress, not just un-isolate
The agent still had no network on k8s: the agent-env chart's egress is a
namespace-wide Cilium allow driven by the top-level
allowDomains/allowEntities/allowCIDR (empty == offline). Setting the
agent's networkIsolated:False only dropped its per-service deny; nothing
granted egress. Add top-level allowEntities:["world"] (opens the internet
and enables `*` DNS). The comparator keeps networkIsolated:True, whose
per-service egressDeny/ingressDeny wins over the namespace allow in
Cilium, so the verifier stays fully offline. Docker path unchanged.
* Simplify the comparator sandbox to the threat-model minimum
The security obligation reduces to one invariant: every check starts
with .lake bit-identical to pristine (landrun confines the untrusted
solution build to writes in .lake + /dev, and /dev is a sink no trusted
step reads). Mechanism now:
- Drop the read-only rootfs and size-capped tmpfs/emptyDir mounts from
both backend configs (they defended against out-of-model events;
disk exhaustion is fail-closed).
- reset-workspace.sh -> reset-dotlake.sh: rm -rf .lake and recreate it
from /opt/pristine (skeleton copy + packages symlink); the /tmp and
run/ wipes were outside the write grant. The checker recreates run/
itself before staging each check's inputs.
- Run the comparator image as a non-privileged user (comparator README
assumption 6, a stated precondition of its soundness guarantee).
/root becomes traverse-only 711 for the toolchain paths; a system
git safe.directory setting keeps lake from misreading the root-owned
pristine packages as "URL has changed" (and trying to re-clone them).
- Delete comparator-migration-plan.md; existing section references
resolve in git history.
Validated: non-root container smoke (reset, staging, lake env, both
binaries link, /root sealed, pristine unwritable) and an end-to-end
comparator check via test_comparator_security. Version bumped to
0.1.7rc1 so the image tags roll.
* Document why the sandbox configs stay backend-native (comparator#83)
k8s_sandbox can auto-convert compose files to Helm values, and with the
hardening keys gone almost everything we set is expressible through its
x-inspect_k8s_sandbox extensions. Record the one reason we still write
the values file directly: the runtimeClassName pin is silently unsound
to lose while comparator#83 is open (gvisor has no Landlock; landrun's
--best-effort disables itself without error), so it must not ride
through a translation layer. Revisit collapsing to compose-only once
the upstream fix makes a missing runtime fail loudly.
* Collapse the four pytest CI jobs into a matrix
The suites differed only in their pytest args; one matrix job keeps the
same check-run names (tests, comparator-tests, isolation, gold-proofs),
fail-fast off preserves their independence, and adding a suite is now a
matrix entry. Trim the multi-line job comments to one line each.
* Keep the stub Challenge/Solution artifacts in the pristine tree
Drop the find that stripped them: the reset copies them into each
check's .lake, where lake's content-hash traces make them inert --
staged files hash differently and rebuild, and reuse on a byte-identical
file is the same compilation. Also note on the stub build itself that it
exists to fail plumbing errors at image build rather than at the first
check.
* Resolve lean4export/landrun via comparator's PATH defaults
Install lean4export in /usr/local/bin beside landrun and drop the
COMPARATOR_* env indirection everywhere: the Dockerfile ENV block and
the checker's per-exec env dict (comparator's own defaults are PATH
lookups, its README-preferred setup). The vuln test keeps the attack
target's baked path as a local constant, and its comment now states the
current write-denial story (landrun + root-owned binary vs the
non-privileged user) instead of the removed read-only rootfs.
Validated by a rebuilt-image smoke (no COMPARATOR_* in env, PATH
resolution) and an end-to-end comparator check.
* Set only a memory limit on the k8s services
k8s defaults the request to the limit, so scheduling still reserves the
memory and the pod keeps Guaranteed QoS on it; CPU is compressible, so
the CPU request/limit knobs bought nothing. Also drop the extensions
aside from the backend-native rationale comment.
* Bump version to 0.1.7rc2
* Keep Kubernetes agent under gVisor
* Bump version to 0.1.7
* Remove resolved TODO
* Treat Comparator execution as one phase
* Score an exec output overflow INCORRECT instead of erroring the sample
Inspect's sandbox exec raises OutputLimitExceededError past its 10 MiB
output cap, and SandboxComparator.check caught only TimeoutError and
UnicodeDecodeError -- so a submission whose build printed enough (an
elaboration-time #eval loop, fully agent-controlled) escaped its
INCORRECT into an uncaught scoring error. Output volume is
submission-controlled for the same reason non-UTF-8 bytes are (the
trusted phases print a handful of progress lines), so map it to a
comparator_output_limit rejection like the other submission-attributed
exec failures.
* Build the gold-proof disproof line via disproof_declaration
The staging transform hand-formatted the appended disproof declaration
as an f-string literal that had to stay byte-identical to what
scripts.isolation.disproof_declaration produces (the generators use it
for every committed spec). Call the shared helper instead, so a change
to the disproof shape cannot leave the gold-proof staging appending a
stale spelling and rejecting every case for the wrong reason.
* Derive the redteam/primitives FC util import from the pin's profile
COLLATZ_SPEC and the primitive-constants probe hardcoded
'import FormalConjectures.Util.ProblemImports' while building against
fc_commit(OEIS_DIR)'s image -- the two remaining sites bypassing the
fc_profile registry that exists exactly to absorb upstream's util-module
rename. Both now render the import from
fc_profile(pin).util_module, so an OEIS pin bump past the rename can no
longer silently break the red-team task's challenge phase or fail the
primitives probe at compile time.
* Render the prompt's axiom list from checker.PERMITTED_AXIOMS
The prompt duplicated the permitted-axiom list as a local literal, with
only the checker comment 'Mirrored in the prompt' holding the two in
sync -- a change to one without the other would tell agents they may
build on an axiom the verifier rejects. user_prompt now renders from
the same tuple comparator_config enforces, and the checker comment
states the new relationship.
* Strip private modifiers from erdos isolated specs (comparator#58 drift)
Erdos101.erdos_101 -- a live bloom_selection member -- was a confirmed
false reject: its private linesWithPointsFor sits in the target's
closure, so the byte-identical Challenge/Solution builds elaborate to
different module-mangled names (_private.Challenge.0... vs
_private.Solution.0...) and Comparator rejects every faithful
submission. Adopt the OEIS generator's strip_private for the erdos
generator and apply it to the one affected committed spec (privacy has
no semantic effect beyond name mangling, and no downstream generation
step touches the line, so the committed edit is byte-equivalent to a
regenerate -- verified by running the strip over the whole corpus:
only this file changes). Erdos101 accordingly leaves
CANDIDATE_IDS/CONFIRMED_REJECT_IDS; the fc100open private case remains
the documented fail-closed limitation. The container isolation suite
re-certifies the spec (statement certificate, disproof certification,
compile) in CI.
* Test Comparator quoted declaration names
* Require explicit proof claims in postprocessing
* Treat Comparator output overflow as resource failure
* Drop comparator privileges per exec instead of a USER directive
Inspect does not play nice with images whose default user is non-root
(write_file's tee/mkdir run as that user, and k8s_sandbox implements
exec's user= switch with runuser, which only root may invoke), so the
comparator image now ends as root and the checker passes
user=COMPARATOR_USER on every exec against that sandbox instead. All
scoring work still runs as the non-privileged user; staged inputs
written as root land 0644 inside the comparator-owned run/.
* Bump version to 0.1.8 for rebuilt sandbox images
* Run the .lake reset as root to clear permission traps
The untrusted build owns what it creates under .lake and Landlock does
not govern chmod, so it can leave a nonempty mode-000 directory that a
comparator-user rm -rf cannot traverse -- turning the next check's
trusted reset into an infrastructure error instead of a verdict. The
checker now execs reset-dotlake.sh as root (rm is then immune to
permission traps) and the script drops back to the comparator user for
the pristine copy, so .lake stays comparator-owned. Regression-tested
end to end: a submission plants the trap via IO.setAccessRights and the
following honest check must still score.
* Use in-process IO for landrun-confined tamper snippets
The submission build runs under landrun, which blocks spawning a
subprocess, so the IO.Process.output lines in these #eval attacks were
silent no-ops. Drop the dead `rm` fallback in the packages-poisoning
snippet (removeFile already unlinks the symlink) and replace the
subprocess chmod in the exporter-tamper snippet with in-process
IO.setAccessRights. Both e2e cases still reject.
* Bump version to 0.1.9 for rebuilt sandbox images
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.