一句话：用语言模型分析 Coq 与 HOL Light 证明语料，发现证明具有高度可预测的语言规律性，补全可节省超 60% 输入。
机械化证明助手虽能辅助检查证明一致性，但编写证明仍然繁琐，若能像编程语言那样借助统计语言模型提供自动化提示，将显著提升效率。本文研究证明是否具有“自然性”，即是否存在可供语言模型利用的重复语言模式。作者收集 Coq 和 HOL Light 两个证明助手的大型证明语料，并应用当前最先进的语言模型进行预测实验。结果表明，证明文本的预测难度与主流编程语言相当，具有高度可预测性；基于此实现的 Coq 证明代码补全可节省超过 60% 的键入工作量。由于证明在 CompCert 等大型可验证正确程序开发中日益核心，该发现为引入语言学启发的工具支持（如错误发现、证明重写、依赖推荐乃至证明步骤合成）开辟了空间。
Proofs play a key role in reasoning about programs and verification of properties of systems. Mechanized proof assistants help users in developing and checking the consistency of proofs using the proof language developed by the systems; but even then writing proofs is tedious and could benefit from automated insight. In this paper, we analyze proofs in two different proof assistant systems (Coq and HOL Light) to investigate if there is evidence of "naturalness" in these proofs: viz., recurring linguistic patterns that are amenable to language models, in the way that programming languages are known to be. Such models could be used to find errors, rewrite proofs, help suggest dependencies, and perhaps even synthesize (steps of) proofs. We apply state-of-the-art language models to large corpora of proofs to show that this is indeed the case: proofs are remarkably predictable, much like other programming languages. Code completion tools for Coq proofs could save over 60% of typing effort. As proofs have become increasingly central to writing provably correct, large programs (such as the CompCert C compiler), our demonstration that they are amenable to general statistical models unlocks a range of linguistics-inspired tool support.
DOI 原文 ·
@inproceedings{paperbot4671,
title = {On the naturalness of proofs},
author = {Vincent J. Hellendoorn and Premkumar T. Devanbu and Mohammad Amin Alipour},
booktitle = {FSE},
year = {2018},
doi = {10.1145/3236024.3264832}
}