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 shows that it is possible to build support for specifications written in expressive subsets of natural language, within existing proof assistants, consistent with the principles used to establish trust and auditability in proof assistants themselves. We implement a means to provide specifications in a modularly extensible formal subset of English, and have them automatically translated into formal claims, entirely within the Lean proof assistant. Our approach is extensible (placing no permanent restrictions on grammatical structure), modular (allowing information about new words to be distributed alongside libraries), and produces proof certificates explaining how each word was interpreted and how the sentence's structure was used to compute the meaning. We apply our prototype to the translation of various English descriptions of formal specifications from a popular textbook into Lean formalizations; all can be translated correctly with a modest lexicon with only minor modifications related to lexicon size.

翻译：交互式证明助手是精心构建的计算机程序，旨在以高置信度检查数学命题的人工验证证明。然而，这仅验证了形式化命题的真实性，而该命题可能源自对自然语言表述的错误翻译。当使用证明助手根据自然语言规约对软件正确性进行形式化验证时，这一问题尤为突出。从非形式化到形式化的转换仍是一个耗时且难以审计正确性的挑战性过程。本文表明，在现有证明助手中，可以构建对自然语言表达性子集规约的支持，并与证明助手自身建立信任和可审计性的原则保持一致。我们实现了一种方法，可在Lean证明助手内部提供模块化可扩展的英语形式化子集规约，并将其自动翻译为形式化命题。我们的方法具有可扩展性（不对语法结构施加永久限制）、模块化（允许将新词信息与库一同分发），并生成证明证书，解释每个单词的解释方式以及句子结构用于计算语义的过程。我们将原型系统应用于流行教材中多种英语形式化规约描述的Lean形式化翻译；所有规约均可通过中等规模的词典正确翻译，仅需对词典规模进行微小调整。