arXiv cs.SE· Sirui Jiang, Dongming Xiang, Shichao Wu, Yuxuan Zhou, Yihong Wu, Fangze Zhu, Wang Lin, Guanjun Liu·· 2 小时前AI 评分22
DocAuth：为形式化库的自然语言文档引入归因检查
Beyond Correctness: Attribution of Natural-Language Documentation for Formal Libraries
AI 导读
研究者提出 DocAuth 文档生成方法，用"归因"（attribution）判断文档语句是否依赖函数的具体行为，并为每句附上可检验的形式化性质与证据。在 ACL2 定理证明器 Community Books 库的 150 个函数上，三个大语言模型对约三分之一的函数生成了可证明但不可归因的性质。
来源：arXiv cs.SE · arxiv.org