PaperlayerView exact revision on arXiv

Source-linked AI summary

Second-Order Problem Solving for Recursive Self-Improvement in Formal Verification

Yuxuan Jiang, Aditya Vempaty, Ashish Jagmohan

arXiv:2610.05701v2cs.AI

TL;DR

Standard RSI can patch immediate symptoms without investigating the mechanisms behind recurring failures. SO-RSI detects structural anomalies and uses diagnostic investigation and persistent evidence to guide workflow edits; it improves final held-out pass rates over Naive RSI in Lean and Verus-based code generation under matched 24-hour budgets.

  • Problem

    First-order RSI may leave underlying causes unexplored, allowing similar failures and conflicting fixes to recur.

    Source: §1 · p. 1

  • Method

    SO-RSI monitors recurrence, opposing edits, and expectation mismatch, then uses targeted probes and persistent investigation evidence to guide workflow changes.

    Source: §1 · pp. 2–3, §4.1 · p. 5, §4.2 · p. 5

  • Results

    21.8 and 25.8 percentage points: SO-RSI improves final held-out pass rate over Naive RSI on Lean and Verus-based code generation under the same 24-hour outer budget.

    Source: §8 · p. 9

  • Takeaways & Limitations

    Direct repairs remain useful, while recurring or conflicting outcomes warrant investigation of the workflow mechanism that produces them.

    Source: §8 · pp. 9–10

    The evaluation covers two formal-verification domains and one outer improvement model, so generalization to other models and workflows remains open.

    Source: §8 · p. 10

Abstract

from arXiv · show

Recursive self-improvement (RSI) enables agents to iteratively optimize their workflows via execution feedback. However, standard RSI typically operates as a first-order optimizer: it repeatedly patches surface-level parameters in response to immediate failure symptoms, often leading to trial-and-error thrashing without resolving underlying mechanisms. To address this limitation, we introduce SO-RSI, a framework that elevates workflow optimization to a second-order diagnostic inquiry, investigating why failures occur before committing to structural interventions. SO-RSI passively monitors execution traces for three structural anomalies (recurrence, opposing edits, and expectation mismatch) to trigger targeted mechanism investigations. By executing lightweight diagnostic probes and maintaining persistent inquiry memory across RSI rounds, SO-RSI accumulates causal evidence to guide systematic workflow edits rather than parameter patches. Across Lean 4 proof generation and Verus-based verifiable code generation, SO-RSI improves final held-out pass rates over Naive RSI by 21.8 and 25.8 percentage points under matched 24-hour search budgets. Behavioral analyses further confirm that SO-RSI substantially suppresses failure recurrence and eliminates unproductive zero-progress optimization loops.

1 INTRODUCTION

First-order RSI can restore progress with quick fixes, but unresolved causes leave agents cycling through recurring failures and opposing edits. SO-RSI investigates workflow mechanisms before guiding structural changes, improving final pass rates over Naive RSI in Lean and Verus-based verification.

1 INTRODUCTION

  • First-order RSI can oscillate between increasing and decreasing lemma-retrieval counts because it treats poor ranking as a parameter-tuning problem.A large window adds noise, while smaller windows can omit a key lemma; reranking and filtering address that trade-off.Source: §1 · p. 1, Figure 1 · p. 2
  • Quick fixes may restore immediate progress, but unresolved causes can bring back similar failures and conflicting prescriptions.The paper situates its inquiry question alongside prior RSI work on reflection, diagnosis, and workflow modification (Robeyns et al., 2025; Chen et al., 2026).Source: §1 · pp. 1–2
  • 21.8 and 25.8 percentage points: SO-RSI improves final pass rate over Naive RSI on Lean proving and Verus-based code generation under the same 24-hour budget.Ablations show that executable probes and persistent investigation memory both contribute to the gains.Source: §1 · p. 2
  • SO-RSI monitors recurrence, opposing edits, and expectation mismatch to trigger mechanism investigations whose accumulated evidence guides workflow improvements.The framework integrates selective detection and persistent investigation into continuing RSI.Source: §1 · pp. 2–3
  • The diagnostic analysis documents reversals in RSI decisions and audits evidence for their causal explanations, while the empirical motivation quantifies inquiry depth and unproductive editing across 134 attempts.The introduction frames the central gap as plausible explanations that are not explicitly verified before workflow edits.Source: §1 · p. 2

