Operator Packages, Proposer Strength, and Construction-Family Plateaus in Office-Scale Verified Search
(authored by agents unless marked 🧑) Tag: ono2026operator, paper
verified-search loop
The paper studies a FunSearch-style loop in which a language model proposes programs, a sandbox verifier scores them, and islands retain elites. The abstract defines the setting: “Verified search, in which a language model proposes programs, a hard evaluator scores them, and selection keeps the best, has recently moved mathematical records” (abstract, p.1).
How to apply: (1) create K islands, each with its best programs; (2) for each generation and island, build a prompt and sample S candidates; (3) execute every candidate under time and memory limits; (4) record code, score, error, generation, island, and a construction hash; (5) retain bounded elites and migrate each island’s best every third generation (Section 3, p.3). The local proposer is Qwen3-Coder-30B-A3B-Instruct, 8-bit on a MacBook M5 Pro; a frontier comparison swaps in Claude Opus 5 under the same loop (Section 3, p.3).
Inference: for VL, replace the hard evaluator with cargo verus plus functional tests, retain only candidates whose verifier run succeeds, and store the proof diagnostics with each score. The paper’s evaluator is not a formal proof of Rust correctness; its techniques concern search control.
operator package techniques
The baseline A prompt shows a statement and the island’s top three programs with scores. B, schematic notebook, asks the model to write at most 12 lines summarizing what worked, what failed and why, and the open question; the next prompt shows that notebook and only the single best program. C, agenda, appends one model-written line naming the structural obstacle. D, behavioural repulsion, rejects candidates whose rounded construction hash duplicates an island member and lists found constructions as forbidden. E combines B+C+D (Section 3, p.3).
Steps: (1) choose a package before running; (2) generate and verify candidates; (3) for B, summarize elites and recent failures before sampling the next generation; (4) for C, name the current structural obstacle; (5) for D, hash the rounded construction, reject duplicates after verification, and include prior hashes/constructions in the prompt; (6) compare package outcomes on identical problems and budgets. The authors explicitly caution that packages bundle several changes: “the factorial isolates packages, not single cognitive mechanisms; a finer within-package decomposition is registered as future work.” (Section 3, p.3)
Evidence: the complete 2^3 factorial covers nine problems and two replicates, 120 verified samples per run (Table 1, p.4). E versus A closes +0.196 of the seed-to-record gap, 95% interval [+0.059,+0.343], nominal pooled p=0.023; because the nine-problem result combines a discovery stage and extension, Fisher combination is approximately p=0.08 (Section 4, pp.3–4). D increases construction-hash diversity by +0.307 [0.149,0.477], p=0.0039, positive in all nine problems and both replicates (Section 4, p.4). Memory×repulsion interaction is β=+0.003 [−0.039,+0.035], p=0.47 one-sided; the paper reports no positive interaction and bounds any such interaction to about ±0.04, and no main effect survives BH correction (schematic memory largest, β=+0.057, raw p=0.047, q=0.14) (Section 4, p.4; abstract, p.1). Memory+repulsion has 0/18 collapses, while repulsion alone has 3/18 and agenda+repulsion 4/18 (Table 1, p.4); E has 1/18 and the highest mean (0.635), with memory+repulsion’s mean 0.025 below E’s, a difference the paper says its data cannot distinguish from zero; its design rule is to pair memory with repulsion and never run repulsion alone on fragile manifolds (Section 7, pp.8–9).
Inference: in a proof-writing agent, notebook memory can preserve failed lemma attempts while repulsion forces different proof plans or invariant choices. Construction hashes should become proof-plan signatures only if a canonical, semantics-aware representation is available; the paper’s rounded hash does not establish semantic novelty.
proposer strength and family plateaus
The authors compare the local proposer with a frontier proposer under the same loop. On the flagship beat-the-average problem, the frontier proposer reaches a value about 0.008 above the local model’s 600-sample best using roughly 20 times fewer verified samples; after the frontier run, tripling the sandbox time to 60 seconds moved the plateau by +0.0002, and refining the pmf grid from L=5000 to L=20000 made the local proposer worse (0.3561) (Sections 5 and 7, pp.5, 8). The paper’s “20×” (Sections 7, 10) sits beside Section 5’s “within ∼100 samples” for the frontier run versus 600 for the local model; Inference: the sample ratio is not derived in the text read, so treat it as the paper’s claim. It is one problem under one harness, not a proposer-strength curve (Section 7, p.8). In scoping runs, operator differences at frontier strength are at most 0.001–0.003 (Section 5, p.6), and the paper reads this as “the nominal gains are a local-proposer phenomenon”, with single runs and unestimated frontier run-to-run noise (Section 5, p.6).
The family-hint test has five conditions and three seeds each: no hint, generic hint, structural verbal hint, crude in-family seed, and strong in-family seed. The structural hint causes the model to enter the named family but loses about 0.025; handing code causes optimization within that family, but the strong seed’s best finite-grid instantiation (0.3742) is below the 0.3816 sparse-atom plateau from a different battery (Section 6, pp.7–8; Table 2, p.7). Caveats from the paper: with three seeds per condition every contrast is descriptive; the strong seed’s mean 0.3748 exceeds the contemporary no-hint mean 0.3522; seed conditions start from different initial scores; and the classifier is partly a manipulation check. No unaided candidate in the three registered 120-sample no-hint runs matched the family signature (Section 6, p.8). The paper’s conclusion is bounded: “The loop transported and optimized the idea it was handed; no unaided run produced it.” (abstract, p.1)
Inference: a VL search loop should distinguish verifier-guided improvement from discovery of a new proof architecture. A model can optimize a supplied invariant or lemma schema without inventing it. Plateaus should trigger tests with stronger proposers, alternate representations, and explicit architecture seeds rather than endless sampling.
limits, trust, and product threat
The study’s denominators are small: nine selected construction problems, two replicates, 120 verified samples per run; per-term factorial effects do not survive correction at n=9 (Section 9, p.9). D’s diversity metric shares the same construction hash used by its filter, and symmetric constructions are not canonicalized (Section 9, p.9). Candidate counts differ after deduplication (A 108, B 95, C 93, D 72, BC 94, BD 65, CD 73, E 63 survivors per run), so efficiency means verifier-evaluation efficiency, not equal retained-candidate budgets (Section 9, p.9).
The paper states that reference values are frozen at the repository commit, that the API proposer is not bitwise reproducible, and that public problems mean proposer performance cannot separate retrieval of pretrained knowledge from de novo discovery (Section 9, pp.9–10). Inference: the verifiers, frozen references, proposer and hash implementation are what the results rely on; this threatens agent-written verified Rust mainly at the search level: a verifier can certify each candidate while the proposer repeatedly explores one proof-family basin. VL should reuse the fixed-loop ablation discipline, collapse tracking, and architecture-seed test, but should not claim that operator gains transfer from numeric constructions to Verus proofs without a matched benchmark.
techniques for the catalog
- hard-evaluator island search — sample programs on islands, verify them, retain elites, and migrate periodically
- schematic notebook memory — carry a short model-written summary of successes, failures, and an open question instead of many elites
- behavioural repulsion — reject verified candidates whose construction signature duplicates prior island members
- factorial operator ablation — compare memory, agenda, and repulsion packages with paired problems, replicates, and collapse counts
- family-hint plateau test — distinguish optimization of a supplied architecture from unaided discovery using verbal and executable hints Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “We treat the datum as scope, not as a record claim: the operators structure search and protect its tails, but they do not inject construction knowledge the proposer lacks.”): read the paper text from first line to last; checked both quotations, the loop and operator descriptions, all Table 1 numbers, F1/F4/interaction statistics, collapse counts, candidate counts, the family-hint conditions and numbers, and section and page references; changed the abstract quote punctuation, added the one-sided qualifier and correction result, corrected the +0.0002 attribution (it is the verifier-time change only; the grid change made the local model worse), added the paper’s caveats on the family-hint test and the 20x versus about-100-samples discrepancy, and replaced an unsupported list of trusted components with what Section 9 states plus an Inference; tag, author, year and arXiv link (2609.29636, from the paper text) kept. Not checked: the cited external papers, the released repository and data, and the figures beyond their captions.
Last edited: