論文の概要: Neural Proof Nets

• arxiv url: http://arxiv.org/abs/2009.12702v1
• Date: Sat, 26 Sep 2020 22:48:47 GMT
• ステータス: 処理完了
• システム内更新日: 2022-10-14 08:37:30.541315
• Title: Neural Proof Nets
• Title（参考訳）: ニューラルプルーフネット
• Authors: Konstantinos Kogkalidis, Michael Moortgat, Richard Moot
• Abstract要約: 本稿では,Sinkhorn ネットワークをベースとした証明ネットのニューラルバリアントを提案する。 AEThelでは,テキスト文の正しい書き起こしを線形ラムダ計算の証明や用語として70%の精度で行うことができる。
• 参考スコア（独自算出の注目度）: 0.8379286663107844
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Linear logic and the linear {\lambda}-calculus have a long standing tradition in the study of natural language form and meaning. Among the proof calculi of linear logic, proof nets are of particular interest, offering an attractive geometric representation of derivations that is unburdened by the bureaucratic complications of conventional prooftheoretic formats. Building on recent advances in set-theoretic learning, we propose a neural variant of proof nets based on Sinkhorn networks, which allows us to translate parsing as the problem of extracting syntactic primitives and permuting them into alignment. Our methodology induces a batch-efficient, end-to-end differentiable architecture that actualizes a formally grounded yet highly efficient neuro-symbolic parser. We test our approach on {\AE}Thel, a dataset of type-logical derivations for written Dutch, where it manages to correctly transcribe raw text sentences into proofs and terms of the linear {\lambda}-calculus with an accuracy of as high as 70%.
• Abstract（参考訳）: 線形論理と線形 {\lambda}-計算は自然言語形式と意味の研究において長い伝統を持っている。 線形論理の証明計算の中で、証明ネットは特に興味深く、従来の証明論的形式の官僚的複雑さによって妨げられない導出の魅力的な幾何学的表現を提供する。 セット理論学習の最近の進歩に基づき、シンクホーンネットワークに基づく証明ネットのニューラルバリアントを提案し、構文的プリミティブを抽出し、それらをアライメントする問題として解析を翻訳する。 本手法は,形式的かつ高効率なニューロシンボリック解析器を実現するバッチ効率でエンドツーエンドの微分可能アーキテクチャを誘導する。 そこで我々は,オランダ語における型論理的導出のデータセットである {\AE}Thel を用いて,原文を線形な {\lambda}-計算の証明と用語に精度70%の精度で正しく転写する手法を検証した。

関連論文リスト

• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。 本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。 我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
  論文  参考訳（メタデータ） (2023-10-23T17:58:40Z)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。 我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。 我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
  論文  参考訳（メタデータ） (2023-10-16T08:42:39Z)
• Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs [5.045988012508899]
  オートフォーマル化(Autoformalization)は、自然言語で書かれた証明を、対話的定理証明を通じてコンピュータで検証可能な形式表現に変換することによって、この問題に対処しようとする。 本稿では, 基本数学的証明を, Coq の対話的定理証明器の言語における等価な形式化に変換する, ユニバーサルトランスフォーマーアーキテクチャに基づく意味解析手法を提案する。
  論文  参考訳（メタデータ） (2023-01-05T17:56:00Z)
• On Parsing as Tagging [66.31276017088477]
  そこで我々は,現在最先端の選挙区タグであるテトラタグを減らして,シフト-リデュース解析を行う方法を示す。 我々は、線形化器、学習者、復号器の異なる選択でタグ付けパイプラインの分類を実証的に評価する。
  論文  参考訳（メタデータ） (2022-11-14T13:37:07Z)
• A Neural Model for Regular Grammar Induction [8.873449722727026]
  我々は文法を計算のモデルとして扱い、正および負の例から正規文法を誘導する新しいニューラルアプローチを提案する。 我々のモデルは完全に説明可能であり、その中間結果は部分解析として直接解釈可能であり、十分なデータが得られると任意の正規文法を学習することができる。
  論文  参考訳（メタデータ） (2022-09-23T14:53:23Z)
• A Logic-Based Framework for Natural Language Inference in Dutch [1.0178220223515955]
  オランダ語文ペア間の関係を導出するための枠組みを提案する。 提案するフレームワークは、推論ラベルにつながる検査可能な証明を生成するために、論理ベースの推論に依存している。 我々は最近作成されたオランダの自然言語推論データセットの推論パイプラインを評価する。
  論文  参考訳（メタデータ） (2021-10-07T10:34:46Z)
• Extracting Grammars from a Neural Network Parser for Anomaly Detection in Unknown Formats [79.6676793507792]
  強化学習は、ある未知のフォーマットで文を解析するために、人工知能を訓練する技術として、最近約束されている。 本稿では、ニューラルネットワークから生成規則を抽出し、これらの規則を用いて、ある文が名目か異常かを決定する手順を提案する。
  論文  参考訳（メタデータ） (2021-07-30T23:10:24Z)
• Refining Labelled Systems for Modal and Constructive Logics with Applications [0.0]
  この論文は、モーダル論理や構成論理のセマンティクスを「経済的な」証明システムに変換する手段として機能する。 精製法は、ラベル付きおよびネストされたシーケント計算の2つの証明理論パラダイムを結合する。 導入された洗練されたラベル付き電卓は、デオン性STIT論理に対する最初の証明探索アルゴリズムを提供するために使用される。
  論文  参考訳（メタデータ） (2021-07-30T08:27:15Z)
• The Logic for a Mildly Context-Sensitive Fragment of the Lambek-Grishin Calculus [0.0]
  ランベク・グリシン計算に基づく木に隣接した言語の証明論的特徴付けを行う。 純粋に構造的な結合性、有用性、HLGの証明ネットに関するグラフ理論的議論など、いくつかの新しい手法が証明に導入されている。
  論文  参考訳（メタデータ） (2021-01-10T22:28:05Z)
• Provably Efficient Neural Estimation of Structural Equation Model: An Adversarial Approach [144.21892195917758]
  一般化構造方程式モデル(SEM)のクラスにおける推定について検討する。 線形作用素方程式をmin-maxゲームとして定式化し、ニューラルネットワーク(NN)でパラメータ化し、勾配勾配を用いてニューラルネットワークのパラメータを学習する。 提案手法は,サンプル分割を必要とせず,確固とした収束性を持つNNをベースとしたSEMの抽出可能な推定手順を初めて提供する。
  論文  参考訳（メタデータ） (2020-07-02T17:55:47Z)
• Logical Natural Language Generation from Open-Domain Tables [107.04385677577862]
  本稿では,その事実に関連付けられた自然言語文をモデルで生成するタスクを提案する。 提案した論理的 NLG 問題の研究を容易にするために,幅広い論理的・記号的推論を特徴とする既存の TabFact データセットcitechen 2019tabfact を用いる。 新しいタスクは、シーケンス順序と論理順序のミスマッチのため、既存のモノトニック生成フレームワークに課題をもたらす。
  論文  参考訳（メタデータ） (2020-04-22T06:03:10Z)

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

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。