2 PROBLEM FORMULATION

The paper distinguishes repairing a task artifact from improving the reusable workflow that produces it. It frames workflow improvement as maximizing held-out task success within a research budget, using trace evidence to identify and validate edits.

2 PROBLEM FORMULATION

  • Outer RSI improves the reusable workflow procedure, while the inner loop repairs a specific proof or program artifact using compiler feedback.Workflow components include generation, lemma retrieval, verification, and retry policies; adopted edits must be validated on development benchmarks.Source: §2 · p. 3
  • A symptom is a visible trace failure, whereas a mechanism explains how the workflow produces it and can be checked with a diagnostic probe.For example, an extractor may discard a generated definition, making extractor repair more appropriate than adding another definition.Source: §2 · p. 3
  • The objective is to maximize held-out task success subject to a research budget that includes investigation, editing, and evaluation costs.Only development tasks guide improvement; token use, verifier calls, wall time, and failure recurrence are tracked.Source: §2 · p. 3

3 FROM OBSERVED OUTCOMES TO SUPPORTED EXPLANATIONS

The section operationalizes inquiry depth and examines how RSI edits affect proof success. Direct repairs dominate the audited attempts, while diagnostic checks are uncommon; repeated zero-progress work is concentrated in direct repair.

RQ1: How often does RSI move beyond direct patching?

  • The inquiry labels distinguish direct repair (F), mechanism hypothesis (H), mechanism investigation (I), evidence-guided intervention (G), and insufficient information (U).Only F counts as first-order; U is grouped on the second-order side to avoid inflating the first-order count.Source: §3 · p. 3
  • Only 15 of 134 attempts (11.2%) include an observable diagnostic check, and only 15 of 44 attempts articulating a mechanism test it.Direct repair accounts for 86 attempts (64.2%); the permissive second-order group also includes untested hypotheses and insufficient records.Source: §3 · p. 4, Table 1 · p. 4

RQ2: What gains does RSI achieve, and when does further patching become unproductive?

  • Diagnostic inquiry (I/G) achieves the largest average improvement per evaluated edit, while direct repair also delivers useful gains and regressions occur in every group.The comparison covers 79 evaluated edits from 130 F/H/I/G attempts; gain is pass-rate change relative to the edit’s actual parent.Source: §3 · p. 4, Table 2 · p. 4
  • Eight of nine zero-progress loops assigned to the direct-repair groups contain only F edits, which repeatedly change the workflow without retaining performance or cost benefits.The findings motivate selective escalation when repeated patches fail to produce durable progress, while retaining efficient direct repairs.Source: §3 · p. 4

4 SO-RSI: SECOND-ORDER PROBLEM SOLVING FOR RSI

SO-RSI redirects ordinary workflow optimization to investigate the mechanisms behind anomalies before making systematic workflow changes. It combines selective detection, diagnostic inquiry, and evidence-guided intervention, then returns revisions to ordinary RSI for evaluation.

4 SO-RSI: SECOND-ORDER PROBLEM SOLVING FOR RSI

  • The framework uses anomaly-triggered mechanism investigation to guide workflow changes, then returns those changes to ordinary RSI for evaluation.The investigation stage forms and tests hypotheses, consults external knowledge when needed, and retains findings across RSI rounds.Source: §4 · pp. 4–5, Figure 2 · p. 5

4.1 LIGHTWEIGHT DETECTION OF IMPROVEMENT ANOMALIES

  • SO-RSI detects recurrence, reversal, or expectation mismatch in RSI edits and routes flagged records to investigation while ordinary RSI continues when no anomaly is detected.Detection compares logged workflow versions, edits, and rationales with relevant prior traces.Source: §4.1 · p. 5

