Fugu-MT 論文翻訳(概要): Natural Language Specifications in Proof Assistants

論文の概要: Natural Language Specifications in Proof Assistants

arxiv url: http://arxiv.org/abs/2205.07811v1
Date: Mon, 16 May 2022 17:05:45 GMT
ステータス: 処理完了
システム内更新日: 2022-05-17 16:53:56.361293
Title: Natural Language Specifications in Proof Assistants
Title（参考訳）: 証明アシスタントにおける自然言語仕様
Authors: Colin S. Gordon, Sergey Matskevich
Abstract要約: 既存の証明アシスタント内で自然言語仕様のサポートを構築することができる。本稿では,既存の証明アシスタント内で自然言語仕様のサポートを構築することが可能であることを論じる。
参考スコア（独自算出の注目度）: 0.0
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 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.
Abstract（参考訳）: 対話型証明アシスタントは、人間によって設計された数学的クレームの証明を、実装に高い信頼性で確認するために、慎重に構築されたコンピュータプログラムである。しかし、これは、自然言語でなされた主張から誤訳されたかもしれない形式的主張の真理のみを証明している。証明アシスタントを使用して自然言語仕様に関してソフトウェアの正当性を正式に検証する場合、これは特に問題となる。形式的から形式的への翻訳は、正確さの監査が難しい困難で時間を要するプロセスであり続けている。本稿は,証明アシスタント自体の信頼性と監査性を確立するために用いられる原則を補完する形で,既存の証明アシスタント内で自然言語仕様をサポートすることができる,と論じる。

関連論文リスト

Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文参考訳（メタデータ） (2024-07-14T01:43:07Z)
LLM Critics Help Catch Bugs in Mathematics: Towards a Better Mathematical Verifier with Natural Language Feedback [71.95402654982095]
本研究では,自然言語フィードバック型検証器Math-Minosを提案する。実験の結果,少量の自然言語フィードバックが検証器の性能を大幅に向上させることがわかった。
論文参考訳（メタデータ） (2024-06-20T06:42:27Z)
Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
本稿では,検証対応言語における仕様の質を評価するための指標を提案する。 MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
論文参考訳（メタデータ） (2024-06-14T06:52:08Z)
Trustworthy Formal Natural Language Specifications [3.8073142980733]
本稿では、自然言語の表現的サブセットで書かれた仕様を構築できることを示す。モジュール的に形式化された英語のサブセットで仕様を提供する手段を実装し、それらを形式的なクレームに自動的に変換する。我々は,各単語の解釈方法と文の構造を用いて意味を計算したことを示す証明証明書を作成した。
論文参考訳（メタデータ） (2023-10-05T20:41:47Z)
ProofBuddy: A Proof Assistant for Learning and Monitoring [0.0]
証明能力(Proof competence)、すなわち、(数学的な)証明を書き、チェックする能力は、コンピュータ科学において重要なスキルである。主な問題は、形式言語の正しい使用と証明、特に学生自身の証明が完璧で正しいかどうかの確認である。多くの著者は、証明能力を教えるのに証明アシスタントを使うことを提案したが、その方法の有効性は明らかではない。デンマーク工科大学でProofBuddyのユーザビリティに関する予備的な研究を行った。
論文参考訳（メタデータ） (2023-08-14T07:08:55Z)
STL: Surprisingly Tricky Logic (for System Validation) [0.04301276597844757]
検証正当性を決定する上では,仕様書の真正性,形式的手法に精通した被験者の親密性,教育水準が重要な要因であることが判明した。参加者は肯定バイアスを示し、有効仕様の精度は大幅に向上したが、無効仕様の精度は著しく低下した。
論文参考訳（メタデータ） (2023-05-26T21:01:26Z)
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)
NaturalProver: Grounded Mathematical Proof Generation with Language Models [84.2064569475095]
自然数理言語における定理証明は、数学の進歩と教育において中心的な役割を果たす。本研究では,背景参照を条件づけて証明を生成する言語モデルであるNaturalProverを開発する。 NaturalProverは、短い(2-6ステップ)証明を必要とするいくつかの定理を証明でき、40%の時間で正しいと評価された次のステップの提案を提供することができる。
論文参考訳（メタデータ） (2022-05-25T17:01:18Z)
Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文参考訳（メタデータ） (2022-05-25T02:22:30Z)
Data Annealing for Informal Language Understanding Tasks [66.2988222278475]
本稿では,非公式な言語タスクのパフォーマンスギャップを埋めるために,データアニーリング変換学習手法を提案する。これは、非公式言語でBERTのような事前訓練されたモデルを利用することに成功した。
論文参考訳（メタデータ） (2020-04-24T09:27:09Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。