利用语言模型学习格式化 Coq 代码
人机交互
2020-07-01 v1 计算与语言
编程语言
软件工程
摘要
记录声明中的最后一个右括号是否应单独成行？rewrite 策略的参数之间是否应仅用一个空格分隔？Coq 代码往往因不同人和团队而呈现各异的书写风格。Coq 语言与记法的表现力、灵活性及可扩展性意味着 Coq 项目具有多种多样可辨识的编码风格，有时还被明确记录为命名与格式约定。特别地，即便缺乏经验的用户也能区分使用标准库和纯 Ltac 的 vernacular 与使用 Mathematical Components (MathComp) 库和 SSReflect 的惯用 vernacular。尽管编码约定对理解与维护十分重要，但文档化与强制实施成本高昂。基于规则的格式化工具（如 Coq 的美化器）灵活性有限，在大型验证项目中仅能覆盖所需约定的一小部分。我们认为，应用语言模型——一类用于捕捉语料规律的自然语言处理（NLP）技术——可为这一难题提供解决方案。更具体地，我们认为，基于从现有 Coq 代码自动学习约定、进而在恰当语境向用户建议惯用代码的方法，无论在投入还是效果上，都优于人工方法与静态分析工具。作为第一步，我们在此概述用于学习并建议 Coq 文件中空格格式的初始模型，给出针对 Coq 8.10 的初步实现，并在基于 MathComp 1.9.0 的语料（包含来自四个核心项目的 164k 行 Coq 代码）上进行评估。
引用
@article{arxiv.2006.16743,
title = {Learning to Format Coq Code Using Language Models},
author = {Pengyu Nie and Karl Palmskog and Junyi Jessy Li and Milos Gligoric},
journal= {arXiv preprint arXiv:2006.16743},
year = {2020}
}
备注
Accepted in the Coq Workshop 2020