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

Yuxuan Jiang; Aditya Vempaty; Ashish Jagmohan

cs.AIOct 5, 2026

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

Authors: Yuxuan Jiang, Aditya Vempaty, Ashish Jagmohan

Organizations: University of Maryland, Baltimore County · Emergence AI

Abstract

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.

Figures & tables

Figure 1: One symptom, opposite fixes. Repeated unsolved goals feedback leads a first-order response to alternate between hypotheses of insufficient recall ( $k=20$ ) and exceeded context limit ( $k=15,18$ ). Top: The agent oscillates through parameter patching without resolving the failure. Bottom: The underlying issue is poor retrieval ranking—a large window introduces excessive noise, while smaller windows exclude the low-ranked key lemma. Relevance-based reranking and filtering eliminate this trade-off, producing a dense context. Blue/dark-blue tiles denote relevant/key lemmas, and gray tiles denote noise.

Inquiry category	Attempts	Share
First-Order: Direct repair (F)	86	64.2%
Second-Order Behavior (Permissive Grouping)	48	35.8%
Mechanism hypothesis, untested ( H )	29	21.6%
Mechanism investigation ( I )	8	6.0%
Evidence-guided intervention ( G )	7	5.2%
Insufficient information ( U )	4	3.0%

Table 1: Problem-solving behavior in outer RSI (RQ1). Under our permissive convention, only direct repairs ( F ) count as first-order. The second-order group contains hypotheses ( H ), diagnostic investigations ( I ), evidence-guided interventions ( G ), and insufficient records ( U ). I+G denotes an observable diagnostic check, not necessarily a confirmed mechanism or successful intervention. Shares use all 134 attempts across five trajectories.

Inquiry group	Evaluated edits	Mean gain $\uparrow$ (pp)	Performance regressions $\downarrow$
Direct repair (F)	51	+8.7	20/51 (39.2%)
Untested hypothesis (H)	17	+11.2	4/17 ( 23.5% )
Diagnostic inquiry (I/G)	11	+14.3	3/11 (27.3%)

Table 2: Gains and regressions of evaluated RSI edits (RQ2). Gain is the pass-rate change relative to the edit’s actual parent, in percentage points (pp); regressions are edits with a negative change. Results cover 79 evaluated edits from 130 F/H/I/G attempts; arrows indicate the preferred direction.

Figure 2: From first-order thrashing to second-order improvement. Anomalies in the RSI history trigger mechanism investigation (I); diagnostic evidence guides a workflow change (G), evaluated by ordinary RSI. Within I, the agent forms and tests hypotheses, consults external knowledge when needed, and retains findings across RSI rounds.

	Lean proving		Verus VCG
Method	Pass $\uparrow$	$\Delta\uparrow$	Pass $\uparrow$	$\Delta\uparrow$
Initial workflow $S_{0}$	29.4	0.0	14.8	0.0
Naive RSI	$49.4\pm 2.8$	+20.0	$33.4\pm 5.2$	+18.6
SO-RSI	$71.2\pm 1.9$	+41.8	$59.2\pm 3.7$	+44.4

Table 3: Held-out verification performance. RSI methods share a 24-hour outer budget and identical per-task limits. Pass is task pass rate (%);

\Delta

is the change from the corresponding seed (pp). Pass reports mean

\pm

standard deviation over three independent runs;

\Delta

is the mean gain over the fixed starting-point reference

S_{0}

Figure 3: Verification performance across RSI checkpoints. Naive RSI and SO-RSI on Lean proving and Verus VCG. A denotes the initial workflow and B the final result; 1–11 are intermediate checkpoints shown in sequence, not elapsed-time intervals. Curves show the reported pass rates without checkpoint-level uncertainty estimates.

Variant	Lean pass $\uparrow$	VCG pass $\uparrow$
SO-RSI	$71.2\pm 1.9$	$59.2\pm 3.7$
w/o executable probes	$63.4\pm 5.6$	$33.0\pm 3.8$
w/o persistent investigation memory	$60.9\pm 4.2$	$36.7\pm 6.2$

Table 4: Contribution of executable probes and persistent investigation memory. Held-out pass rates (%) are reported as mean

\pm

standard deviation over three runs. All variants share the initial workflow and 24-hour outer budget.

Lean proving
	Investigation		G edits		Persistence
Method	Tested (%)	Revised (%)	Accept (%)	$\Delta$ Pass $\uparrow$	$\Delta$ Rec. $\downarrow$	Loops $\downarrow$
Naive RSI	14.8	0.9	54.8	4.4	-7.3	18.7
SO-RSI	46.0	22.6	67.1	9.8	-31.4	7.2
w/o probes	—	—	56.5	6.1	-12.8	13.9
w/o memory	41.6	15.3	59.7	7.0	-19.6	11.8

