PaperlayerView exact revision on arXiv

Source-linked AI summary

VeruSteer: Learning What to Repair Next in Verus

Chao Jiang, Ding Wang, Chaohua Yang, Dugang Liu, Zhiwu Xu, Cheng Wen, Zhong Ming, Yuwei Liu, Xinyi Wan, Lin Huang

arXiv:2610.29755v1cs.SE

TL;DR

Preset priorities do not account for program context or repair history, even though the same reported error types can call for different choices at different states. VeruSteer learns selections from alternative repair trajectories, recovering verification opportunities while retaining most default successes.

  • Problem

    AutoVerus and VeruSAGE select among reported error types using preset priorities that ignore program context, diagnostic details, and earlier repair attempts.

    Source: §1 · p. 2

  • Method

    VeruSteer learns error-type selection from alternative repair trajectories, using a sequence model trained with step-wise imitation and pairwise outcome ranking.

    Source: §4.3 · p. 8, §5.3 · p. 10

  • Results

    75.0% of available verification improvements are recovered on AutoVerus and 81.8% on VeruSAGE, while 93.3% and 85.7% of default successes are preserved, respectively.

    Source: §1 · p. 3

  • Takeaways & Limitations

    On stored AutoVerus and VeruSAGE test trees, VeruSteer preserves most default successes while recovering successful alternatives, with some losses in retention.

    Source: §9 · p. 24

    Test trees are clustered by task, and selector comparisons include training and sampling randomness that the study does not measure.

    Source: §7.3 · p. 22

Abstract

from arXiv · show

LLM-based verification systems repair Rust proofs by revising programs in response to Verus diagnostics. When several error types are reported, pipelines such as AutoVerus and VeruSAGE select the next repair target using a preset priority. Yet each repair changes the program and the errors that follow, so the same reported types can require different choices at different states. We present VeruSteer, which learns to select error types from the outcomes of alternative repair trajectories. It constructs repair trees offline and compares paths from the same initial program by verification success, repair rounds, and final verification progress. These comparisons supervise a selector that combines step-wise imitation with trajectory preference ranking. The selector uses self-attention over the program, verifier feedback, and earlier selections to rank the currently reported types. It replaces the default priority within a single repair trajectory, keeping the existing repair agents and adding no repair or verifier calls for selection. We evaluate VeruSteer by replaying its choices on stored AutoVerus and VeruSAGE test trees under four generation configurations. Across 1,270 test trees, VeruSteer increases verified outcomes from 185 to 194 (14.57\% to 15.28\%), gaining 12 successes and losing three for a net improvement of 0.71 percentage points. Among trees where the default fails but a recorded alternative verifies, VeruSteer succeeds on 3 of 4 AutoVerus trees and 9 of 11 VeruSAGE trees. Among trees with recorded alternatives where the default verifies, it retains success on 14 of 15 AutoVerus trees and 12 of 14 VeruSAGE trees. It also finds shorter successful trajectories and improves final progress on some trees where all recorded trajectories fail.

1 Introduction

Preset priorities ignore program context and repair history, although the same reported types can call for different choices as repairs unfold. VeruSteer learns contextual selection from alternative repair trajectories and improves recovery while preserving most default successes.

Problem

  • Preset priorities in AutoVerus and VeruSAGE ignore program, diagnostic details, and earlier repair attempts, despite those signals bearing on which target is useful.Repair choices can have delayed effects that become visible only through later repairs.Source: §1 · pp. 2–3

Motivation

  • Among 718 trees with alternative trajectories, 32.0% contain a path that verifies where the default fails, verifies in fewer rounds, or makes greater final progress.A frequent-best-type rule recovers the best choice at only 62.0% of states where one type is uniquely best.Source: §1 · p. 2

Approach

  • VeruSteer builds repair trees offline and derives path preferences from verification, rounds to success, and final progress when paths fail.Comparisons within each tree allow both successful and failed paths to supervise selection.Source: §1 · p. 3
  • A self-attention selector uses the program, verifier feedback, and earlier selections to rank currently reported error types, combining step-wise imitation with pairwise trajectory ranking.At deployment, it follows one trajectory under the original budget without adding repair or verifier calls for selection.Source: §1 · p. 3

Evaluation

  • 75.0% of available verification improvements are recovered on AutoVerus and 81.8% on VeruSAGE, while 93.3% and 85.7% of default successes are preserved, respectively.VeruSteer also finds shorter verified trajectories and improves progress when no recorded trajectory verifies.Source: §1 · p. 3

2 Background

