用验证器奖励蒸馏，让大模型生成更正确的系统级断言。
Reward-Weighted On-Policy Distillation with an Open Property-Equivalence Verifier for NL-to-SVA Generation
- 基于验证器反馈的在线蒸馏，强化属性等价性而非单纯模仿文本。
- 在多个评测集上超越76%准确率的旧模型，新基准达90%以上。
- 适合做硬件验证自动化或大模型可解释性研究的人使用。
基于大语言模型的SystemVerilog断言（SVA）生成虽接近饱和，最强专用模型在NL2SVA-Human上仅达约76%准确率。我们发现，整体表现掩盖了时间维度上的差距：现有模型在有界延迟与活性规范上仍退化为少数蕴含模板。根本原因在于主流监督微调优化的是词级模仿，而非定义SVA正确性的属性等价性。本文提出奖励加权的在线蒸馏（RWOPD），通过开放式的SymbiYosys+Z3属性等价检查器（PEC）评分学生模型生成的序列，仅对通过验证的采样序列应用冻结140亿参数教师模型的验证器奖励加权前KL梯度。该方法在每一步响应中保持密集监督，并将选择与损失权重均锚定于属性等价行为。通过将CodeV-SVA-14B蒸馏至Qwen2.5-Coder-7B-Instruct学生模型，在NL2SVA-Human与NL2SVA-Machine上，pass@1、pass@5、pass@10均刷新基准，超越此前最先进专用模型及6710亿参数通用基线。
原文摘要 · Abstract (English)
LLM-based generation of SystemVerilog Assertions (SVA) is often reported as nearing saturation, with the strongest specialized model reaching ${\sim}76\%$ accuracy on NL2SVA-Human. We show that this aggregate hides a temporal gap: models that appear strong overall still collapse to a few implication templates on bounded-delay and liveness specifications. The core issue is that the dominant recipe, supervised fine-tuning on NL/SVA pairs, optimizes token-level mimicry rather than the \emph{property equivalence} that defines SVA correctness. We introduce \emph{Reward-Weighted On-Policy Distillation} (RWOPD), an on-policy distillation method that samples student rollouts, scores them with an open SymbiYosys+Z3 Property-Equivalence Checker (PEC), and applies a verifier-reward-weighted forward-KL gradient from a frozen 14B teacher on verifier-passable rollouts. This keeps the supervision dense at every response token while grounding both selection and loss weight in property-equivalent behavior. RWOPD distills CodeV-SVA-14B into a Qwen2.5-Coder-7B-Instruct student that sets a new state of the art on NL2SVA-Human and NL2SVA-Machine across pass@1, pass@5, and pass@10, surpassing both specialized prior SOTA models and 671B general-purpose baselines.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。