论文标题
证明助手中的自然语言规格
Natural Language Specifications in Proof Assistants
论文作者
论文摘要
交互式证明助理是精心构建的计算机程序，以对实施充满信心地检查数学主张的人类设计的证明。但是，这只能证实正式主张的真理，这可能是从自然语言提出的主张中被误认为的。当使用证明助手正式验证软件相对于自然语言规范的正确性时，这尤其有问题。从非正式到正式的翻译仍然是一个具有挑战性的，耗时的过程，很难审核正确的正确性。本文认为，有可能在现有证明助理中建立对自然语言规格的支持，以补充用于建立证明助手本身的信任和可审计性的原则。
Interactive proof assistants are computer programs carefully constructed to check a human-designed proof of a mathematical claim with high confidence in the implementation. However, this only validates truth of a formal claim, which may have been mistranslated from a claim made in natural language. This is especially problematic when using proof assistants to formally verify the correctness of software with respect to a natural language specification. The translation from informal to formal remains a challenging, time-consuming process that is difficult to audit for correctness. This paper argues that it is possible to build support for natural language specifications within existing proof assistants, in a way that complements the principles used to establish trust and auditability in proof assistants themselves.