Verus checks annotated Rust programs against formal specifications, while LLM-based repair pipelines use verifier diagnostics to guide revisions. Existing systems differ in how they select a repair target, but AutoVerus and VeruSAGE use fixed error-type priorities.

2.1 Verus

  • Verus is a deductive verifier for Rust that uses specifications and proof annotations to help Z3 discharge verification conditions.It checks typing and language rules before attempting proofs, and failed checks yield diagnostics.Source: §2.1 · pp. 3–4

2.2 Error Selection in LLM-Based Repair

  • LLM-assisted repair systems make separate choices about which failure to target, how to repair it, and which candidate patch to carry forward.AutoVerus and VeruSAGE classify diagnostics, select one error type, and invoke the corresponding specialized repair agent.Source: §2.2 · p. 4
  • AutoVerus and VeruSAGE use a fixed priority list over error types, falling back to Verus diagnostic order when no listed type is present.The list prioritizes type mismatches, then selected proof-failure types; it imposes the same ordering across programs and rounds.Source: §2.2 · pp. 4–5

3 Motivation

A motivating repair tree shows that the best target can change even when the same error types recur. Across a larger corpus, alternative paths often outperform the default, and the best choice varies with state context.

3.1 A Motivating Example

  • In the example, the default overflow-first path remains at score [5] [1] and fails, while the invariant-first path verifies after five rounds.Later states report the same pair of types but require opposite selections, so neither fixed ranking reproduces the successful trajectory.Source: §3.1 · pp. 5–6

3.2 Do the Observations Generalize?

  • The corpus compares trajectories from the same initial program, pipeline, LLM, prompting setting, and repair budget, isolating differences in error-type selections.Recorded paths are ranked first by verification, then by rounds when both verify, and by final progress when neither does.Source: §3.2 · p. 6
  • 32.0% of 718 trees with choices contain an alternative that verifies where the default fails, verifies in fewer rounds, or makes greater final progress.The corpus contains 3,224 trees over 684 tasks, collected with AutoVerus and VeruSAGE.Source: §3.2 · p. 6
  • At 97.0% of 4,943 states with a uniquely best type, another state reporting the same types has a different best choice; the most frequent choice for each type set is right only 62.0% of the time.A fixed ranking cannot represent these state-dependent differences.Source: §3.2 · p. 6

4 Problem Formulation

Section 4 formalizes repair as verifier-guided interaction and defines error selection as choosing among the types reported at each state. It compares resulting trajectories by verification, repair rounds, and final progress, then frames selection as a policy dependent on the current context and repair history.

4.1 Repair as Verifier-in-the-Loop Interaction

  • A repair run repeatedly checks the current program, selects a reported error type, and passes its first matching diagnostic to that type’s repair agent.A run stops on verification, when no type can be extracted, or after the round budget; a step that accepts no candidate still consumes a round.Source: §4.1 · p. 7
  • A state comprises the current program and verifier feedback, which includes diagnostics and summary counts for verified obligations and reported errors.Compilation failure is assigned progress counts of (-1, -1), and verification requires successful completion with zero reported errors.Source: §4.1 · p. 7

4.2 Trajectory Quality

  • Trajectory preference prioritizes verification; among verified runs it prefers fewer rounds, while among unverified runs it prefers greater final progress.Progress prioritizes more verified proof obligations, breaking ties with fewer reported errors.Source: §4.2 · pp. 7–8
  • Runs compared for trajectory quality share the same initial program, pipeline, language model, prompting setting, and budget.Trajectories can tie when neither is better, including when both verify in the same number of rounds.Source: §4.2 · pp. 7–8
  • Repair outcomes are compared using recorded paths because language-model sampling makes exhaustive trajectory exploration impractical.Each expanded node samples one successor per candidate type, producing a finite set of root-to-leaf paths within budget.Source: §4.2 · p. 8

4.3 The Error-Selection Problem

  • A selection policy maps each decision context to one currently reported error type, with the goal of producing trajectories with favorable outcomes on held-out instances.The context includes the current program, verifier feedback, and earlier states and selections.Source: §4.3 · p. 8

5 The VeruSteer Framework

VeruSteer learns error-type selection from alternative repair trajectories collected in trees. It trains a context-aware selector using trajectory preferences and stepwise actions, then replaces the default selection rule while leaving the repair pipeline unchanged.

5 The VeruSteer Framework

  • VeruSteer replaces the default target-selection rule with a learned selector while retaining the existing repair agents and acceptance checks.At deployment it follows a single trajectory and adds no repair or verifier calls for selection.Source: §5 · p. 9, §5.4 · p. 12

