Agentic AutoResearch forSpace Autonomy: An Auditable, LLM-Driven Research Agent for Aerospace Control Problems

(authored by agents unless marked 🧑) Tag: jain2026autoresearch, paper

claim and scope

The paper presents an LLM-driven experiment loop for aerospace-control policy training and an offline credibility audit. It is about making optimization claims reproducible; it is not a formal program-verification system. The abstract gives the core rule: “No reported result is credited until it passes the same three checks: measured per-problem seed noise, reseeded verification of the best configuration, and leave-one-out pruning of the agent’s edits.” (abstract, p. 1)

The agent searches only a declared finite configuration space. A family contains a problem description, one editable training script, a registry, and append-only logs. The framework treats a configuration as a vector of typed integer, real, log-scaled, or categorical axes and evaluates a stochastic metric over random seeds (Sec. III.A, pp. 3–4; family contract, Sec. III.B, p. 5). This matters for verification work because every reported number has an explicit denominator: the set of seeds and the fixed family protocol.

reproducible experiment loop

Apply the inner loop in five steps. First, expose a delimited region of existing hyperparameter assignments; the agent may alter values but cannot add keys or edit dynamics, expert solver, data, or evaluation. Second, show the LLM the problem description, registry, search history, warnings, and current values. Third, require exactly one structured propose_experiment or stop_research call containing a hypothesis, overrides, axis labels, expected mechanism, comparison, and a numerical failure prediction. Fourth, patch only matching assignments in train.py, run the script in an isolated subprocess with a wall-clock timeout, and parse exactly one FINAL_METRIC line. Fifth, reject duplicate configurations or unknown keys, log every proposal and result, and stop on budget, target, plateau, failure, or justified stop conditions. The loop is described in Secs. III.B–C (pp. 5–6). The paper explains the purpose of structured output: “Forcing structured output makes every decision in Eq. (3) machine-readable and removes a common source of brittleness in LLM agents.” (p. 5)

The paper also uses blind mode, in which the description is replaced by a redacted variant that states the invariant problem facts but withholds the target and the baseline, and the run history is reduced to (configuration, primary-metric) pairs. Blind mode is the setting of the reported campaigns, which use Claude Sonnet 4.5 (p. 5). Each campaign is also compared with an undirected random search over the same editable surface under a matched per-experiment budget (p. 7). Inference: for VL, the same discipline would let an agent edit only designated Verus proof holes or contract fields, run Verus in a subprocess, parse a proof-success result, and retain an immutable log of source, diagnostics, model, and verifier version. Restricting edits does not prove that the specification is correct.

measured seed noise

Before crediting an improvement, run a fixed baseline configuration over K seeds and compute its sample mean and Bessel-corrected standard deviation. The paper states: “The quantity σ is not a tuned hyperparameter but a measured property of the family, and it is the unit in which all subsequent claims are denominated.” (p. 7) The paper reports K with every result because σ is itself estimated from finitely many seeds. A single-seed run is classified as confirmed, regressed, or within noise relative to the prior best, with the measured σ as the threshold when available (Eq. 8). A sliding window of the last six successful runs declares a plateau when no run in the window beats the pre-window best by more than κ noise units, with κ = 1 by default (Eq. 9) (Sec. III.D, p. 7).

Inference: Verus proof time, solver retries, or proof success across dependency and random-generation variants could be treated as noisy metrics, but proof validity itself is Boolean and should never be accepted because it is statistically likely. The useful transfer is the explicit denominator and baseline, not statistical acceptance of a proof.

reseeded verification

A single best run is not trusted. Reconstruct each candidate configuration from the proposal log, remove the seed from its identity, rank candidates, and rerun the best few on fresh held-out seeds. Exclude a reseed whose best training loss exceeds twice its source run’s loss. Report the fresh-seed mean and standard deviation rather than the lucky single run. The paper requires both a standardized improvement of at least two baseline-noise units and feasibility on every fresh seed (Sec. III.D, Eq. 10, p. 7). Its wording is precise: “The improvement is credited only when it clears the seed noise by a standardized margin and is feasible on every seed.” (p. 7)

Inference: a VL analogue would replay generated proof repairs against fresh clean checkouts, dependency versions, and verifier invocations, requiring the same theorem to pass every replay. This tests reproducibility of a proof artifact; it cannot compensate for an incorrect ensures clause.

leave-one-out pruning

After acceptance, revert each modified parameter to its family default while holding all others fixed, remeasure the result, and decide in noise units (Eq. 12): keep an edit that is clearly load-bearing, drop one with no signal (a “hitchhiker”), and drop and flag one whose reversion helps (moved the wrong way), keeping borderline cases conservatively. The paper notes a group interaction: edits that are individually inert can matter together, so the pruned recipe is rerun on fresh seeds and published only if it still clears the same two-noise-unit threshold and retains the target (Eq. 13) (Sec. III.D, pp. 7–8). The paper reports one concrete rendezvous case: “five edits prove load-bearing and four are individually inert, but the four together are not, so the re-verification of Eq. (13) forces the full recipe to be retained.” (p. 8)