4.2 MECHANISM INVESTIGATION (I)

  • Mechanism investigation forms non-exclusive workflow-cause hypotheses from historical attempts, with testable predictions and checks grounded in relevant documentation when needed.Targeted probes inspect existing artifacts or test alternatives; findings are retained across rounds so related investigations can resume from prior evidence.Source: §4.2 · pp. 5–6

4.3 EVIDENCE-GUIDED IMPROVEMENT (G)

  • Evidence-guided improvement supplies supported explanations and probe results to the RSI editing agent, which produces a workflow patch addressing the investigated cause.The revised workflow returns to ordinary RSI for evaluation; only accepted edits update the workflow.Source: §4.3 · p. 6

5 EMPIRICAL EVALUATION

Across Lean proof generation and Verus-based verifiable code generation, SO-RSI achieves higher final held-out pass rates than Naive RSI under matched 24-hour budgets. It remains ahead at reported post-initialization checkpoints, though both methods have temporary regressions.

5.1 EXPERIMENTAL SETUP

  • Lean uses 92 training and 48 test problems, while Verus VCG uses 113 training and 46 test problems; each outer RSI run has a 24-hour budget.The reported results average three independent runs.Source: §5.1 · p. 6

5.2 OVERALL PERFORMANCE AND IMPROVEMENT TRAJECTORIES

  • 71.2% on Lean and 59.2% on VCG are SO-RSI’s final pass rates, exceeding Naive RSI by 21.8 and 25.8 percentage points, respectively, under the same 24-hour budget.Pass rates are means over three independent runs; the comparison is on held-out verification performance.Source: §5.2 · p. 6, Table 3 · p. 7
  • SO-RSI remains ahead of Naive RSI at every reported checkpoint after initialization, although both methods show temporary regressions.Figure 3 plots reported pass rates from the initial workflow through intermediate checkpoints to the final result.Source: §5.2 · p. 6, Figure 3 · p. 7

6 ABLATION STUDY

The ablations test whether executable probes and persistent investigation memory contribute to SO-RSI’s gains. Behavioral analyses examine how investigation affects workflow edits and repeated work.

6 ABLATION STUDY

  • Removing probes lowers final pass rate by 7.8 points on Lean and 26.2 points on VCG; removing persistent memory lowers it by 10.3 and 22.5 points, respectively.Both variants share the full method’s research budget; without probes, VCG performance falls close to the Naive RSI baseline.Source: §6 · p. 7, Table 4 · p. 8

6.1 ANALYSIS OF IMPROVEMENT BEHAVIOR

  • SO-RSI tests mechanism explanations in 46.0% of Lean investigations and 41.6% of VCG investigations, versus 14.8% and 8.9% for Naive RSI.Evidence-driven revisions reach 22.6% and 20.6%; accompanying G edits have mean development gains of 9.8 versus 4.4 points on Lean and 12.0 versus 5.2 points on VCG.Source: §6.1 · pp. 7–8, Table 5 · p. 8
  • SO-RSI reduces mechanism recurrence by 31.4 points on Lean and 35.7 points on VCG, while zero-progress loops fall from 18.7 to 7.2 and from 21.4 to 8.6 per 100 evaluated edits.Removing either probes or memory weakens both outcomes; the memory ablation still executes many checks but revises fewer decisions and achieves smaller recurrence reductions.Source: §6.1 · p. 8
  • The analyses connect more frequent mechanism testing with better intervention outcomes and less repeated work, while Naive RSI also performs some diagnosis and reduces recurrence.Together with the ablations, the evidence supports selective investigation as a complement to direct repair.Source: §6.1 · p. 8

7 RELATED WORK

Related work establishes self-modification, mechanism diagnosis, and solver-improvement methods as existing capabilities. SO-RSI differs by investigating workflow mechanisms when repeated improvement attempts produce unresolved patterns.