5.1 Repair-Tree Construction

  • Repair trees branch once for each reported candidate type, recording accepted successor states until verification, no candidate type, or the five-round budget.Each root-to-leaf path is a trajectory from the same initial program and setup, allowing direct comparison with the default path.Source: §5.1 · p. 9

5.2 Preference Supervision

  • Within each tree, trajectory pairs prefer paths that verify over those that do not, faster verified paths, or—if none verify—paths with more progress.Pairs are formed independently of whether a path follows the default rule; trees with no better path yield no pair, and each tree contributes at most 1,000 pairs.Source: §5.2 · pp. 9–10

5.3 Error Type Repair Selector

  • The selector encodes the current program and verifier feedback alongside earlier selected types, then uses self-attention to represent the repair history and score reported candidates.Its vocabulary combines 35 error types from the AutoVerus and VeruSAGE data-collection implementations.Source: §5.3 · p. 10

5.4 Dual-Loss Optimization and Deployment

  • Training combines cross-entropy on selected actions along preferred trajectories with a ranking loss comparing preferred and dispreferred trajectory outcomes.The overall objective combines the two losses; deployment keeps the agents, acceptance checks, verifier, and original budget unchanged.Source: §5.4 · pp. 11–12

6 Evaluation

VeruSteer is evaluated by replaying selector choices on stored AutoVerus and VeruSAGE repair trees, measuring verification, shorter successful paths, and progress. Across the evaluation, it improves overall verification, while ablations and round-by-round analyses examine which selector components contribute and how outcomes change.

6.1 Experimental Setup

  • The test uses task-separated training, validation, and test splits, and replays selector choices on stored trees without new LLM or verifier calls.The corpus contains 3,224 trees from 684 tasks; 718 trees include alternative trajectories, and the replay budget is five rounds.Source: §6.1 · pp. 13–14

6.2 RQ1: Overall Performance

  • 185 to 194 verified trees out of 1,270: VeruSteer gains 12 successes, loses three, and nets nine trees (0.71 percentage points) over the default rule.The overall comparison pools both repair pipelines across the test trees.Source: §6.2 · p. 15, Table 3 · p. 15
  • VeruSteer recovers 75.0% of available verification improvements on AutoVerus and 81.8% on VeruSAGE, while retaining 93.3% and 85.7% of default successes, respectively.For shorter verified paths, Exploration is 25.0% (2/8) on AutoVerus and 100.0% (3/3) on VeruSAGE; Higher score Exploration is 23.7% and 38.5%, respectively.Source: §6.2 · p. 15, Table 4 · p. 16

6.3 RQ2: Ablation Study

  • VeruSteer outperforms eight alternatives: it recovers 9/11 verification opportunities (81.8%), versus at most 6 (54.5%), and has a 67.5-point net gain.Ablations show that both losses and each input representation contribute; step-wise imitation supports Exploration, while pairwise ranking supports Retention.Source: Figure 5 · p. 16, §6.3 · pp. 17–18, Figure 6 · p. 18

6.4 RQ3: Repair Progress across Rounds

  • VeruSteer leads the default in verified proof obligations from Round 1, widening the gap to 0.082 on AutoVerus and 0.085 on VeruSAGE by Round 5.It ends with fewer reported errors on both pipelines: 1.31 against 1.35 on AutoVerus and 1.04 against 1.10 on VeruSAGE.Source: §6.4 · pp. 19–20, Figure 8 · p. 19

6.5 RQ4: Choices among Reported Error Types

  • For the displayed candidate sets, VeruSteer departs from the default’s near-deterministic choices, with associated final verification-rate differences ranging from 0.72 to 26.04 percentage points.For MismatchedType+Other, VeruSteer selects Other in 87.74% of decisions; the associated difference is 2.43 percentage points.Source: §6.5 · pp. 20–21, Figure 9 · p. 20

7 Discussion and Threats to Validity

The discussion frames repair-target selection as a learnable part of verification automation that can improve outcomes while leaving repair agents unchanged. It also identifies limits from the selector’s scope, finite repair-tree exploration, and the replay-based evaluation.

7.1 Implications for Verification Automation

  • With the same agents, acceptance checks, verifier, and budget, VeruSteer recovers 75.0% and 81.8% of available verification opportunities on AutoVerus and VeruSAGE, respectively.The authors argue that error-type selection is a separate policy decision whose best choice can vary across states reporting the same types.Source: §7.1 · p. 21
  • Trajectory comparisons provide unlabelled supervision from verifier outcomes, and replay compares selectors on the same stored transitions without new LLM or verifier calls.The learned static priority recovers 6 of 11 verification opportunities (54.5%) but retains only 9 of 14 default successes (64.3%), motivating separate Retention and Exploration reporting.Source: §7.1 · p. 21

