arXiv cs.AI· Sirui Jiang, Dongming Xiang, Shichao Wu, Yuxuan Zhou, Yihong Wu, Fangze Zhu, Wang Lin, Guanjun Liu·· 12 小时前AI 评分31
DocAuth：为形式化库的自然语言文档引入“归因”检查
Beyond Correctness: Attribution of Natural-Language Documentation for Formal Libraries
AI 导读
研究者提出 DocAuth 文档生成方法，用“归因”（attribution）判断文档语句是否依赖函数的具体行为，并为每句附上可检验的形式化性质与证据。
正文 · AI 翻译
摘要：形式化语言在软件工程中被广泛用于指定和验证程序性质。由于其数学记法和逻辑难以阅读，开发者常常依赖自然语言文档来理解形式化库中的函数。然而，一条文档陈述可能可证明为真，并且在函数行为改变后仍然成立。我们将陈述对函数具体行为的依赖称为归因，并给出一种检查它的方法。我们设计并实现了 DocAuth，这是一种文档生成方法，它使用归因来决定发布什么，并为每个发布的句子附上从该句恢复出的形式化性质，以及可检查的证据。在 ACL2 定理证明器的 Community Books 库中的 150 个函数上，三个大语言模型为约三分之一的函数生成了已证明但不可归因的性质。DocAuth 的归因率与基于变异的过滤器相当或更高，同时多提供 37% 的可归因句子。与仅检查真实性的流水线相比，它将第二个模型确认为可归因的已发布句子比例从 82.9% 提高到 94.7%。这些结果表明，可证明的真实性并不能保证文档反映函数的实际行为。归因作为为形式化库生成和评估文档的标准，补充了真实性。
| 评论： | 20 页，9 幅图，6 张表 |
| 主题： | 软件工程（cs.SE）；人工智能（cs.AI） |
| ACM 分类： | D.2.4；D.2.7；I.2.7 |
| 引用为： | arXiv:2610.33094 [cs.SE] |
| （或 arXiv:2610.33094v1 [cs.SE] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.33094 由 DataCite 颁发的 arXiv DOI |
提交历史
来自：Sirui Jiang [查看电子邮件]
[v1]
2026 年 10 月 22 日星期四 07:42:17 UTC（379 KB）
来源：arXiv cs.AI · arxiv.org