作者： Daniel Koh, Yannic Noller, Corina S. Pasareanu, Adrians Skapars, Youcheng Sun
提交/修订日期： 2025年6月9日提交，2025年9月16日修订 (v2)
摘要：
大语言模型（LLMs）在代码生成、补全和修复等任务上表现出色，但其处理代码复杂符号推理的能力仍有待探索。本文引入了最坏情况符号约束分析任务，该任务要求推断出表征程序最坏情况执行的符号约束；这些约束可以被求解以获得暴露软件系统性能瓶颈或拒绝服务漏洞的输入。研究表明，即使是最先进的大语言模型（例如GPT-5）直接应用于此任务时也存在困难。为应对这一挑战，本文提出了WARP，一种创新的神经符号方法。该方法首先利用现有程序分析工具计算较小具体输入规模上的最坏情况约束，然后利用大语言模型将这些约束泛化到更大的输入规模。具体而言，WARP包含三个部分：(1) 基于大语言模型的增量式最坏情况推理策略；(2) 一个将强化学习与SMT（可满足性模理论）求解相结合、与求解器对齐的神经符号框架；(3) 一个精心策划的符号约束数据集。实验结果表明，WARP持续改进了最坏情况约束推理的性能。利用该约束数据集，我们使用强化学习微调了一个模型WARP-1.0-3B，其性能显著超越了规模匹配甚至更大的基线模型。这些结果表明，增量式约束推理增强了大语言模型处理符号推理的能力，并突显了在严格的程序分析中神经学习与形式化方法进行更深层次集成的潜力。
主题分类：
- 主要主题： 软件工程 (cs.SE)
- 其他主题： 人工智能 (cs.AI)
arXiv标识符： arXiv:2506.08171 [cs.SE]