arXiv cs.AI· Rongkang Li, Jiaxin Hu, Taolue Chen, Yong Li, Fu Song, Zhilin Wu·· 14 小时前AI 评分29
RAINFALL：用 LLM 生成排序函数证明循环终止
Ranking Function Generation with LLMs for Termination
AI 导读
神经符号框架 RAINFALL 将排序函数合成转化为代码补全任务，由 LLM 填充循环的四个预定义槽位，再经符号验证器检查，失败时将诊断转为自然语言反馈迭代精修。
正文 · AI 翻译
摘要：秩函数是证明循环终止的一项基础技术，但手动构造秩函数颇具挑战性，且需要大量专业知识。我们提出 RAINFALL，一个遵循生成-验证-精炼范式的神经符号框架，将 LLM 与符号验证紧密结合。RAINFALL 将秩函数合成表述为代码补全任务：在输入程序中插入占位符，并约束 LLM 为每个循环填充四个预定义槽位。补全后的程序随后由符号验证器检查。若验证成功，则获得有效的秩函数；否则，验证器的诊断信息被转换为自然语言反馈，以指导 LLM 输出的迭代精炼。我们在两个公共基准套件上评估 RAINFALL，共包含 358 个可终止的 C 程序。使用 MiniMax V2.7，RAINFALL 为 323 个程序（90.22%）合成了可验证的秩函数，优于所有有前景的基线。特别地，它比 PROTON 2.1 多解决了 12 个程序，后者是表现最佳的基线，也是 SV-COMP 2026 终止类别的获胜者。此外，将 RAINFALL 与 PROTON 2.1 结合可将成功率提升至 96.65%（346/358 个程序）。我们还进行了消融研究，确认了占位符契约、少样本示例、符号验证和诊断信息反馈各自的贡献。跨 LLM 的实验进一步证实了 RAINFALL 的有效性。我们的结果表明了一个通用的、可靠的秩函数合成框架，并且在终止性之外，还适用于 LLM 辅助合成可形式化检查的活性证书，这两者都代表了软件工程研究的新方向。
| 注释： | 24 页，6 页 |
| 主题： | 软件工程（cs.SE）；人工智能（cs.AI）；计算机科学中的逻辑（cs.LO） |
| 引用为： | arXiv:2610.35523 [cs.SE] |
| （或 arXiv:2610.35523v1 [cs.SE] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.35523 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Fu Song [查看电子邮件]
[v1]
2026 年 10 月 26 日星期一 14:41:52 UTC（1,255 KB）
来源：arXiv cs.AI · arxiv.org