Abstract:Specification synthesis asks a model to generate specifications and auxiliary annotations for an existing program. In modern software verification projects, specification accuracy is critical. A specification is the abstraction of a method's behavior, and callers are verified against the callee's specification rather than its implementation. As a result, the specification for a callee can strongly affect what properties callers can prove. However, verifier feedback alone is a poor training signal for specification synthesis: verification can prove that a specification is sound for the implementation, yet it cannot tell whether the specification is too weak. We present SpecRL, a reinforcement learning framework that adds an empirical completeness signal to specification synthesis in Dafny. SpecRL constructs negative tests, or spectests, from implementation-impossible input-output pairs that weak specifications such as ensures true may still admit. During training, SpecRL rewards verified candidates according to the fraction of spectests their specifications reject, thereby ranking these candidates by how many implementation-impossible behaviors they rule out. On the out-of-distribution DafnyComp-Spec benchmark, the 7B SpecRL model improves verification success and completeness over supervised fine-tuning by 49.96% and 26.46%, respectively. These relative gains show that fine-grained spectest feedback improves both verifiability and specification accuracy.
From: Zhechong Huang [view email]
[v1]
Tue, 7 Apr 2026 12:53:42 UTC (497 KB)
[v2]
Tue, 14 Jul 2026 09:49:12 UTC (1,107 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。