Table 5: How investigation translates into workflow improvement. The first three columns are percentages calculated from their respective reported numerator/denominator counts (Appendix C.6 ); Tested and Revised share the denominator of all investigation episodes; Revised counts changes driven by executed diagnostic evidence. G acceptance is a percentage of evaluated G edits.

\Delta

Pass is the mean parent-to-edit development gain (pp), including rejected edits.

\Delta

Rec. is post-edit minus pre-edit mechanism recurrence (pp; negative indicates reduction). Loops are zero-progress loops per 100 evaluated edits. Dashes in the w/o probes row mark probe-dependent metrics as not applicable. The table reports point estimates; run-level standard deviations are not available for these behavioral metrics.

Appendix figures & tables7 assets

Supplementary material from the paper’s appendix.

Appendix

Criterion	Evidence required	Insufficient evidence
M: Mechanism explanation	Identifies how a workflow process produces the failure, beyond restating the symptom.	“Too few lemmas; increase $k$ ” merely redescribes a shortage.
D: Diagnostic check	Actually checks whether the proposed mechanism occurs or distinguishes competing causes; the target is not only aggregate task performance.	Comparing solve rates at $k=10$ and $k=20$ alone tests settings, not the cause of failure.
L: Evidence-guided intervention	The intervention is explicitly justified by diagnostic findings; contradictory or inconclusive evidence can change or halt the proposal.	Increasing $k$ regardless of the diagnostic result.

Appendix

Table 6: Observable criteria for mechanism-directed investigation. These criteria describe a progression, not an additive score.

Label	Decision rule	Binary group
F: Direct repair	Observable behavior is limited to immediate repair or settings search, without an upstream mechanism explanation.	First-order
H: Mechanism hypothesis	M is present, but no diagnostic check D is carried out.	Second-order
I: Mechanism investigation	M is present and D is carried out; findings may be inconclusive or refute the hypothesis.	Second-order
G: Evidence-guided intervention	M and D are present, and the resulting intervention satisfies L. Task-level success is not required for this label.	Second-order
U: Insufficient information	The available record does not support a judgment of the attempt’s inquiry process.	Second-order, by convention

Appendix

Table 7: Fine-grained labels and the permissive binary convention. Lack of diagnostic evidence yields H when a mechanism hypothesis is recorded; inadequate records to judge the attempt yield U.

Observed optimization behavior	Label	Rationale
Claims that more lemmas are needed; raises $k$ from 10 to 20 and observes a higher solve rate.	F	Establishes a setting’s performance, not why the failure occurred.
Later claims that there are too many lemmas; lowers $k$ from 20 to 15 and observes a higher solve rate.	F	Opposite settings search; evaluation across instances does not itself establish mechanism inquiry.
Hypothesizes that lexical ranking pushes a key lemma below top- $k$ , then replaces the retriever without checking that explanation.	H	Provides a process-level hypothesis but no diagnostic check.
Checks the needed lemma’s rank in failed cases and whether it actually entered the generation prompt.	I	Tests whether key evidence was omitted by the retrieval process.
Holds the count fixed while replacing an irrelevant lemma with a needed one; or preserves needed lemmas while removing irrelevant ones.	I	Probes evidence quality or distraction rather than only searching over counts.
Uses diagnostic findings to select ranking, filtering, or count changes, then evaluates the intervention.	G	The intervention follows from mechanism evidence rather than a predetermined solution.

Appendix

Table 8: Illustrative annotations for lemma retrieval. These are coding examples, not measured experimental trajectories.

Label	Attempts	Share
F: Direct repair	86	64.2%
H: Mechanism hypothesis	29	21.6%
I: Mechanism investigation	8	6.0%
G: Evidence-guided intervention	7	5.2%
U: Insufficient information	4	3.0%
Total	134	100%

Appendix

Table 9: Fine-grained breakdown underlying RQ1. All shares use the same denominator of 134 outer optimization attempts across five trajectories as Table 1 . The subtotal I+G identifies attempts with an observable diagnostic check, including inconclusive or refuted hypotheses. U is retained explicitly despite its inclusion on the second-order side. Percentages are rounded to one decimal place.

Trajectory	Initial	Final	$\Delta$	Cost
1	29.4	46.2	+16.8	25
2	29.4	50.4	+21.0	28
3	29.4	48.0	+18.6	26
4	29.4	44.9	+15.5	23
5	29.4	51.6	+22.2	32
Mean / total	29.4	48.2	+18.8	134

Appendix

