数据密集型计算中通过属性模板进行代理证明和基于属性的测试

随着人工智能的代码生成成本变得越来越便宜，软件工程的新瓶颈已经转移到意图规范和验证上。克服人工智能驱动编码的持久性危机需要的不仅仅是传统的模糊测试：每个候选属性都必须在模型上被证明是正确的，并被证明可以在实际实现中保持不变，从而使形式证明和基于属性的系统测试（PBT）相辅相成。然而，以这种方式大规模验证属性需要解决两个子问题：验证候选属性和在没有人工智能幻觉的情况下操作 PBT。我们假设，将重复出现的属性模式转换为属性模板（带有漏洞的抽象参数化形式）可以同时解决这两个问题。本文研究了 Apache Spark 中的重复属性模式。在数据密集型可扩展计算系统中，正确性属性源于数据分区、计算分解和数据流计算的原理。例如，聚合分解将在整个数据集上执行的全局函数与后跟重组器的局部函数相关联。我们设计了一个代理的双轨验证框架，该框架使用属性模板来正式验证 Lean 4 定理证明器中的正确性，并将 PBT 模板实例化为可执行的 PySpark 测试。我们的评估表明，属性模板将代理证明工程的成功率提高了 2.6 倍（平均 1.6 倍），并将证明幻觉减少了 59%。模板引导的 PBT 合成将意图偏差从 22 减少到 1，并将合成成本降低高达 5.7 倍（平均 3.8 倍）。模板引导综合进一步超越了最先进的 Spark 模糊器，并在代码覆盖率上接近基于 LLM 的无引导 PBT。最后，比较这两个轨道可以提供丰富的信息：当证明成功但 PBT 找到反例时，这种不匹配就确定了正式模型和实现之间的差距。