通过带有形式化验证的语义等价自我博弈提升大语言模型代码推理能力

本文提出了一种基于 Haskell 语义等价的自我博弈框架，利用形式化验证指导生成器与评估器之间的对抗训练。该框架借助 Liquid Haskell 证明验证等价性，并通过执行反例处理不等价情况，结合难度感知课程进行组织。为此，作者发布了包含约 2.8 万个已验证 Haskell 程序的综合数据集 OpInstruct-HSx。实验表明，该评估器在下游任务中表现优异，在 EquiBench 上准确率提升达 13.3%，并在 PySecDB 上取得一致增益。消融研究证实，等价性证明是提升模型推理能力的关键因素。