Trustworthy Formal Natural Language Specifications
Trustworthy Formal Natural Language Specifications
复制标题
值得信赖的正式自然语言规范
DOI：
10.1145/3622758.3622890
复制
发表时间：
2023
期刊：
影响因子：
--
通讯作者：
Matskevich, Sergey
中科院分区：
文献类型：
--
作者：
Gordon, Colin S.;Matskevich, Sergey
交互式证明助手是精心构建的计算机程序，用于检查人工设计的数学声明的证明，并在实施过程中具有很高的置信度。然而，这只验证了正式索赔的真实性，这可能是从自然语言提出的索赔错误翻译而来的。当使用证明助手来正式验证软件相对于自然语言规范的正确性时，这尤其成问题。从非正式到正式的转换仍然是一个具有挑战性的、耗时的过程，很难对正确性进行审计。本文展示了在现有的证明助手中建立对用自然语言的表达子集编写的规范的支持是可能的，这与用于建立对证明助手本身的信任和可审核性的原则一致。我们实现了一种方法，以模块可扩展的英语形式子集提供规范，并将它们自动转换为正式声明，完全在精益证明助手中。我们的方法是可扩展的(对语法结构没有永久的限制)，模块化(允许与库一起分发关于新词的信息)，并生成证明证书，解释如何解释每个单词以及如何使用句子的结构来计算含义。我们将我们的原型应用于将流行教科书中的各种形式规范的英语描述翻译成精益形式化；所有这些都可以用适度的词典正确翻译，只需对词典大小进行微小修改。
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.
登录
查看更多内容
使用语言模型学习的局限性
DOI：
--
发表时间：
2023
期刊：
STARSEM
影响因子：
--
作者：
Nicholas M. Asher;Swarnadeep Bhar;Akshay Chaturvedi;Julie Hunter;Soumya Paul
通讯作者：
Soumya Paul
多模态语言推理
DOI：
10.1007/bf00159344
发表时间：
1995
期刊：
Journal of Logic, Language and Information
影响因子：
--
作者：
M. Moortgat
通讯作者：
M. Moortgat
DOI：
10.3115/1067807.1067836
发表时间：
2003
期刊：
Linguistic Issues in Language Technology
影响因子：
--
作者：
Geert;Jason Baldridge
通讯作者：
Jason Baldridge
苹果脚本
DOI：
10.1145/1238844.1238845
发表时间：
2007
期刊：
Proceedings of the third ACM SIGPLAN conference on History of programming languages
影响因子：
--
作者：
W. Cook
通讯作者：
W. Cook
可扩展的校样文本编辑器
DOI：
10.1007/3-540-44404-1_6
发表时间：
2000
期刊：
BRICS Report Series
影响因子：
--
作者：
T. Hallgren;Aarne Ranta
通讯作者：
Aarne Ranta