LLM生成ACSL契约验证PETSc，竟发现藏了27年的老bug！
Verification of PETSc with CIVL using LLM-generated ACSL contracts and deterministic driver generation
📖 AI 总结
这篇论文针对并行数值库PETSc长期缺乏形式化验证的问题，提出了一种将大语言模型（LLM）与确定性验证工具链相结合的验证方法。其核心思路是：不让LLM自由生成代码，而是仅在受限场景下根据函数文档生成规模小、可人工认证的ACSL契约，再由确定性工具链生成驱动程序，调用CIVL验证器检查实现是否符合契约，并在存在参考模型时进行比对。作者在MatAXPY、MatAYPX和MatFilter（非压缩模式）三个PETSc函数上完成了端到端验证，其中MatAYPX无参考模型，认证契约成为唯一判定依据。该流程成功发现MatAYPX中一个自1997年起便存在、此前未被察觉的缺陷，表明LLM辅助的受限契约生成结合确定性验证，能够在真实科学计算库中发现深层错误，为数值库的形式化验证提供了可行路径。
🔑 关键词速览
| PETSc | 一个用于科学计算的并行数值库，提供线性代数、非线性求解器等高性能组件。 |
| ACSL | ANSI/ISO C Specification Language，一种用于C语言程序形式化规约的规范语言，支持契约式设计。 |
| CIVL | 一个用于并发程序验证的验证器，支持C语言程序的断言检查与规约验证。 |
| LLM | 大语言模型，一种基于深度学习的自然语言处理模型，能够生成文本、代码等。 |
| MatAXPY | PETSc中执行矩阵操作Y = alpha*X + Y的函数，其中alpha为标量，X和Y为矩阵。 |
📱 每天一份 AI 前沿日报
关注公众号，每天 09:00 推送 · 不错过任何重磅