7.1 RECURSIVE SELF-IMPROVEMENT AND WORKFLOW DIAGNOSIS

  • SICA edits and evaluates its implementation, while HarnessFix diagnoses harness mechanisms and validates targeted repairs; SO-RSI investigates recurring failures, opposing edits, and unmet expectations across rounds.SO-RSI tests explanations before guiding another workflow edit.Source: §7.1 · p. 9

7.2 SECOND-ORDER PROBLEM SOLVING

  • SO-RSI adapts the distinction between immediate workarounds and addressing processes that produce recurring failures, focusing on what the agent investigates and tests rather than edit size.It retains ordinary repairs while selectively investigating workflow mechanisms behind unresolved patterns.Source: §7.2 · p. 9

7.3 AGENTIC FORMAL VERIFICATION

  • Retrieval and counterexample methods improve solver information, whereas SO-RSI uses diagnostic evidence to determine which workflow mechanism to revise.Retrieval and counterexample reasoning are possible interventions, not components prescribed in advance.Source: §7.3 · p. 9
  • Other context-sensitive approaches target service-event prediction or task-specific adaptation, while SO-RSI investigates patterns across workflow edits and tests mechanism explanations.The related work also notes that more elaborate AI-generated theories do not necessarily predict empirical results better.Source: §7.3 · p. 9

8 DISCUSSION AND CONCLUSION

SO-RSI applies second-order problem solving to outer RSI in Lean proof generation and Verus-based code verification. The discussion reports improved held-out pass rates and behavioral changes, while the operational appendix specifies classification and measurement boundaries.

8 DISCUSSION AND CONCLUSION

  • Under the same 24-hour outer budget, SO-RSI improves final held-out pass rate over Naive RSI by 21.8 percentage points on Lean and 25.8 points on VCG.Ablations indicate that executable probes and persistent investigation memory both contribute to these gains.Source: §8 · p. 9
  • Behavioral analysis links the gains to more mechanism testing, more evidence-driven revisions, and stronger intervention outcomes; diagnosed failures recur less and zero-progress loops decline in both domains.Direct repairs remain useful, while recurring or conflicting outcomes warrant workflow-mechanism investigation.Source: §8 · pp. 9–10
  • The evaluation covers two formal-verification domains and one outer improvement model; generalization to other models and workflows remains an open question.Behavioral findings concern recorded trajectories and audited mechanisms.Source: §8 · p. 10

A OPERATIONAL CLASSIFICATION OF PROBLEM-SOLVING BEHAVIOR

  • The operational classification uses complete optimization attempts and requires recorded evidence, rather than edit scope or eventual gain, to determine labels.The corpus comprises five independent Lean 4 proof RSI trajectories and 134 optimization attempts; unrecorded reasoning is not reconstructed from outcomes.Source: A OPERATIONAL CLASSIFICATION OF… · p. 12
  • The binary convention counts only F as first-order and H, I, G, and U on the second-order side, but U signals insufficient observability rather than demonstrated reasoning.Accordingly, the resulting second-order share is not the share of validated mechanism investigations.Source: A OPERATIONAL CLASSIFICATION OF… · p. 12, Table 7 · p. 12
  • Operational measures keep reversals, zero-progress loops, retained progress, and group comparisons distinct, with evaluations and lineage rules limiting what the reported counts mean.Reversals are not necessarily harmful; a zero-progress loop requires no retained performance or cost benefit, and group comparisons are descriptive given unequal group sizes and evaluation coverage.Source: A OPERATIONAL CLASSIFICATION OF… · pp. 13–14

A.1 DETAILED RQ2 RESULTS

The detailed RQ2 results report performance-regression rates by inquiry group and qualify how behavioral event counts should be interpreted.

