什么在证明中？分析 F* 和 Verus 中的专家证明编写过程
软件工程
2025-08-06 v1 人机交互
摘要
证明导向编程语言 (POPL) 赋予开发者在代码中编写形式正确性证明的能力，提供代码遵循指定要求的形式保证。尽管具有强大的功能，POPL 仍面临学习曲线陡峭且尚未被广泛采纳。缺乏对证明开发过程及专家证明开发人员如何与 POPL 交互的理解，阻碍了有效证明工程的发展以及证明合成模型/工具的开发。在本研究中，我们进行了一项用户研究，收集并分析了来自 eight 名专家在 F* 和 Verus 两种语言中进行的细粒度源代码遥测数据。结果揭示了关于专家如何推理证明以及在证明开发过程中遇到的关键挑战的有趣趋势和模式。我们识别出三种 distinct strategies 以及多个不包含在最终代码快照中的非正式实践，这些实践与任务结果预测性强。我们将这些发现翻译为具体的 AI 证明助手设计指导方针：鼓励早期规范草拟、显式子目标分解、受限主动错误以及规范化验证器交互。我们还呈现了一个基于这些建议的 F* 证明代理案例研究，展示了相对于基线 LLM 的 improved performance。
引用
@article{arxiv.2508.02733,
title = {What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus},
author = {Rijul Jain and Shraddha Barke and Gabriel Ebner and Md Rakib Hossain Misu and Shan Lu and Sarah Fakhoury},
journal= {arXiv preprint arXiv:2508.02733},
year = {2025}
}