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

arXiv: https://arxiv.org/abs/2610.05701 · HTML: https://mlsanity.com/paper/2610.05701/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 22 of its 25 references that are in the map.
- First posted on arXiv 5 Oct 2026.

## Builds on (most cited first, 22 of 22)

- [A Self-Improving Coding Agent](https://mlsanity.com/paper/2504.15228/) (2025)
- [AutoManual: Constructing Instruction Manuals by LLM Agents via Interactive Environmental Learning](https://mlsanity.com/paper/2405.16247/) (2024)
- [From Failed Trajectories to Reliable LLM Agents: Diagnosing and Repairing Harness Flaws](https://mlsanity.com/paper/2606.06324/) (2026)
- [In-context Time Series Predictor](https://mlsanity.com/paper/2405.14982/) (2024)
- [Reasoning-Enhanced Domain-Adaptive Pretraining of Multimodal Large Language Models for Short Video Content Governance](https://mlsanity.com/paper/2509.21486/) (2025)
- [Audio-Enhanced Vision-Language Modeling with Latent Space Broadening for High Quality Data Expansion](https://mlsanity.com/paper/2503.17551/) (2025)
- [ZeroTuning: Unlocking the Initial Token's Power to Enhance Large Language Models Without Training](https://mlsanity.com/paper/2505.11739/) (2025)
- [Read Before You Think: Mitigating LLM Comprehension Failures with Step-by-Step Reading](https://mlsanity.com/paper/2504.09402/) (2025)
- [LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving](https://mlsanity.com/paper/2605.13137/) (2026)
- [WorldCoder-Bench: Benchmarking Physically Grounded 3D World Synthesis](https://mlsanity.com/paper/2606.01869/) (2026)
- [VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean](https://mlsanity.com/paper/2602.18307/) (2026)
- [IPS: In-Prompt Process Supervision for Short Video Content Moderation](https://mlsanity.com/paper/2412.15251/) (2024)
- [Can LLMs Handle WebShell Detection? Overcoming Detection Challenges with Behavioral Function-Aware Framework](https://mlsanity.com/paper/2504.13811/) (2025)
- [RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation](https://mlsanity.com/paper/2502.05344/) (2025)
- [ICA Lens: Interpreting Language Models Without Training Another Dictionary](https://mlsanity.com/paper/2606.11722/) (2026)
- [Chain-Aware Encoding for Microservice Trace Anomaly Detection](https://mlsanity.com/paper/2607.10156/) (2026)
- [ExVerus: Verus Proof Repair via Counterexample Reasoning](https://mlsanity.com/paper/2603.25810/) (2026)
- [VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation](https://mlsanity.com/paper/2605.08553/) (2026)
- [GRACE: Grounded Reasoning via Adapter Composition and Evidence-Aware Calibration for Educational Visual Question Answering](https://mlsanity.com/paper/2608.19355/) (2026)
- [GeoCueFormer: Geometry-Guided Wavelet Representation and Prediction-Cued Dual-Stage Decoder for Underwater Semantic Segmentation](https://mlsanity.com/paper/2609.18069/) (2026)
- [ReVA: A Scene-Centric Dataset Beyond Repetition for Remote Sensing Video Question Answering](https://mlsanity.com/paper/2609.35507/) (2026)
- [RAGScope: A Leakage-Controlled, Cost-Aware Evidence-Gating Protocol for RAG Hallucination Triage](https://mlsanity.com/paper/2609.39075/) (2026)

## Abstract (arXiv)

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.