論文の概要: Trustworthy Formal Natural Language Specifications
- arxiv url: http://arxiv.org/abs/2310.03885v1
- Date: Thu, 5 Oct 2023 20:41:47 GMT
- ステータス: 処理完了
- システム内更新日: 2023-10-10 06:35:31.846768
- Title: Trustworthy Formal Natural Language Specifications
- Title(参考訳): 信頼できる正式な自然言語仕様
- Authors: Colin S. Gordon, Sergey Matskevich
- Abstract要約: 本稿では、自然言語の表現的サブセットで書かれた仕様を構築できることを示す。
モジュール的に形式化された英語のサブセットで仕様を提供する手段を実装し、それらを形式的なクレームに自動的に変換する。
我々は,各単語の解釈方法と文の構造を用いて意味を計算したことを示す証明証明書を作成した。
- 参考スコア(独自算出の注目度): 3.8073142980733
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: 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.
- Abstract(参考訳): 対話型証明アシスタントは、人間によって設計された数学的クレームの証明を、実装に高い信頼性で確認するために、慎重に構築されたコンピュータプログラムである。
しかし、これは、自然言語でなされた主張から誤訳されたかもしれない形式的主張の真理のみを証明している。
証明アシスタントを使用して自然言語仕様に関してソフトウェアの正当性を正式に検証する場合、これは特に問題となる。
形式的から形式的への翻訳は、正確さの監査が難しい困難で時間を要するプロセスであり続けている。
本稿では,自然言語の表現豊かなサブセットで記述された仕様を,既存の証明アシスタント内で構築することが可能であり,証明アシスタント自身で信頼と監査性を確立するための原則と一致していることを示す。
モジュール的に拡張可能な英語の形式的なサブセットで仕様を提供する手段を実装し、それらが自動的に形式的なクレームに変換されるようにします。
提案手法は拡張可能であり(文法構造に恒久的な制限はない)、モジュラー(図書館にまたがる新しい単語に関する情報を配布できる)、各単語の解釈方法と文構造を用いて意味を計算したことを示す証明証明書を生成する。
われわれのプロトタイプは、一般的な教科書からリーン形式への形式的仕様の様々な英語記述の翻訳に適用するが、すべては、レキシコンサイズに関する小さな修正しか持たない、控えめなレキシコンで正しく翻訳できる。
関連論文リスト
- Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳(メタデータ) (2024-07-14T01:43:07Z) - How Proficient Are Large Language Models in Formal Languages? An In-Depth Insight for Knowledge Base Question Answering [52.86931192259096]
知識ベース質問回答(KBQA)は,知識ベースにおける事実に基づいた自然言語質問への回答を目的としている。
最近の研究は、論理形式生成のための大規模言語モデル(LLM)の機能を活用して性能を向上させる。
論文 参考訳(メタデータ) (2024-01-11T09:27:50Z) - Formal Proofs as Structured Explanations: Proposing Several Tasks on
Explainable Natural Language Inference [0.16317061277457]
構造化された説明を用いてNLIタスクを定義する方法を示す。
提案したタスクは、説明の粒度で定義される難易度に応じて順序付けすることができる。
論文 参考訳(メタデータ) (2023-11-15T01:24:09Z) - nl2spec: Interactively Translating Unstructured Natural Language to
Temporal Logics with Large Language Models [3.1143846686797314]
大規模言語モデル(LLM)を適用するためのフレームワークであるnl2specは、構造化されていない自然言語から正式な仕様を導出する。
本稿では,自然言語におけるシステム要求のあいまいさを検知し,解決する新たな手法を提案する。
ユーザは、これらのサブ翻訳を反復的に追加、削除、編集して、不正なフォーマル化を修正する。
論文 参考訳(メタデータ) (2023-03-08T20:08:53Z) - Towards Autoformalization of Mathematics and Code Correctness:
Experiments with Elementary Proofs [5.045988012508899]
オートフォーマル化(Autoformalization)は、自然言語で書かれた証明を、対話的定理証明を通じてコンピュータで検証可能な形式表現に変換することによって、この問題に対処しようとする。
本稿では, 基本数学的証明を, Coq の対話的定理証明器の言語における等価な形式化に変換する, ユニバーサルトランスフォーマーアーキテクチャに基づく意味解析手法を提案する。
論文 参考訳(メタデータ) (2023-01-05T17:56:00Z) - Language Models as Inductive Reasoners [125.99461874008703]
本稿では,帰納的推論のための新しいパラダイム(タスク)を提案し,自然言語の事実から自然言語規則を誘導する。
タスクのための1.2kルールファクトペアを含むデータセットDEERを作成し,ルールと事実を自然言語で記述する。
我々は、事前訓練された言語モデルが自然言語の事実から自然言語規則をいかに誘導できるかを、初めてかつ包括的な分析を行う。
論文 参考訳(メタデータ) (2022-12-21T11:12:14Z) - Towards a Mathematics Formalisation Assistant using Large Language
Models [5.485439959027125]
リーン定理証明器の形式化を支援するために,大規模な言語モデル(Codex)の能力について検討する。
コーデックスは、短い数学的ステートメントを120ドルの定理ステートメントに対して75%近い精度でアンダーグレードレベルで定式化することができる。
新たなプロンプト戦略により、コーデックスはこれらの証明を自然言語で定式化することができ、12のコーデックスのうち少なくとも1つの完備化は、完全な証明に容易に修正できることが示される。
論文 参考訳(メタデータ) (2022-11-14T16:52:32Z) - Natural Language Specifications in Proof Assistants [0.0]
既存の証明アシスタント内で自然言語仕様のサポートを構築することができる。
本稿では,既存の証明アシスタント内で自然言語仕様のサポートを構築することが可能であることを論じる。
論文 参考訳(メタデータ) (2022-05-16T17:05:45Z) - Learning Symbolic Rules for Reasoning in Quasi-Natural Language [74.96601852906328]
我々は,ルールを手作業で構築することなく,自然言語入力で推論できるルールベースシステムを構築した。
本稿では,形式論理文と自然言語文の両方を表現可能な"Quasi-Natural"言語であるMetaQNLを提案する。
提案手法は,複数の推論ベンチマークにおける最先端の精度を実現する。
論文 参考訳(メタデータ) (2021-11-23T17:49:00Z) - A Matter of Framing: The Impact of Linguistic Formalism on Probing
Results [69.36678873492373]
BERT (Delvin et al.) のような事前訓練されたコンテキスト化エンコーダは、下流タスクで顕著なパフォーマンスを示す。
調査における最近の研究は、事前学習中にこれらのモデルによって暗黙的に学習された言語知識について調査している。
形式主義の選択は調査結果に影響を及ぼすか?
BERTによる意味的役割情報とプロトロール情報のエンコーディングにおける言語学的意義の相違は,形式主義に依存している。
論文 参考訳(メタデータ) (2020-04-30T17:45:16Z) - On the Importance of Word Order Information in Cross-lingual Sequence
Labeling [80.65425412067464]
ソース言語の単語順に適合する言語間モデルでは、ターゲット言語を処理できない可能性がある。
本研究では,ソース言語の単語順序に敏感なモデルを作成することで,対象言語の適応性能が向上するかどうかを検討する。
論文 参考訳(メタデータ) (2020-01-30T03:35:44Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。