SO-RSI 让 formal-verification agents 先诊断失败机制，再递归改进 Lean / Verus 工作流

Jiang、Vempaty 与 Jagmohan 提出 SO-RSI，把 agent workflow 的 recursive self-improvement 从“看到失败就局部改参数”的一阶修补，升级为先识别 recurrence、opposing edits 与 expectation mismatch 三类结构异常，再通过 lightweight diagnostic probes 和跨轮次 persistent inquiry memory 积累因果证据后修改工作流。论文在匹配的 24 小时搜索预算下报告：相较 Naive RSI，Lean 4 proof generation 的最终 held-out pass rate 提高 21.8 个百分点，Verus verifiable-code generation 提高 25.8 个百分点；消融实验也显示 executable probes 与 persistent investigation memory 都是主要增益来源。