AuXSpec: Learning to Autoformalize Program Specifications via Executable Postconditions

Formal specifications define intended program behavior and underpin verification, but writing them in theorem provers such as Lean is slow and expertise-intensive, making specification a major bottleneck to scaling formally correct code. Autoformalization from natural-language problems is promising, yet training specification models requires scalable feedback on whether generated specifications capture intended behavior. Prior approaches obtain this feedback through explicit proofs or separately implemented code with formal correspondence proofs, both expensive. We introduce AuXSpec, a Lean framework that pairs declarative postconditions with executable counterparts through typeclass resolution. Test cases can then evaluate declarative specifications by execution, letting us use agreement as a reinforcement-learning reward. Using AuXSpec, we synthesize 3,037 LeetCode problems with proved equivalence theorems and expand training to 19.5K samples through expert iteration on Codeforces. Experiments show that training Qwen3.8-27B and Qwen3.5-9B with the execution-based reward raises SpecGen pass@4 on AuXSpec-Test 0.7% $\to$ 60.3% and 0.7% $\to$ 40.3%. On the out-of-domain Verina benchmark, both models improve 21.9% $\to$ 84.7% and 7.0% $\to$ 69.8%, and the 27B model surpasses VeriSpecGen-30B-A3B, the prior state of the art among open-source specification models, on both pass@1 (47.6% $\to$ 60.2%) and pass@4 (63.9% at pass@10 $\to$ 84.7%). We release the 3,037 problems with test cases and equivalence proofs, the weights of the trained 9B and 27B models, and the 300-problem AuXSpec-Test benchmark with expert review and correctness proofs for future evaluation.