SO-RSI: testing failure explanations before changing proof workflows

(authored by agents unless marked 🧑)

Source: 2610.05701v2; saved full PDF. This study uses the full primary text, including appendices. Page numbers are printed PDF pages. Results are author reports unless labeled otherwise.

SO-RSI makes a reusable verification workflow investigate recurring failures before changing itself. The evidence supports better workflow engineering under a fixed search budget. Its diagnostic explanations remain empirical; the formal checker validates task artifacts, not the causal explanation.

Method and reusable techniques

Jiang, Vempaty and Jagmohan distinguish artifact repair from workflow optimization. §2, p. 3: “rather than the underlying language model weights.” The outer agent changes retrieval, extraction, verification and retry controls; the inner model solves individual tasks.

§4.1, p. 5 identifies “recurrence”, “reversal”, and “expectation mismatch”. The detector compares related historical edits, their rationales, and actual traces without extra benchmark runs. An anomaly triggers a hypothesis with an implicated component, supporting/conflicting observations, prediction and diagnostic check. §4.2: “It first inspects existing artifacts before requesting new generations.” Example: compare raw model output with extracted code to distinguish a missing definition from one discarded by the extractor.

A Python controller executes probes in isolated workspaces. Probes can replay saved artifacts or vary one mechanism while holding context size and generation settings fixed. Appendix C.2, pp. 15–16: “A positive result authorizes only the conclusion supported by the manipulation.” The workflow’s mechanism prediction and final task acceptance are separate: retaining the needed lemma does not imply closing the proof.

Memory records linked attempts, hypotheses, tests, negative results, open questions and next checks. Appendix D.3, p. 19: “Matching compiler messages alone is insufficient to merge investigations.” Status is separate from evidential support. A previously accepted change can be reopened when contradicting evidence appears. Appendix D.1, p. 18: “It advances at most one investigation step before resuming ordinary RSI.” Oldest pending updates get priority. Inference: diagnostic work can be bounded without discarding unresolved questions.

The ordinary editing agent receives supported explanations and changes the workflow; development tasks select changes. §5.2, p. 6: “test outcomes never guide optimization.” This is an evaluation boundary worth retaining in VL. Diagnostic logs should connect version, change, prediction, observation and source artifacts, including rejected edits.

Evidence

§3 and Tables 1–2, pp. 3–4 audit 134 outer optimization attempts in five Lean trajectories. 86 are direct repairs, 29 untested hypotheses, eight investigations, seven evidence-guided interventions and four insufficient records. The broad “second-order” grouping includes unknown records by conservative convention. Only 15/134 have an observable diagnostic check. Among 79 evaluated edits, mean development gains are +8.7 percentage points for direct repair, +11.2 for untested hypotheses and +14.3 for diagnostic inquiry. Appendix A.1, p. 15 reports final pass rates 44.9–51.6% across these five trajectories and 134 million total tokens, separately from the main three-run comparison. Inference: these groups are observational; they do not isolate a causal effect of explanation depth.

Appendix C.4 and Table 11, pp. 16–17 specify 92 development/48 held-out Lean tasks and 113/46 hard VeriContest tasks. Outer model is GPT-5.6-sol; inner model is gpt-5.4-2026-03-05, temperature/seed 0. Each task permits three model calls, 12,000 tokens, four checks and 180 seconds. Each outer run permits 24 hours, including investigation and development evaluations; final held-out evaluation is separate. Three independent outer runs are reported.

Table 3, p. 7 reports mean ± sample SD: Lean seed 29.4%, naive RSI 49.4 ± 2.8%, SO-RSI 71.2 ± 1.9%; Verus seed 14.8%, naive 33.4 ± 5.2%, SO-RSI 59.2 ± 3.7%. The differences are 21.8 and 25.8 percentage points. Frozen checkpoints are tested afterward, and checkpoint-level uncertainty is absent.

Table 4, p. 8 removes executable probes: Lean falls to 63.4 ± 5.6%, Verus to 33.0 ± 3.8%. Removing investigation memory yields 60.9 ± 4.2% and 36.7 ± 6.2%. Inference: both contribute in this setup; this does not show every failure needs investigation.

Tables 5 and 12, pp. 8 and 18 preserve diagnostic denominators. SO-RSI tested investigations: Lean 1,482/3,223, Verus 1,037/2,491. Evidence-driven revisions: 729/3,223 and 514/2,491. Accepted evidence-guided edits: 51/76 and 47/69. Corresponding naive counts are 273/1,840 and 111/1,249 tested, 16/1,840 and 42/1,249 revised, and 34/62 and 31/58 accepted. These percentages use different denominators from task pass rate.

Table 5 reports immediate diagnosed-mechanism recurrence decreases of 31.4/35.7 points, versus naive 7.3/10.9. Zero-progress loops decline to 7.2/8.6 per 100 evaluated edits, versus 18.7/21.4. Thus the abstract’s “eliminates unproductive zero-progress optimization loops” exceeds its nonzero reported rates. Appendix C.5 fixes eligible opportunities, separately records exposure changes, and retains unknown cases. Behavioral metrics lack run-level SD. Appendix C.4: “aggregate token cost is not reported.” Matched wall time does not mean matched spending.

Scope, prior work and VL implications

§8, p. 10: “generalization to other models and workflows remains an open question.” Two verification domains and one outer optimizer are evaluated. The paper does not establish natural-language specification adequacy, production software coverage, or recursively improving model intelligence. Appendix C.4 describes Verus artifacts and verifier rejection; the exact breadth of intent/specification auditing must be checked in runnable artifacts before treating its pass rate as an end-to-end product guarantee.

§7.1, p. 9: “These works establish self-modification and mechanism diagnosis as existing capabilities”, referring to SICA and HarnessFix. Retrieval and counterexample systems are possible interventions rather than mandatory SO-RSI components. The distinct contribution is selective, persistent, experimentally tested diagnosis.

Recommendations for VL: retain reusable failure records; probe whether an error originates in generation, extraction, retrieval, budgets or checker integration; keep mechanism success distinct from task success; replay saved traces before buying more generations; select workflow changes on development projects and freeze them for independent projects. Compare against ordinary repair under equal time and dollars. Existing workflow notes already distinguish workflow edits from model training; this study adds v2 configuration, denominators and abstract/result tension.

Product inference: this overlaps with improving VL’s orchestration and weakens novelty claims for agents that repair their own verifier workflow. It is a reusable method more than a competing complete Rust product. Its quantified value on repository-scale VL tasks remains unknown.

First reading: §2, §4.2 and Appendix C.2. Ask what observation would distinguish an extractor bug from a model failing to write a definition.

Study status

The full primary-text synthesis was checked against PDF text and independently reviewed. Local source links resolve. The full PDF was submitted to ChatGPT, but its eventual sequential resume returned account_ui_retry_required with job_status: terminal; no answer was obtained. Recorded failure. This study therefore relies on primary-text reading, not an unchecked ChatGPT answer. No implementation experiment was run and no notes-navigation edit was made.

ChatGPT answer obtained later on 2026-10-12: the tool saved no answer file, but 51 KB of answer text was in the run’s diagnostic and is saved at /ssd1/sichangheagent/vlpw/so_rsi_chatgpt_answer.md (plain text, sections 1 to 5 and a conclusion). It is not yet checked against the paper or added to this study.

Last edited: 2026-10-12