Wonton Soup: Proof Structures Under Interventions

wonton-soup is our intervention harness for proof-search experiments. The question:

when we perturb a solver’s search process, does it return to the same proof structure, or settle into a different one?

We run wild-type and intervention sweeps over deterministic theorem samples, capture full search artifacts (*_history.json, *_mcts_tree.json, *_graph.json, *_comparison.json), and compare outcomes across seeds, tactics, providers, and backends.

1. What We’re Looking For

We treat proof search as a stochastic process over structured states.

• A perturbation can be a blocked tactic or tactic family, a seed change, or a policy/scheduler change.
• A response can be recovery to the same recurring proof shape or migration into a different proof-graph cluster, which the basin analysis treats as an attractor.
• The object of study is not only solve rate; it is the shape and stability of search trajectories.

This is why we log enough structure to replay and compare runs months later under fixed configuration.

2. Theoretical Mapping

Our intervention protocol applies three specific concepts from the Diverse Intelligence research program to formal proof search.

Search efficiency as a metric ($K$)

Following Chis-Ciure and Levin (2025), we treat intelligence as search efficiency in problem spaces, measuring the log-ratio between a random walk ($\tau_{blind}$) and our observed agent ($\tau_{agent}$): $$K = \log_{10}(\tau_{blind} / \tau_{agent})$$ A positive $K$ quantifies how many orders of magnitude our policy saves over a brute-force baseline.

Lesions and Rerouting

Zhang et al. (2024) demonstrate that decentralized systems, such as self-sorting arrays, can navigate around “damaged” components to reach a global goal, whereas our proof-search version blocks specific tactics or lemma families from a known solution path and measures whether the solver finds a different proof route or fails under the block.

Pattern Invariance (TAME)

The TAME framework (Levin, 2022) argues that behavioral structures, not just low-level mechanisms, persist under perturbation, and in wonton-soup we use Graph Edit Distance (GED) and basin analysis to determine whether proof search repeatedly settles into the same proof-graph clusters across different seeds and interventions.

3. Harness and Corpus Design

Corpus and run configuration are saved as explicit inputs to every comparison: corpus builds are manifest-backed, run configs are snapshot-pinned, and downstream analysis reads those inputs directly, keeping the baseline fixed while only the intervention changes.

We also separate validity from capability: a theorem can be well-formed for a backend even if the provider cannot solve it under budget, so Gate A checks that an item is structurally processable for the chosen backend and schema, whereas Gate B checks whether the provider and search policy can do meaningful work on that valid slice.

Deterministic selection (--sample with --seed) is how we ensure replayability, since rerunning later with the same corpus ref and selector inputs should recover the same theorem slice and comparable outputs.

Run-level schemas complete the provenance record with run_config.json, run_status.json, and summary.json.gz for postprocess, lake extraction, and cross-run audits.

What is fixed per comparison run

• Corpus reference plus build provenance (manifest.json, item ordering, hash identity).
• Selection procedure (--sample, --seed, --offset, --limit) and resulting theorem slice.
• Search budget and core execution knobs (mode, iteration budget, intervention declaration).
• Analysis inputs consumed by downstream tools (run_config.json, run_status.json, summary.json.gz, theorem subfiles).

4. Search Core: Centralized and Distributed MCTS

Both modes walk a tactic-conditioned state graph and use compatible log formats, so a mode switch changes execution dynamics without changing what downstream analysis reads.

Centralized mode is the structural baseline, where a single global selection loop owns frontier choice and expansion order, gives one policy view over one queue, and minimizes coordination effects, making it the simplest setup for studying proof families, basin structure, reroute versus collapse, recovery after intervention, and blind-relative efficiency.

Distributed mode adds multiple workers over that same proof-search space, where local agents operate over a shared frontier, inflight reservations reduce duplicate expansion pressure, and scheduling controls let us change coordination directly: block, delay, reroute, virtual loss, and depth/path bias interventions change who explores what and when.

Centralized MCTS maps the proof-search space for a theorem slice, whereas distributed MCTS changes how workers choose and reserve parts of that same shared frontier, testing whether solve behavior depends on one expansion regime or stays robust when worker scheduling changes.

Both modes emit compatible tree and trace files, so comparisons can use the same analysis path (*_mcts_tree.json, traces, run summaries) instead of requiring mode-specific postprocess logic.

How to read the figure: each worker lane represents local agent activity against a shared frontier, with reservations and scheduler policy shaping contention and handoff, while dense synchronized bands suggest strong coupling and staggered bands indicate looser parallel exploration.

5. Backend Families and Artifact Compatibility

We use a multi-backend harness to test whether behavioral patterns persist across backends or are implementation artifacts. A pattern that recurs across backend families with different proof objects and trace outputs is a stronger candidate invariant.

wonton-soup currently supports five execution backends:

• lean
• coq
• e
• vampire
• z3

Run-level schemas are shared (run_config.json, run_status.json, summary.json.gz), and run_status.json flags plus file-presence checks say which outputs each backend can actually produce, so downstream analysis does not silently compare missing or incompatible files.