Table 10: Detailed trajectory and edit outcomes for RQ2. Top: pass rates (%), final-minus-initial gain (percentage points), and total cost (million tokens). Bottom: three mutually exclusive inquiry groups;

\Delta

is the pass-rate change in percentage points relative to an attempt’s actual parent. U remains in trajectory totals but is excluded from group comparisons. Reversals use the closing edit’s group; loops spanning groups are not assigned to a single group. The summary row averages pass rates and gains and sums costs.

Setting	Lean proving	Verus VCG
Benchmark / subset	RSI-Exam + VeriSoftBench	VeriContest, hard
Training / test problems	92 / 48	113 / 46
Outer improvement model	GPT-5.6-sol	GPT-5.6-sol
Inner model snapshot	gpt-5.4-2026-03-05	gpt-5.4-2026-03-05
Inner temperature / seed	0 / 0	0 / 0
Outer budget per run	24 hours	24 hours

Appendix

Table 11: Main experiment configuration. The seed is the common RSI starting point. Both domains retain the RSI-Exam inner model and per-task limits.

Lean proving
Method	Tested	Revised	Accepted G
Naive RSI	273/1840	16/1840	34/62
SO-RSI	1482/3223	729/3223	51/76
w/o probes	—	—	39/69
w/o memory	1194/2870	438/2870	43/72
Verus VCG

Appendix

Table 12: Underlying counts for behavioral rates. Entries show numerator/denominator for each reported metric. Dashes indicate probe-dependent metrics that are not applicable without probes; the corresponding investigation totals are 2,017 (Lean) and 1,668 (VCG).

Explore similar work

MetaRSI / RSI2: A Meta-Recursive Self-Improving System for Recursive Self-Improving Systems Themselves
Sep 6, 2026Zihan Tan, Leixin Sun, Zitong Shi +28Recursive Self-Improvement Recursive Models
Hugging Face
Which Self-Improvements Should We Trust? Reliable Self-Improvement When Agents Reuse Their Benchmarks
Sep 27, 2026Xiaojing Sun, Yuhan Zeng, Zihua She +1Recursive Self-Improvement AI Trustworthiness
Purdue University
FC-SWE: Failure-Conditioned RL for Long-Horizon Software Engineering Agents
Oct 6, 2026Jia Liufu, Bin Hu, Linglin Jing +5Swe-Bench Verified Retrying
NVIDIA · Tsinghua University

Sep 6, 2026, cs.LGJ/K move · Enter open · S save

MetaRSI / RSI2: A Meta-Recursive Self-Improving System for Recursive Self-Improving Systems Themselves

Zihan Tan, Leixin Sun, Zitong Shi, Yitao Liu+27

Hugging Face

Recursive Self-Improvement Recursive Models Meta-Learning Mle-Bench Lite Scientific Discovery Dream

Open paper AskPDF arXiv

Recursive self-improvement (RSI) lets a system improve the model-building machinery from its own failures, so every later model inherits the gain. Yet RSI has been validated almost exclusively on coding and formal benchmarks such as science QA and mathematics. This format bound limits RSI to improvement within a machine-checkable slice, not general capability where questions are open and correctness is settled by argument, replication, or measurement. We argue RSI must next operate across real, diverse scientific, engineering, and meta-scientific domains, not where formal evaluation is merely tractable. To that end we present MetaRSI-v1, where improvement is the scheduled composition of three typed operators over one unified paradigm. Data-RSI amplifies existing competence and marks its boundary; Harness-RSI edits a five-slot scaffold without touching weights; Model-RSI internalizes capability into parameters through bounded training. Sharing one loop kernel and artifact vocabulary, they make data, scaffold, and model changes composable rather than exclusive. A two-axis optimizer jointly decides operator order and each operator's proposal policy, while a meta-level policy revises the schedule across terms. We validate MetaRSI-v1 under the field's standard evaluations, on code and closed-form science, with no external teacher: the target model plays every role in its own loop. MetaRSI-v1 reframes self-improvement from a single-surface edit to a composition across the full model-production pipeline, opening two paths: a model route internalizing capability through training, and a harness route leaving weights untouched and thus extending self-improvement to any model reachable through an interface, with Data-RSI redefined as the shared substrate feeding both. The framework further yields refutable laws on where loops exist, how operators compose, and what supervision buys.

Abstract

Explore similar work

MetaRSI / RSI2: A Meta-Recursive Self-Improving System for Recursive Self-Improving Systems Themselves

Which Self-Improvements Should We Trust? Reliable Self-Improvement When Agents Reuse Their Benchmarks

FC-SWE: Failure-Conditioned RL for Long-Horizon Software Engineering Agents