用形式化验证增强大模型的代码推理能力，提升等价性判断准确率。
Improving LLM Code Reasoning via Semantic Equivalence Self-Play with Formal Verification
- 通过生成器与评估器对抗训练，结合液态霍斯金证明验证等价性。
- 在EquiBench上最高提升13.3个百分点，对齐任务表现显著改善。
- 适用于需高可靠性代码验证的研究者，尤其关注形式化方法的团队。
我们提出一种用于霍斯金语言的语义等价性自对弈框架，利用形式化验证引导生成器与评估器之间的对抗训练。该框架采用液态霍斯金（Liquid Haskell）证明验证等价性，以执行结果反例判定非等价性，并基于难度感知课程组织训练过程。为支持此研究，我们发布了约28,000个经验证的霍斯金程序合成数据集——OpInstruct-HSx。实验证明，所训练的评估器可有效迁移至下游任务，在EquiBench上实现最高13.3个百分点的准确率提升，并在PySecDB上持续取得增益。消融实验表明，尽管非等价监督提供数据量，但等价性证明才是模型推理能力的关键来源。整个训练流程与数据集已分别公开于GitHub和Hugging Face。
原文摘要 · Abstract (English)
We introduce a self-play framework for semantic equivalence in Haskell, utilizing formal verification to guide adversarial training between a generator and an evaluator. The framework leverages Liquid Haskell proofs for validating equivalence and execution-based counterexamples for inequivalence, organized via a difficulty-aware curriculum. To facilitate this, we release \textbf{OpInstruct-HSx}, a synthetic dataset of $\approx$28k validated Haskell programs. Empirical experiments show that our evaluator transfers effectively to downstream tasks, achieving up to 13.3pp accuracy gain on EquiBench and consistent gains on PySecDB. Ablation studies on the SEQ-SINQ regimes indicate that while inequivalence supervision provides data volume, equivalence proofs are uniquely responsible for the model's reasoning capabilities. The entire training pipeline and dataset are publicly released on GitHub and Hugging Face respectively.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。