AI 中文总结
研究软件工程中意图规范和验证问题，提出用属性模板解决验证候选属性和实施PBT的子问题，设计智能体双轨验证框架，经评估该框架能提高证明成功率、减少幻觉、降低成本并提升代码覆盖，还能发现模型与实现差距。
AI 中文摘要
随着人工智能使代码生成成本降低，软件工程的新瓶颈已转向意图规范和验证。克服人工智能驱动编码的耐久性危机需要超越传统的模糊测试：每个候选属性必须在模型上被证明正确，并在实际实现中成立，这使得形式证明和基于属性的系统测试（PBT）相辅相成。大规模验证属性需要解决两个子问题：验证候选属性和在无人工智能幻觉的情况下实施PBT。我们假设，作为属性模板的重复属性模式可同时解决这两个问题。本文研究了Apache Spark中的重复属性模式。在数据密集型可扩展计算系统中，正确性属性源于数据分区、计算分解和数据流计算的原则。例如，聚合分解将在整个数据集上执行的全局函数与随后是重组器的局部函数相关联。我们设计了一个智能体双轨验证框架，该框架使用属性模板在Lean 4定理证明器中正式验证正确性，并将PBT模板实例化为可执行的PySpark测试。我们的评估表明，属性模板将智能体证明工程的成功率提高了2.6倍（平均1.6倍），并将证明幻觉减少了59%。模板引导的PBT合成将意图偏差从22减少到1，并将合成成本降低了5.7倍（平均3.8倍）。模板引导的合成在代码覆盖方面进一步超过了先进的Spark模糊器，并接近基于无引导大语言模型的PBT。最后，比较这两条轨道很有意义：当一个证明成功而PBT找到一个反例时，不匹配就识别出形式模型和实现之间的差距。
英文摘要
As the cost of code generation becomes cheaper with AI, the new bottleneck in software engineering has shifted to intent specification and validation. Overcoming this durability crisis of AI-driven coding requires more than traditional fuzzing: each candidate property must be proven correct over a model and shown to hold on the real implementation, making formal proof and systematic property-based testing (PBT) complementary. However, validating properties this way at scale requires solving two subproblems: verifying candidate properties and operationalizing PBT without AI hallucination. We hypothesize that recurring property patterns, cast as property templates--abstract, parameterized forms with holes--address both at once. This paper investigates recurring property patterns in Apache Spark. In data-intensive scalable computing systems, correctness properties arise from the principles of data partition, computation decomposition, and dataflow computation. For instance, aggregation decomposition relates a global function executed on the entire dataset to a local function followed by a recombiner. We design an agentic, dual-track validation framework that uses property templates to formally verify correctness in the Lean 4 theorem prover and instantiate PBT templates as executable PySpark tests. Our evaluation shows that property templates increase agentic proof engineering success by up to 2.6x (1.6x on average) and reduce proof hallucinations by 59%. Template-guided PBT synthesis reduces intent misalignments from 22 to 1 and cuts synthesis cost by up to 5.7x (3.8x on average). Template-guided synthesis further exceeds a state-of-the-art Spark fuzzer and approaches unguided LLM-based PBT on code coverage. Finally, comparing the two tracks is informative: when a proof succeeds yet a PBT finds a counterexample, the mismatch identifies a gap between the formal model and implementation.
Comments12 pages, 7 figures, 4 tables; supplementary material included as ancillary file