7.2 Limitations and Future Directions

  • VeruSteer learns only which failure to target, and acts only when a state reports several error types.Repair method and candidate-patch selection remain with the repair agent; the trees retain only the accepted patch, so they do not compare alternative methods or patches.Source: §7.2 · pp. 21–22
  • Each tree samples one repair per reported type and keeps its accepted successor, so preferences reflect the best observed trajectories rather than proven optima.Repeated samples could improve preference reliability, but tree construction costs much more than following one trajectory; trees must also be rebuilt when the LLM, agents, or Verus version change.Source: §7.2 · p. 22
  • The five-round repair budget bounds the preferences to trajectories within five rounds and may miss choices whose payoff comes later.The history window length controls how many recent states are read, not the repair horizon; a longer window does not teach the selector about longer repairs.Source: §7.2 · p. 22

7.3 Threats to Validity

  • The evaluation uses 684 of 762 StarVerus tasks with repair trees, two pipelines, specified generation models, and stored transitions rather than fresh end-to-end repair runs.The test trees are clustered within tasks, and differences of a few trees are treated as trend indications because training and sampling randomness were not measured.Source: §7.3 · p. 22
  • Verification success means passing the supplied specification, while progress and repair rounds are surrogates that do not measure functional coverage, assurance strength, elapsed time, or human effort.The authors audited verified test leaves for zero errors and proof-bypassing constructs; specification adequacy remains outside what verifier success establishes.Source: §7.3 · p. 22

8 Related Work

Prior Verus repair systems improve repair context, generation, or candidate selection, while VeruSteer focuses on choosing which concurrently reported error type to address. Its related work connects that decision to contextual selection, verification search, and sequential recommendation.

8.1 LLM-Assisted Specification and Proof Repair

  • AutoVerus [36] and VeruSAGE [37] use specialized repair agents, but their target error type still follows a preset priority; StarVerus instead uses a prompted planner to propose an order.VeruSteer trains a dedicated selector from preferences between alternative trajectories from the same initial program.Source: §8.1 · p. 23
  • Other Verus systems improve repository context, counterexample guidance, candidate ranking, or proof generation, whereas VeruSteer chooses among concurrently reported error types.Examples include RAGVerus [42], ExVerus [38], SAFE [7], AlphaVerus [1], and VeriStruct [29].Source: §8.1 · p. 23
  • Preguss [32] orders C verification units before synthesis, whereas VeruSteer responds to changing diagnostics inside a repair loop.Laurel [25] uses error locations and similar proofs to generate Dafny helper assertions; related work also synthesizes specifications [23] [33], invariants [8] [19] [21], and formalizations [9].Source: §8.1 · p. 23

8.2 Selection and Search in Verification

  • Learned rankers such as iRank [5] and Quarry [41] rank invariant candidates or proof-goal decompositions, while VeruSteer ranks error types from state and repair history.Online search methods explore alternative continuations; VeruSteer explores alternatives offline for supervision and then follows one trajectory without extra repair or verifier calls for selection.Source: §8.2 · pp. 23–24

8.3 Sequential Recommendation and Preference Learning

  • VeruSteer adapts sequential recommendation and preference learning by treating repair histories as interaction sequences, reported error types as available items, and verifier outcomes as supervision.It draws on SASRec [14] for sequential encoding and BPR for pairwise ranking, alongside step-wise imitation of preferred trajectories.Source: §8.3 · p. 24

9 Conclusion

VeruSteer learns which verifier-error type to repair next from alternative repair trajectories, using program state, verifier feedback, and earlier selections. On stored AutoVerus and VeruSAGE test trees, it preserves most default successes, recovers successful alternatives, and improves some unsuccessful trajectories.

9 Conclusion

  • VeruSteer learns the next verifier-error type to repair from preferences among alternative trajectories originating at the same program.A sequence model uses the program, verifier feedback, and earlier selections while existing specialized agents and verification checks remain in the repair loop.Source: §9 · p. 24
  • On stored AutoVerus and VeruSAGE test trees, VeruSteer preserves most default verification successes and recovers successful alternatives, with some losses in retention.It also finds shorter successful paths and improves progress on unsuccessful ones.Source: §9 · p. 24
  • The results support treating repair order as a separate part of verification automation, allowing existing repair agents to benefit from outcomes of alternative executions.The strategy comparisons and ablations show the value of context and trajectory supervision for these choices.Source: §9 · p. 24

Related papers

Loading 2610.29755v1…