This matters for mixed analyses: ged_search_graph is meaningful only when a true search graph exists, whereas external solver traces may map to ged_trace_graph or proof-object comparisons instead, and capability flags plus validity metadata keep those distinctions visible.

Backend Output Types (Typical)

Cross-backend comparisons are safest on shared run-level outcomes and explicitly labeled measurement types. Structure-level comparisons should be grouped by compatible output types, not collapsed into one undifferentiated score.

Showcase

We pin two recurring analysis views: attractor separation and blind-relative efficiency.

6. Metrics and Comparison Families

Each metric answers a different comparison question:

• K-style search efficiency (k_search_efficiency) from trace-derived blind nulls.
• Paper-style paired blind baseline (paper_k) from basin runs with --basin-blind.
• GED measurement types (ged_search_graph, ged_search_graph_soft, ged_proof_graph, ged_trace_graph) with explicit validity metadata.
• Trajectory comparison (divergence, reconvergence, recovery iterations).
• Basin analysis (solve rate, structure hash diversity, dominant basin frequency).
• Sheaf analyses (equivalence consistency and tactic-transform residuals).
• Cross-run lake exports for reproducible, cross-experiment aggregation.

Quick Metric Interpretation

K is reported as:

$$K = \log_{10}\left( \frac{\tau_{blind}}{\tau_{agent}} \right)$$

Example calibration: $K=\log_{10}(120/9)=1.12$ (about $13\times$ fewer attempts than blind).

• $\tau_{agent}$: attempted tactic edges until first terminal solve in the observed search graph.
• $\tau_{blind}$: expected attempted edges for a matched blind null policy over the same available tactic choices.
• $K$: orders-of-magnitude efficiency over blind (K > 0 is better than blind).

Two related outputs:

• k_search_efficiency: trace-derived null model from postprocess.
• paper_k: paired blind baseline from basin runs with --basin-blind.

7. Intervention Protocol

For each theorem, we first solve a wild-type run and extract the solution path $\pi = \{\tau_1, \dots, \tau_n\}$. We then run controlled lesions by blocking one tactic (or tactic family) from that path and rerun under the same budget and configuration.

This gives a clean comparison: same theorem, same search budget, one constrained action channel, repeated across all path tactics.

How to Read Attractor Analysis

• Panel A (GED matrix): pairwise structural distance between runs.
• Panel B (clustering + cut): where we place the cut determines attractor families.
• Panel C (basins): seed mass captured by each attractor family.

Interpretation: low GED + large shared basin mass implies robust proof structure; high GED with split mass implies genuine rerouting under intervention.

8. Log-Derived Vignettes

Vignette Gallery Player

A. Alternate Tactic at Same Structure

From a recent February corpus sweep:

• control_null: solved, normalized GED 0.00.
• block_intros: solved, normalized GED 0.45.
• block_split_ifs: unsolved, normalized GED 0.57.

Interpretation: one theorem shows both outcomes we care about, since some lesions reroute and recover whereas others collapse, and the split between GED=0 replicate and GED>0 reroute/collapse appears inside a single local intervention family.

B. Different Theorems, Different Intervention Patterns

From 2026-02-04:

• contrapositive: block contrapose! solved, normalized GED 0.67. Blocking contrapose! forces a forward proof via intro, flipping the intermediate goal from $Q$ to $\mathsf{False}$ before discharge.
• nat_succ_pred: block positivity solved, normalized GED 0.00. A local tactic swap: the proof keeps the same goal sequence but replaces an automated step with a direct lemma.
• iff_intro: block exact solved, normalized GED 0.00. A shallow reroute: the structure is intact but the terminal discharge uses a different tactic.

9. Observations and Results

Multistability in Proof Space

Proof search is not a single path: different seeds and interventions often converge to a small number of recurring proof shapes, suggesting that “the proof” is often a family of related trajectories rather than a single sequence of steps.

Competency through Constraint

Targeted damage to search sometimes improves global outcomes, as in cases like set_inter_self, where blocking the highest-priority tactics forces the system into routes that the unconstrained policy does not reach within budget, while the relevant parallel to biological morphogenesis is concrete: a local disruption can change the route without preventing the target pattern.

Search Efficiency

When $K > 0$, the observed search reaches a solve with fewer attempted tactic edges than its matched blind null, and the measurement is useful only after calibration to the available tactic choices: evidence that the policy is using useful structure in the action space, not a universal intelligence score.

Recurring Proof Families

When wild-type, blocked-tactic, and seed-variation runs converge to the same low-GED proof shape, the narrow claim is that this policy/corpus slice has a stable cluster of related proofs, with recurrence as the evidence; stronger TAME-style claims require the same family to survive broader backends, encodings, and null calibrations.

Next steps: cross-backend basin agreement tests, calibrated $K$ estimation with matched null models, and wider corpus and provider coverage.

This is a technical draft for the Specter Labs research blog. For a compiled dashboard of selected runs, visit the Wonton Soup Dashboard.