通过形式验证的语义等价自博弈提升大语言模型代码推理
Improving LLM Code Reasoning via Semantic Equivalence Self-Play with Formal Verification
AI总结：
本文提出一种基于形式验证的语义等价自博弈框架，利用对抗训练提升代码推理能力，通过验证等价性与非等价性，释放OpInstruct-HSx数据集，实验显示在EquiBench上提升13.3个百分点。
摘要：
我们介绍了一种用于Haskell语义等价性的自博弈框架，利用形式验证来指导生成器和评估器之间的对抗训练。该框架利用Liquid Haskell证明来验证等价性，并利用基于执行的反例来验证非等价性，通过难度感知的课程进行组织。为了促进这一目标，我们发布了OpInstruct-HSx，一个包含约28,000个验证过的Haskell程序的合成数据集。实验证明，我们的评估器能够有效转移到下游任务，在EquiBench上实现高达13.3个百分点的准确率提升，并在PySecDB上实现一致的提升。对SEQ-SINQ模式的消融研究显示，虽然非等价监督提供数据量，但等价证明是模型推理能力的关键。整个训练流程和数据集已分别在GitHub和Hugging Face上公开。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
