Add doctest validation stage to Callable decoding - #694
Draft
eb8680 wants to merge 167 commits into
Draft
Conversation
* add example using object handles * coerce into the same format --------- Co-authored-by: Eli <eli@basis.ai>
This was referenced Jun 20, 2026
eb8680
force-pushed
the
eb-doctest-synthesis
branch
from
June 20, 2026 17:11
e1a8b8b to
1eaa685
Compare
… does not reproduce Answering "can this be closed at n=40 rather than n=200": yes, it can be tested at n=40, and the answer is no. Both corpora rebuilt so that 18 of 23 faithful claims carry an opaque invariant (`Valid bs`, `Wf p`), against 4 of 22 before -- close to upstream's 26 of 27, and built specifically to exercise the mechanism its benchmark actually tests: a faithful theorem whose conclusion is a conjunct of an invariant whose definition is never sent. Unconditional algebra moved to top-level helpers that no requirement maps to, so the audited theorems are thin corollaries carrying the invariant. 45 theorems, 43 claims, all compile. The invariant caveat upstream's prompts carry was added to the two rich arms. Five corpus configurations, twelve runs each: mixed, 4/22 invariant-carrying gpt-4o 7-0, p=0.016 78% invariant-carrying, with caveat none significant 78% invariant-carrying, no caveat none significant ...plus subtle traps, no caveat gpt-4.1 5-0, p=0.062 ...plus subtle traps and caveat (final) none significant Final numbers, exact McNemar on the paired items: model two-pass single-pass naive two-pass vs naive gpt-4o 81.4% 72.1% 81.4% 2-2 (p=1.00) gpt-4.1 88.4% 83.7% 83.7% 2-0 (p=0.50) gpt-4.1-mini 81.4% 76.7% 81.4% 1-1 (p=1.00) gpt-5.5 88.4% 95.3% 93.0% 0-2 (p=0.50) The one significant cell from the first configuration did not replicate under any of four later variants. Across ~40 tests at alpha=0.05, a single p=0.016 is what chance produces, so the previous commit's claim that "the published ordering holds" is withdrawn as a false positive. What survives: two-pass leads single-pass in 3 of 4 models and led in most cells throughout -- a directional trend too small to resolve at this n -- and the discriminating items are consistently the subtle weakenings, not the invariant projections. Concentrating the projection shape raised every arm together rather than separating them. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…g it The pack domain was a demonstration of the loop; this makes it a genuine attempt at the result in section 5.3, closing the four gaps that were flag-unreachable: - The artifact takes the paper's signature, pack(n, time_budget, current_best), and is handed the incumbent packing to polish rather than restarting each time. - It may use whatever numeric libraries are actually installed (scipy and numpy here), since the paper's winner is an LP over radii with dual-variable gradients driving a local optimizer over centres -- unreachable in the standard library. - The single-task Pareto objectives are Mechanism 3's run-distribution metrics (max, mean, stability, improvement rate over repeated runs), not one score. - The search evolves two modules on one shared frontier, the packer and a refiner instruction, which is Mechanism 2's leapfrogging. This needed nothing from the engine: a candidate is a PackSystem and the domain's proposer picks which module to mutate. Threading the incumbent makes an evaluation depend on more than its artifact, so optimize_anything gains a state_key by which a domain declares that and keeps the content-addressed cache honest. On the paper's n=26 instance, three runs from the grid seed at 2.1667 reached 2.6083, 2.6147 and 2.6359831 against the paper's reported 2.63598, in about ten evaluations. The winning artifact builds its constraints programmatically and warm-starts SLSQP from the incumbent -- an algorithm, not the published answer recited back, which was worth checking given that the optimum for n=26 is public. Also makes synthesized source recoverable when inspect.getsource cannot tokenize the block, which previously both killed a run and hid a winning artifact. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
One 2000-line file covering three domains asked the reader to hold all of it at once
to follow any of it. The algorithm and the domains now live apart:
optimization/library.py the paper's Algorithm 1, the Side Information types, the
Pareto machinery, the evaluation cache, the scoped worker
handler, and a generic report
optimization/packing.py circle packing, single-task search over code (5.3)
optimization/prompting.py prompt optimization, generalization mode (A.3)
optimization/kernels.py kernel instructions, multi-task search (5.2)
Each script is runnable on its own, carries its own CLI, and documents in its own
header what it does and does not reproduce of its section of the paper -- including
the measured numbers and the claims that did not reproduce. The library header keeps
the argument the example exists to make: that Side Information is an evaluator's typed
return value, that the paper's refiner stage is decode-time certification plus
TenacityRetryer, and that a loop generic in the artifact type never serializes
anything.
The split is mostly mechanical, with three changes to make it work: report() takes
`notes` and `render_artifact` callbacks instead of knowing about PackSystem, each
script defines its own Proposer agent holding only its own templates, and the shared
worker-model handler moves to the library.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…mark The hand-written election/delegation corpora did not reproduce ClaimCheck's result, and upstream's own per-item eval outputs show why: across every scored run its arms make zero false confirms and every error is a false dispute of a faithful lemma. The hand-written corpus measured the opposite regime -- traps subtle enough that mid-capability models missed them -- where two-pass, whose mechanism is a precision gain, has nothing to gain. Replace both with a transliteration of all five upstream domains: same 36 requirement/theorem pairs, same 27/9 split, upstream's requirement sentences verbatim, its lemma names in snake_case, and the three structural properties that carry its effect (opaque `Inv m`, conclusions that are themselves unshown named predicates, un-operationalized requirements). All 36 compile under Lean 4 + Mathlib, 0 errors, no `sorry`. The port reproduces the difficulty: six of gpt-4o's eight false disputes are on upstream's own weakest arm's error list. It does not reproduce the remedy. On gpt-4o the two-pass split is significantly *worse* than the naive prompt (72.2% vs 97.2%, 0-9 discordant, p=0.004), matching the reversal upstream itself reports on VERINA, the one non-Dafny corpus it tried. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…chanism A fresh-context review against the Dafny original found six divergences. Three mattered and are fixed: - The prompts did not reproduce upstream's asymmetry. ROUNDTRIP_COMPARE_PROMPT has no invariant caveat; NAIVE_PROMPT and CLAIMCHECK_PROMPT both do. This port gave all three a caveat plus a conclusion-side carve-out upstream has nowhere -- which helped exactly the arm and the items under test. Comparator now gets none, matching upstream. - contrast_pair_indices_valid dropped Dafny's `0 <= i` conjunct. Since Model is never sent, an auditor could not know the type was natural, making a dispute defensible on a `confirmed` item. Restored. - columns_are_unique used Mathlib's transparent `List.Nodup` where the sibling theorems use the corpus's opaque `NoDupSeq`. Restored. Also: statement_of now raises on an unbalanced extraction rather than silently truncating; two docstring errors corrected (a naive-opus row that spliced n from one results file and the error count from another; a claim that every arm catches every trap, which haiku-haiku.json refutes with 3 false confirms). Removing the caveat moved gpt-5.5 two-pass from 97.2% to 36.1% -- 23 faithful theorems disputed. The blind informalizer correctly rates `(h : Inv m) : 0 <= m` trivial, because a reader who cannot see inside Inv cannot tell whether the conclusion restates the hypothesis, and the comparator then disputes it. That points at batching as upstream's real rescue: its comparator sees a domain's pairs together, so the faithful lemma arrives beside its weakened twins. Stated as a hypothesis; implementing the batch would test it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…els.py A fresh-context review against the paper found the docstrings asserting things the code does not support, and two defects that inflated the kernel domain's headline. Measurement defects: - The kernel evaluator's side information contained "rescanning earlier values for every position is quadratic; carry running state" on every exception. That handed the proposer the exact lesson the domain then credited the search with discovering, and it was attached to unrelated exception types besides. The message now reports what happened and nothing more. - The cross-task transfer count was reported alone. On five tasks with a two-task minibatch, chance alone gives 3.0 -- precisely the "3 of 5" previously reported as evidence. It is now printed against that null. - --single-task kept the last of five runs and overwrote four fields, so the frontier, iteration count and best artifact shown were one task's. It now builds a real aggregate, and since five independent runs have no shared frontier, report() says so rather than inventing one. - The multi-task headline is a per-task maximum over the pool compared against a single seed candidate, so it cannot be negative. report() now prints the matched single-artifact comparison beside it, and the vacuous assert is gone. Re-measured with the hint removed, the paper's 5.4 finding does not reproduce: the single-task control ends ahead (+17.9% against +4.7%) on half the evaluator calls, and transfer is exactly at chance. The two arms' seed measurements differ by 12% for the same instruction on the same tasks, so the noise floor is wider than either effect -- recorded as a result that demonstrates the machinery and not a claim. False or unsupported statements, now corrected: that the plain-Python reference is "what the paper's unoptimized PyTorch baseline is" (KernelBench's is cuDNN/cuBLAS, so the speedups are not comparable quantities); that correctness is a floor the search stays above, contradicted eleven lines later in the same docstring; that a limitation section predicts the correctness cliff; that --selection best is an ablation the paper runs rather than an argument it makes; that every domain the paper reports has a target model; that a 2026-class model answers "any" short arithmetic question, used to justify dropping AIME when the paper measures the same worker model at 46.67% on it; and an invented "~45 and 15" for the AIME splits. Also removes dead code whose docstring misattributed a convergence measure to the paper, discloses the truncation of failing cases and the biased selection protocol, and seeds the timed input from a checksum rather than the task name's length. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… mechanism An adjudication of where the non-reproduction comes from found that both sides were contributing, and that two of the contributions were mine and undocumented. Replication defects, both fixed: - The `narrowed-scope` category description said "an extra hypothesis, or a less general shape, restricts the guarantee". Upstream's says only "lemma only covers a subset of cases the requirement describes" -- nothing about hypotheses. All 36 statements in this corpus carry `(h : Inv m)`, so that clause licensed the comparator to flag the one feature every faithful item has. Corrected; gpt-5.5 two-pass went 36.1% -> 77.8%. - SinglePassAuditor still shared a module with Comparator, so the comparator's system prompt carried the single-pass arm's invariant caveat via module source -- along with a comment announcing the experiment. The published 36.1%-vs-97.2% caveat ablation was measuring prompt position, not caveat presence. Withdrawn. Each arm now has its own module; a dump confirms each carries only its own text. Also withdrawn: the stated mechanism. It claimed the blind informalizer rates invariant projections "trivial" and the trivial rule fires. The transcripts show the back-translations are correct and rated moderate; the comparator disputes the `Inv m` hypothesis as narrowed-scope. Replaced with the transcript. Original-side findings added: the 69.4% arm is upstream's single-prompt text over a different transport, not a no-separation prompt -- at matched transport and run count, naive and single-prompt both score 86.1%. At matched model, upstream's batched two-pass on Opus (93.5%) loses to its per-item naive (94.4%). And upstream's own VERINA run is a per-item Lean replication of its claim that fails at 189 items. Clean numbers, arms properly separated: two-pass 84.0% pooled, single-pass 97.2%, naive 91.0%. The ordering comes out backwards, one cell significant (gpt-4o p=0.039). The claim is untested rather than refuted; the decisive experiment is named in the docstring. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ed code The docstring and comment blocks had accumulated a running account of this example's own development -- a "The leak" section, three withdrawn measurements, a tally of defects found and fixed. That belongs in git history. The header now states only what is true of the current file: what ClaimCheck claims, how the module boundary enforces the scoping, what the corpus is and how it differs from the Dafny original, what the measurement says, and where it is confounded. The one piece of history worth keeping is kept as an impersonal design rule -- the harness serialises a template's defining module, so the module is the confidentiality boundary and each arm owns its file. Numbers re-measured against the shipped code: two-pass 84.7% pooled, single-pass 97.9%, naive 91.7%. Two-pass last in all four models, gpt-4o significant at p=0.021. Also documents the run-to-run variance: repeating a cell at temperature 0 moved it 2.8 points, so cells are +/-3 and only the ordering is stable. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
A fresh-context review of this package against the paper found that
packing.py's headline did not support its claim, and that several
statements in all three scripts contradicted the code beneath them.
Measurement:
- packing.py gains --baseline: warm-started random-restart SLSQP with
analytic constraint Jacobians and no LLM anywhere in it, run for the
same packer wall-clock the search spends. At n=26 over 600s it reaches
2.6342924 in 13116 restarts -- past OpenEvolve@200 (2.6307) and within
0.0007 of AlphaEvolve. The search's 2.6359831 is therefore worth about
0.0017 over calling scipy competently, not 0.47 over a grid. The paper
runs no such control, so its own margin is unattributed too.
- cold_start_note runs the winning artifact once with no incumbent. With
current_best threaded through, a candidate's score accumulates every
earlier candidate's work, so the run's number is not the artifact's.
- numeric_toolbox no longer spells out the LP-over-radii-with-dual-
gradients recipe, and propose_packer no longer lists four more
strategies: those are the paper's findings, handed to the proposer in
the prompt asking it to find them. kernels.py loses the same leak in
two more places ("including degenerate inputs" to the worker, both of
the family's lessons named to the proposer).
The previously reported 2.6083 / 2.6147 / 2.6359831 were measured with
those hints present. A run under the current prompts went 2.1667 ->
2.6208 -> 2.6308 -> 2.6359831 in three accepted proposals before
wedging on iteration 5, so the hint was not load-bearing; both prompt
variants land on exactly 2.6359831. The kernels numbers still need
re-running and say so.
- trajectory_metrics drops to three objectives. "Improvement rate" as
best-minus-first over independent repeats measured the draw, not the
artifact; any scale-free "stability" is maximized by a deterministic
do-nothing, which was consequently unprunable. worst_score replaces
both.
- The kernels single-task control now runs the engine's single-task
mode. It was passing dataset=[task], which is multi-task mode with one
objective -- every tie non-dominated, selection collapsed to greedy --
so it differed from the treatment arm twice over.
- library.transfer_note counted a task whose winner was the unrefined
seed as a transfer while excluding it from the null, turning a run
with zero transfer into "4/5, above chance". Count and null are now
both over refined winners only, each with its own minibatch size.
- The SI ablation no longer pays for the generality check, whose
diagnostics it discards, on a domain budgeted in wall-clock.
Statements corrected:
- The WORKER_MODEL comment claimed the worker provider shadows
TenacityRetryer. It does not: it implements completion and
Template.__apply__, while the retryer intercepts call_assistant
between them. Both LLM domains have a repair loop their scores
include.
- artifact_key's "which is what makes the cache sound" held only for a
pure evaluator; it now names state_key as the condition.
- Three --selection help strings called "best" the paper's greedy
ablation; it is the alternative 4.3 argues against, not an ablation it
runs.
- PackSystem claimed the refiner recovers failed code mutations. The
accept gate never admits a zero-scoring candidate, so the refiner is
only ever handed a packer that already passed.
- module_note now reports per-module proposals, acceptances, mean gain
and the handover order, rather than only which survivors came from
where. There is no per-module score to plot, and it says so.
- packing.py's assert that the search beat its seed could not fail.
Also: dead `type Kernel` in packing.py, "correctness is the floor" where
the header says the opposite, and a note that _run_packer's SIGALRM is
best-effort and can be outlasted by a long C call.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Investigated why this two-pass arm underperforms the published one. A batched pass 2 -- a domain's requirement/statement/back-translation triples in one call, pass 1 left per-item and byte-identical -- moves the arm from 83.3% to 92.6% pooled (15-5 discordant, p=0.041): gpt-4o 72.2 -> 83.3, gpt-4.1 91.7 -> 94.4, gpt-5.5 86.1 -> 100.0, with no new false confirms. It fixes exactly the diagnosed items. So the per-item design, not Lean or the OpenAI models, is the dominant cause. The mechanism is not contrast against degraded siblings: removing all nine traps from the batch leaves the gain intact. What seems to matter is that `Inv m` is on every statement in a batch and stops reading as an extra hypothesis. Corroboration: upstream's own `bench-verina.js` runs two-pass per item and loses at N=189 with the same failure mode. Upstream treats its batching as throughput only. Also corrects a claim with the wrong sign. The matched-model comparison cited `opus-opus.json` (93.5%), but the shipped `INFORMALIZE_PROMPT` carries the literal hint unconditionally, so the matching run is `opus-opus-literal.json` (95.4%) -- which beats per-item naive-opus (94.4%) rather than losing to it. Ruled out with data: the `strength` field and the trivial rule. Dispute rate among faithful items is flat across strength ratings (trivial 15.4%, moderate 16.5%, strong 20.0%), and 14 of 18 false disputes come from `moderate` readings. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… the model auditing_single.py's docstring told the model that the invariant caveat below it was deliberate and load-bearing, and module source goes into the system prompt. Since that rule decides most of the benchmark's hard items, it was a thumb on the scale for one arm. Measured before removing it: worth at most one item (gpt-4o 97.2 -> 94.4, gpt-4.1-mini unchanged), so not an explanation for anything, but it does not belong in the prompt. Table re-measured with it gone. Records why the baselines here far exceed upstream's, which is a model effect and not a property of this port: upstream's own runs put the same NAIVE_PROMPT over the same 36 items at 86.1% on Sonnet 4.5 and 94.4% on Opus 4.6. Its published 86.1% baselines are Sonnet-4.5 numbers. On frontier models the benchmark saturates -- two of four single-pass cells are 36/36 -- so there is no headroom for the technique to demonstrate a gain. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Attributing them to model era does not survive the error sets. Upstream's
single-prompt arm on Sonnet 4.5 makes five errors, all faithful lemmas wrongly
disputed, and misses no traps. gpt-4.1-mini -- a small model -- makes two, both
traps waved through, and disputes nothing, getting all five of Sonnet's failures
right. Disjoint sets in opposite directions; a capability gap would produce
containment. So the items behave differently rather than one model being better.
The Sonnet-to-Opus +8.3pp inside upstream's own data is real but does not
transfer, and the claim that the benchmark saturates on frontier models is
withdrawn -- the smallest model tested already outscores upstream's baseline.
Leading untested candidate recorded instead: upstream sends the Dafny proof body,
almost always literally `{ }`, which reads as a vacuity cue on exactly the
invariant-projection lemmas it false-disputes. This port sends statements only.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
96.3% was the wrong comparator. Upstream's default informalizer is Haiku, and its
own runs show two-pass degrading as the informalizer strengthens: Haiku->Opus
97.2, Haiku->Sonnet 96.3, Haiku->Haiku 96.3, Sonnet->Sonnet 93.5, Opus->Opus
93.5. This file runs one strong model for both passes, so the like-for-like
figure is 93.5%, and batched it scores 92.6% -- 0.9 points off. Per-item
(~9 points, measured) plus the missing model split (~2.8 points, upstream's data)
account for the entire deficit.
That also explains why no single cause fits the whole table: capability helps the
one-call arms and hurts the blind arm. The remaining unexplained quantity is the
surplus in the other direction -- the one-call arms here beat upstream's by 5-11
points -- for which the missing `{ }` proof body is still the best candidate.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… live capture Checked the assembled system messages rather than the module source alone, by intercepting them during a run. Single-pass is clean. The naive arm was not: NaiveJudgement's docstring and the module docstring both named the guidance the arm is supposed to lack, including "the rule that a stronger theorem still matches" -- which decides delegate_non_existent_is_noop, one of only two items every upstream single-call arm gets wrong. Both neutralised; a re-capture shows zero occurrences of the taxonomy, the rule, or Comparison. Re-measured: naive 91.7% -> 93.1% pooled. The leak was real but was not inflating the arm, so it does not explain why these baselines exceed upstream's. gpt-4.1 gains three items and gpt-5.5 loses one, both within the +/-3 run-to-run band. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Only two-pass does. Both single-call arms are the same call -- audit(requirement, statement), one agent, one request, per item -- differing in prompt text, defining module and return type. So the two-pass comparison tests scope and the single-pass/naive comparison tests instruction and schema; the docstring previously described both as signature differences. Also notes what the return type does mechanically: its schema is rendered into the system message, so the weakening taxonomy reaches the model through the type rather than the prompt, and Comparison gates at decode time where NaiveJudgement cannot fail and never retries. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
A prompt-level comparison of the two single-call arms, against upstream's prompts.js and schemas.js, found the drift is in single-pass rather than naive. - naive is a near-verbatim port of NAIVE_PROMPT + NAIVE_TOOL. Unchanged. - single-pass is not a port of CLAIMCHECK_PROMPT. It keeps that prompt's framing, ordering and caveats, grafts on the two-pass arm's five-category taxonomy, and drops six of CLAIMCHECK_TOOL's nine fields -- including `informalization`, which forces upstream's arm to emit the back-translation, and `surprisingRestrictions`. Described accurately now rather than as a port. The gap between them is one sentence, not architecture. Appending "But do flag a hypothesis that restricts *when* the property holds" to the naive prompt and changing nothing else moves gpt-4.1-mini 31->34 and gpt-5.5 34->36, both landing exactly on single-pass. Three of the nine planted flaws are an added hypothesis; that sentence describes them. Ordering and the richer return type are not needed to explain the gap. Discloses an answer-key leak that is upstream's and faithfully reproduced: CLAIMCHECK_PROMPT's worked example `requires Inv(m); ensures m >= 0` is byte-for-byte its benchmark item CounterNonNegative, and the Lean example is counter_non_negative verbatim. Two mechanical corrections. The return type is delivered as response_format, not in the system message, so Comparison's field descriptions never appear in the single-pass prompt -- the previous claim that the taxonomy reaches the model "through the type rather than the prompt" was backwards. And the retry asymmetry does not only cost the structured arms: a successful retry is a free turn naive cannot get, and successful retries are unrecorded. Records the ~14k framework preamble as an untested candidate for the baseline surplus over upstream. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
CLAIMCHECK_PROMPT and NAIVE_PROMPT are separate prompts behind separate flags (roundtrip.js:208 and :285) and score identically on the same 36 items, 86.1% each. So upstream's structured single prompt buys nothing over its own naive baseline, where the port measures +4.1 points. The cause is the error direction already documented above. Every upstream arm catches all nine traps in every run, so the "flag a hypothesis that restricts when" clause has nothing to fix there. Here naive misses three added-hypothesis traps, so the same clause is worth three items. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
single-pass was the one arm that was not a faithful port of anything -- it kept CLAIMCHECK_PROMPT's framing and caveats, grafted on the two-pass arm's taxonomy, and dropped six of CLAIMCHECK_TOOL's nine fields. Its contrast with naive also turned out to measure a single caveat sentence rather than anything structural. Little is lost by removing it. Upstream's CLAIMCHECK_PROMPT and NAIVE_PROMPT score identically on the same 36 items (86.1% each), so naive is the correct comparator for the published middle rung and the ~10-point published gap is two-pass against this floor. What remains is one structural contrast: two agents and two calls with a pass 1 that has no parameter for a requirement, against one call that sees both. Verified that removing it does not perturb the survivors: both remaining system prompts capture byte-identical to the runs the table reports, so the numbers stand unchanged. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The header had grown to 383 lines against 90-100 for the sibling examples, most of it narrating decisions and their reversals rather than describing the example. Now 185: the problem, the four ways the code enforces the scoping claim, the corpus, the ablation, the results with their mechanism, the divergences from the source, why the corpus is a port, and how to read the numbers. No result is dropped. The batching measurement, the informalizer-strength comparison, the transport artifact in upstream's bottom rung, and the open question all survive in compressed form. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Six runs at the paper's instances, one arm each, gpt-5.5 proposing.
Machine was not idle: the packing and kernels arms ran concurrently.
packing.py, n=26 --time-budget 20 --budget 10:
default (Pareto, SI) 2.6359831 3/10 accepted, 15 evals
--no-side-info 2.6319369 2/10 accepted, 19 evals
--selection best 2.6317302 5/10 accepted, 17 evals
- Table 4's 93.96% does not reproduce: score-only reaches 99.85% of
the SI arm. The first accepted proposal in every arm jumps from the
grid to a warm-started SLSQP restart loop within 0.005 of the best
number any arm reaches, so the ablation has almost nothing left to
measure.
- --selection best proves nothing about 4.3. Every run ends with one
candidate on the frontier and every accept prunes exactly one: max,
mean and worst move together for near-deterministic packers, so
dominance is total and Pareto selection chooses from a pool of one.
- The default arm's first accepted proposal scores 2.6342924, which is
the no-LLM control's number to the digit. Total search margin over
scipy: 0.0017.
- cold_start_note earns its keep. The default winner scores 2.6359831
cold, inheriting nothing; --no-side-info's scores 2.5416318 cold
against a run number of 2.6319369, so 0.09 of that arm's headline is
other candidates' work.
- The default winner hardcodes random.Random(15) for n == 26. No
coordinate table, but the zero cold-start gap is partly a tuned
constant replaying its own restart sequence.
- generality_check gives the packer 0.5s against the run's 20s, so the
winner returns its fallback and the diagnostic reports "a table
rather than an algorithm" every iteration -- a false negative fed to
the proposer. Documented, not changed; at 20s the same artifact
scores 2.7827752 at n=29 against the grid's 2.4166667.
kernels.py, --budget 10:
multi-task, 10 iters 1.385 -> 1.569 40 evals, 10 proposals
best single artifact 1.385
control, 2 iters/task 1.328 -> 1.396 15 evals, 10 proposals
control, 7 iters/task 0.999 -> 1.638 40 evals, 35 proposals
- 5.4 goes whichever way the budget is counted. Iteration-matched,
multi-task leads and spends 2.7x the evaluator calls. Evaluation-
matched, the control leads and spends 3.5x the proposer calls. No
setting matches both: a multi-task iteration buys a five-task
evaluation, a single-task iteration buys one, and both buy one
proposer call.
- Noise swallows it regardless. The same seed string scored 1.385,
1.328 and 0.999 on the same five tasks, because the worker rewrites
the kernel each time and on one draw never produced a usable zscore.
- The multi-task arm's best single artifact is 1.38474, exactly the
seed's mean: no instruction the search wrote beat the one it started
from, averaged over the tasks. That arm's whole gain is composition
across four candidates, each best at one or two tasks.
- Transfer 3 of 4 refined winners against a 2.4 null. The corrected
statistic excluded the seed winner and said so.
Docstrings in both files now report these arms and drop the figures
measured under prompts that no longer exist.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`formalization.py` (LEAP: natural language to a proved Lean theorem) and the ClaimCheck auditing example (does the proved theorem mean the requirement?) are two halves of one topic, and neither is about the paper-writing pipeline the rest of `autoresearch/` implements. They now sit together in their own topic folder, alongside `basics/` and `reasoning/`. auditing.py's deferred import of the Lean kernel follows to docs.source.llm_examples.autoformalization.formalization; the two files are siblings again, so the prose references to `formalization.py` stay unqualified. `autoresearch/` keeps illustration, implementation, investigation, review and writing. Verified from the new location: both files typecheck, formalization.py --check-toolchain passes, and auditing.py --verify-only still drives the real Lean toolchain through its sibling (36 theorems, 0 errors, no `sorry`). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
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
2 participants
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.
Addresses #433 #701 #700 #697 #493 #513 #526 #549 #610 #590 #699 #581 #605 #603 #573 #576 #577 #586 #660