Zhechong Huang | Searcharxiv

arXiv2026

SpecRL: Reinforcement Learning with Test-Based Completeness Rewards for Formal Specification Synthesis

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.

cs.SE↗

arXiv2026

Learning to Guarantee Type Correctness in Code Generation through Type-Guided Program Synthesis

Language models have shown remarkable proficiency in code generation; nevertheless, ensuring type correctness remains a challenge. Although traditional methods, such as constrained decoding, alleviate this problem by externally rejecting untypable code, the model itself does not effectively learn type reasoning internally, which ultimately limits its overall performance. This paper introduces TyFlow, a novel system that internalizes type reasoning within code generation to guide the model to learn the type system. The core of our approach is a novel type-guided program synthesis system that maintains an isomorphism between type derivation trees and synthesis derivation trees, enabling a new code representation based on synthesis decision sequences rather than traditional text-based token sequences. By offloading the complexity of type system learning to the representation itself, models can redirect their computational resources toward higher-level program semantics. Our evaluation shows that TyFlow not only eliminates type errors but also significantly improves functional correctness, highlighting the importance of aligning LMs with type systems internally.

cs.PL↗