Trustworthy Formal Natural Language Specifications

要約

インタラクティブ証明アシスタントは、人間が設計した数学的主張の証明を実装に高い信頼性を持ってチェックするために慎重に構築されたコンピュータ プログラムです。
ただし、これは正式な主張の真実性を検証するだけであり、自然言語で行われた主張から誤って翻訳された可能性があります。
これは、自然言語仕様に関してソフトウェアの正しさを正式に検証するために証明アシスタントを使用する場合に特に問題になります。
非公式から公式への変換は、依然として困難で時間のかかるプロセスであり、正確性を監査するのが困難です。
この論文は、証明アシスタント自体の信頼性と監査可能性を確立するために使用される原則と一致して、既存の証明アシスタント内で、自然言語の表現豊かなサブセットで書かれた仕様のサポートを構築することが可能であることを示します。
私たちは、モジュール式に拡張可能な英語の正式なサブセットで仕様を提供する手段を実装し、リーン証明アシスタント内で完全に正式なクレームに自動的に変換します。
私たちのアプローチは拡張可能 (文法構造に永続的な制限を設けない) で、モジュール型 (新しい単語に関する情報をライブラリと一緒に配布できる) であり、各単語がどのように解釈されたか、および文の構造が意味を計算するためにどのように使用されたかを説明する証明証明書を生成します。
私たちはプロトタイプを、一般的な教科書に掲載されている形式仕様のさまざまな英語記述を無駄のない形式に翻訳することに適用します。
適度な語彙を使用して、語彙サイズに関連するわずかな変更を加えるだけで、すべてを正しく翻訳できます。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google