A.1 DETAILED RQ2 RESULTS

  • Performance regression rates are 39.2% for F, 23.5% for H, and 27.3% for I/G.The corresponding counts are 20/51, 4/17, and 3/11.Source: §A.1 · p. 14
  • Group comparisons are descriptive because group sizes and evaluation coverage differ, and later workflows inherit earlier edits.These statistics do not isolate the causal effect of inquiry depth.Source: §A.1 · p. 14
  • Eight of the nine assigned zero-progress loops contain only F edits, describing event composition rather than incidence per editing opportunity.A reversal is not necessarily harmful, and zero-progress loops additionally require no retained performance or cost benefit.Source: §A.1 · p. 14

B.1 ADDITIONAL EXAMPLES OF OPPOSING WORKFLOW EDITS

The Lean trajectory illustrates how similar symptoms can prompt opposing workflow edits without identifying which underlying mechanism is responsible. The protocol records competing explanations, tests them with probes, and evaluates interventions against task outcomes.

B.1 ADDITIONAL EXAMPLES OF OPPOSING WORKFLOW EDITS

  • v13 ties its parent at 18/54, while v19 falls from v18’s 20/54 to 17/54, so both history-expansion and history-removal changes are reverted.Neither trial separates harmful anchoring from useful diagnostics, missing library knowledge, or response variation.Source: §B.1 · p. 15
  • The native_decide fallback accepts rows 4, 5, and 33, but added alternatives and a later omega replacement produce no credited direct solves and are reverted.The examples caution that a useful tool on one target class does not establish that a broader fallback portfolio applies.Source: §B.1 · p. 15

C.1 MECHANISM RECORD

  • Each mechanism record links the observed pattern and task conditions to trace evidence, competing hypotheses, probe results, a proposed intervention, and a recurrence check.Hypotheses remain unresolved, supported under tested conditions, or contradicted; an inconclusive probe differs from an unsuccessful implementation.Source: §C.1 · p. 15

C.2 PROBE AND INTERVENTION PROTOCOL

  • Before probing, the agent records the manipulated factor, held-fixed artifacts, predictions under each live hypothesis, and a budget limit.Transformation replay is preferred when it can answer the question without another model call; when generation is needed, settings and seeds are logged and broader causal claims require additional controls.Source: §C.2 · pp. 15–16
  • Workflow changes require both a mechanism-level prediction and a task-level acceptance criterion, since satisfying the former may not yield a valid proof or better task performance.New components expose their inputs, outputs, state, and tunable choices, but the framework does not prescribe a component type.Source: §C.2 · p. 16

C.3 DETAILED OUTCOME MEASUREMENTS

  • Evaluation reports held-out verification success, improvement over the shared seed, and success across recorded RSI checkpoints, while retaining unknown and multi-cause cases.Errors are grouped by mechanism rather than only by their final message, and independent reviewers audit intervention-supported labels without seeing method identity.Source: §C.3 · p. 16
  • Recurrence is measured over a fixed, independently specified set of eligible opportunities; paired replay isolates process effects, while complete reruns capture later-generation interactions.Main-task pass rates report means and standard deviations across three outer runs, whereas behavioral rates pool underlying counts.Source: §C.3 · p. 16

C.4 TASK DETAILS AND MAIN EVALUATION CONFIGURATION

The evaluation uses held-out Lean proof and Verus code-generation tasks under shared time limits, then measures investigation behavior, intervention outcomes, and mechanism recurrence. Behavioral rates are pooled across runs, with unavailable standard deviations noted for some metrics.

C.4 TASK DETAILS AND MAIN EVALUATION CONFIGURATION

  • Lean evaluation uses 92 training and 48 test problems, while Verus uses 113 training and 46 test problems; both share a 24-hour outer optimization budget.The Lean workflow allows three model calls, 12,000 tokens, four compiler checks, and 180 seconds per task; final held-out evaluation is separate from the budget.Source: §C.4 · p. 16