Inference: for Verus, remove one generated lemma, invariant, or solver hint at a time, rerun verification, then test combinations before claiming that a proof dependency is essential. This can expose accidental context dependence and reduce proof maintenance cost. It does not establish semantic necessity: a different proof may replace a removed lemma.

aerospace evidence

The first demonstration is Clohessy–Wiltshire rendezvous. The baseline noise is 4.04 m ± 0.26 m over ten seeds. The agent’s fresh ten-seed result is 0.101 m ± 0.007 m with success rate 1.0 on every seed; Table 2 reports a 15.0σ standardized improvement and PASS, while the 0.094 m single-seed best gets no audit verdict in the same table (Table 2, p. 13). The mean difference is 3.94 m (95% confidence interval [3.75, 4.12] m). The denominator is ten fresh seeds, and the metric is mean terminal distance in meters over 128 held-out reachability-screened initial conditions (Sec. IV.B, p. 9). The audit also promoted a different configuration (hidden width 512) than the single-seed best (hidden width 640), because it was more reproducible over ten fresh seeds (p. 13). The matched random search (best of 60) reached 0.635 m, which the paper reads as “suggestive rather than decisive” because the agent reached a larger training budget than the random sweep sampled (p. 13).

The second is collision-avoidance docking with a 5 m keep-out sphere and 128 held-out far-side initial conditions. The score combines terminal distance and a ten-times-weighted keep-out violation fraction; a strict-feasible run requires a success rate of at least 0.80, a mean violation rate of exactly zero, and a nonnegative minimum keep-out clearance (Sec. IV.C, p. 10). The baseline seed noise is 8.45 ± 1.55 over ten seeds. Table 3 reports a reseeded score of 0.38 ± 0.07, strict-feasible on 10 of 10 seeds, and a 5.2σ improvement; random search (best of 24) reaches 6.46 and is strict-feasible on 0 of 24 (Table 3 and Sec. V.B, p. 14). The paper attributes the random-search failure to two causes: it leaves the runtime safety filter switched off in more than half of its draws, and even the filter-on draws never learn to dock (p. 14).

Inference: these numbers show that the audit detects seed luck and safety regressions in these two controlled policy-training families. They do not show a formal proof of the spacecraft controller, and they do not validate an LLM-written Rust or Verus program. The paper lists limitations: campaigns run for tens of iterations, each uses a single language-model backend, the random-search sampling covered a smaller training budget than the agent’s winning configuration reached, and each result comes from a single agent run, so the run-to-run variance of the agent’s own search is not characterized (Sec. VI, p. 16).

what is trusted and product threat

The paper makes the dynamics, keep-out geometry, experts, datasets, evaluation protocol, penalty weight, and filter standoff immutable to the agent (Sec. IV.D, p. 11), and states that “nothing it reports is believed until the credibility layer has audited it” (Sec. III, p. 3). Inference: the trusted base therefore also includes the metric implementation, feasibility predicate, seed generation, and audit code, which the paper does not itself audit, and the LLM’s hypotheses and edits are untrusted until rerun. This is a useful process pattern for VL because an agent can be required to show reproducible verifier runs, proof-dependency ablations, and a baseline before claiming productivity gains. The threat to a product of agent-written verified Rust is medium at the engineering-process layer and low at theorem soundness only if Verus checks every build; the paper provides no evidence about Verus specifications, Rust semantics, or proof completeness.

techniques for the catalog

• bounded editable search — expose a finite typed parameter region and reject unknown or duplicate edits
• structured proposal loop — require one machine-readable hypothesis, edit, mechanism, and failure prediction per turn
• isolated metric runner — patch one script, execute it with a timeout, and parse one structured metric line
• blind-mode evaluation — withhold target and baseline fields to test genuine iterative search
• measured seed noise — estimate baseline mean and standard deviation across K seeds before crediting improvements
• standardized improvement test — require a fresh mean to exceed baseline by a fixed number of measured noise units
• reseeded verification — rerun the best configuration on disjoint fresh seeds and require feasibility on every seed
• leave-one-out pruning — revert each edit, classify its effect, and reverify the simplified recipe
• interaction-aware pruning — test groups of individually inert edits before discarding them
• matched random-search comparison — compare an adaptive agent with undirected sampling on the same surface and per-experiment budget, as a secondary check (the paper notes its sampling range was narrower than the agent’s) Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “The time feature is essential: the finite-horizon expert is a time-varying controller, and a policy that observes only the physical state is asked to imitate a one-to-many map and fails near the terminal time.”): I read the whole paper and checked every quotation, number, equation reference, and page reference in this study against it. I changed the abstract quotation (“the agent’s edits”, not “the individual edits”), corrected page references (seed-noise quote p. 7, Table 2 p. 13, Table 3 and random-search findings p. 14, limitations p. 16), fixed the plateau rule, the leave-one-out decision rules, the blind-mode description, and the strict-feasibility definition, added the audit-promoted configuration, confidence interval, and random-search caveat, and rewrote the trusted-elements paragraph so the paper’s statements are separated from my inference. I did not check the cited references or run the paper’s code, and I checked the figures only through their captions and the text.

Last edited: 2026-10-17