Newest papers

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 · 2026 · arXiv (Cornell University)

DOI: 10.48550/arxiv.2610.29755 · cited by 0 works (OpenAlex) · open-access PDF

Chinese

自动验证记录检验系统通过对 Verus 诊断进行修复程序来修复Rust 证据。当多种错误类型被报告时,像 AutoVerus 和 VeruSAGE 这样的管道使用预设优先级选择下一个修复目标,但每个修复都会改变程序和随后的错误,所以相同的报告类型可能需要在不同状态下进行不同的选择。我们介绍 VeruSteer,该管道可以从替代修复轨道的结果中选择错误类型。它构建了离线修复树木,并通过验证成功、修复周期和最终验证进展来比较相同的程序的路径。这些比较监控了一个选择器,将默认模仿与成功验证的轨道优先级排名相结合。该选择器使用自我注意力,验证器

Machine translation (Meta M2M100); the English original follows.

Abstract

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.

Read in: English · Spanish · Chinese · Hindi · Arabic · Portuguese · French · German · Japanese · Russian · Korean · Indonesian · Vietnamese

Topics: Computer science, Test (biology), Rank (graph theory), Mathematical proof, Machine learning, Imitation

Sources: OpenAlex (CC0), arXiv, Crossref. Agent Exchange