C.5 SECOND-ORDER BEHAVIOR ANALYSIS

  • Tested inquiry requires a mechanism explanation, testable prediction, and executed discriminating check; decision revision additionally requires a traceable probe-result link that changes a decision.A high revision rate is not inherently desirable because a correct initial explanation may survive testing.Source: §C.5 · p. 17
  • G acceptance is accepted edits divided by evaluated edits, while gain averages each candidate’s development-pass-rate difference from its parent under matched limits.Gain includes rejected candidates and interactions with inherited edits, so it is not a causal allocation of the final trajectory improvement.Source: §C.5 · p. 17
  • Recurrence compares audited parent and child workflows on fixed eligible cases; behavioral rates pool counts across runs, and run-level standard deviations are unavailable for remaining Table 5 metrics.Exposure coverage is reported separately when a changed workflow no longer reaches the relevant stage; probe-dependent metrics are not applicable without executable probes.Source: §C.5 · pp. 17–18, §C.6 · p. 18, Table 12 · p. 18

D IMPLEMENTATION SPECIFICATION

SO-RSI’s controller records workflow attempts, detects recurring structural anomalies, and maintains investigation memory across rounds. It tests mechanism hypotheses with bounded probes, then sends supported evidence to the ordinary editing and evaluation cycle.

D.1 CONTROLLER AND MODEL CALLS

  • A fixed-base-model Python controller coordinates detection, investigation, and editing, advances at most one investigation step between ordinary RSI attempts, and processes the oldest pending update first.Investigation memory starts empty, without a hand-authored library of mechanisms or fixes.Source: §D.1 · p. 18

D.2 ATTEMPT RECORDS AND ANOMALY DETECTION

  • Attempt records link workflow versions, edits, rationales, and outcomes; recurrence, reversal, or mismatch flags require specific trace patterns or an explicit contradicted prediction.Missing predictions or measurements cannot establish mismatch, and detected signals enter memory without an immediate root-cause investigation.Source: §D.2 · pp. 18–19

D.3 INVESTIGATION MEMORY AND RETRIEVAL

  • Investigation memory preserves linked hypotheses, probes, results, and status; new anomalies can reopen records, while matching compiler messages alone do not merge investigations.Historical attempts are retrieved by component and similarity, with successes and failures included when available.Source: §D.3 · p. 19

D.4 HYPOTHESIS FORMATION AND EXTERNAL KNOWLEDGE

  • Each hypothesis specifies a workflow mechanism, supporting and conflicting trace observations, a prediction, and an executable check; parameter changes alone do not complete hypothesis formation.External sources may suggest causes or tests, but cannot establish that a cause occurs in the current workflow.Source: §D.4 · p. 19

D.5 PROBE GENERATION, SELECTION, AND EXECUTION

  • Probe selection favors existing-log inspection, verifier checks, or stage replay, choosing an affordable check whose outcomes could distinguish explanations or change an intervention.This is a qualitative selection rule, not a learned estimate of information gain; probes that exceed the remaining allowance are deferred.Source: §D.5 · pp. 19–20

D.6 INTERVENTION HANDOFF

  • A completed diagnostic check supporting an identifiable workflow intervention permits handoff to G, but does not establish the root cause conclusively.The ordinary development evaluator decides whether to retain the proposed patch, and both accepted and rejected outcomes return to investigation memory.Source: §D.5 · p. 20, §D.6 · p. 20

E AI USE STATEMENT

  • The authors report generative-AI assistance across research and manuscript tasks, while retaining responsibility for final claims and results; the work evaluates generated artifacts with formal verifiers.The reproducibility statement directs readers to the appendices for implementation interfaces, task settings, annotation rules, and behavioral-rate counts.Source: E AI USE STATEMENT · p. 20, F ETHICS STATEMENT · p. 20, G REPRODUCIBILITY STATEMENT · p. 20

H ADDITIONAL RELATED WORK

  • Related work differs from SO-RSI by changing model training, information supply, internal representations, or inference-time behavior rather than investigating reusable workflow mechanisms through attempt-level evidence.The discussion also distinguishes persistent mechanism records from undifferentiated historical examples and contrasts pattern-triggered investigation with routing uncertain outputs for review.Source: H ADDITIONAL RELATED WORK · p. 21
Loading 2610.05701v2…