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