論文の概要: $O_2$ is a multiple context-free grammar: an implementation-, formalisation-friendly proof
- arxiv url: http://arxiv.org/abs/2405.09396v1
- Date: Wed, 15 May 2024 14:51:11 GMT
- ステータス: 処理完了
- システム内更新日: 2024-05-16 13:06:44.780234
- Title: $O_2$ is a multiple context-free grammar: an implementation-, formalisation-friendly proof
- Title（参考訳）: O_2$は、複数の文脈自由文法である:実装、形式化に親しみやすい証明
- Authors: Marco B. Caminati,
- Abstract要約: それらを生成することができる文法の表現力に応じて言語を分類することは、計算言語学における根本的な問題である。
本稿では,各証明が検証された(すなわち,証明支援者によってチェックされる)アルゴリズムに繋がるかどうかを,MCFGを通して解析できるかどうかを体系的に研究する,計算的および証明理論的な視点から,既存の証明を解析する。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- Abstract: Classifying formal languages according to the expressiveness of grammars able to generate them is a fundamental problem in computational linguistics and, therefore, in the theory of computation. Furthermore, such kind of analysis can give insight into the classification of abstract algebraic structure such as groups, for example through the correspondence given by the word problem. While many such classification problems remain open, others have been settled. Recently, it was proved that $n$-balanced languages (i.e., whose strings contain the same occurrences of letters $a_i$ and $A_i$ with $1\leq i \leq n$) can be generated by multiple context-free grammars (MCFGs), which are one of the several slight extensions of context free grammars added to the classical Chomsky hierarchy to make the mentioned classification more precise. This paper analyses the existing proofs from the computational and the proof-theoretical point of views, systematically studying whether each proof can lead to a verified (i.e., checked by a proof assistant) algorithm parsing balanced languages via MCFGs. We conclude that none of the existing proofs is realistically suitable against this practical goal, and proceed to provide a radically new, elementary, extremely short proof for the crucial case $n \leq 2$. A comparative analysis with respect to the existing proofs is finally performed to justify why the proposed proof is a substantial step towards concretely obtaining a verified parsing algorithm for $O_2$.
- Abstract（参考訳）: それらを生成することができる文法の表現性に応じて形式言語を分類することは、計算言語学における基本的な問題であり、したがって計算理論における問題である。
さらに、そのような分析は、例えば、単語問題によって与えられる対応を通して、群のような抽象代数構造の分類に関する洞察を与えることができる。
このような分類問題の多くは未解決であるが、他の問題も解決されている。
最近、$n$バランスの言語(例えば、文字列が$a_i$と$A_i$と$\leq i \leq n$)が複数の文脈自由文法(MCFG)によって生成されることが証明された。
本稿では,既存の証明を計算的・理論的な視点から分析し,各証明が検証された(すなわち,証明アシスタントによってチェックされる)アルゴリズムに繋がるかどうかをMCFGを用いて解析する。
既存の証明はいずれも、この現実的な目標に対して現実的に適していないと結論し、決定的な場合の$n \leq 2$に対して、真に新しい、初等的で非常に短い証明を提供していく。
既存の証明との比較分析は、なぜ提案された証明が$O_2$の検証解析アルゴリズムを具体化するための重要なステップなのかを正当化するために、最終的に行われる。
関連論文リスト
- MathGAP: Out-of-Distribution Evaluation on Problems with Arbitrarily Complex Proofs [80.96119560172224]
大規模言語モデル(LLM)は、高い精度で算術語問題を解くことができるが、訓練された言語よりも複雑な問題にどのように一般化するかは、ほとんど分かっていない。
本研究では、任意に複雑な算術証明問題に対する LLM の評価フレームワーク、MathGAP を提案する。
論文 参考訳（メタデータ） (2024-10-17T12:48:14Z) - Detecting and explaining (in)equivalence of context-free grammars [0.6282171844772422]
文脈自由文法の同値性を決定し,証明し,説明するためのスケーラブルなフレームワークを提案する。
本稿では,本フレームワークの実装と,教育支援システム内で収集された大規模データセット上での評価を行う。
論文 参考訳（メタデータ） (2024-07-25T17:36:18Z) - Authorship Verification based on the Likelihood Ratio of Grammar Models [0.8749675983608172]
著者検証(英語: Authorship Verification、AV)とは、特定の著者によって書かれたかどうかを判断する一連の文書を分析するプロセスである。
我々は、$lambda_G$ (LambdaG) と呼ぶ量を計算する方法を提案する。
トレーニングに大量のデータを必要としないにも関わらず、LambdaGは計算複雑性の高い既存のAVメソッドよりも優れています。
論文 参考訳（メタデータ） (2024-03-13T12:25:47Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳（メタデータ） (2024-02-14T05:57:58Z) - "You Are An Expert Linguistic Annotator": Limits of LLMs as Analyzers of
Abstract Meaning Representation [60.863629647985526]
文意味構造の解析において, GPT-3, ChatGPT, および GPT-4 モデルの成功と限界について検討した。
モデルはAMRの基本形式を確実に再現でき、しばしばコアイベント、引数、修飾子構造をキャプチャできる。
全体としては,これらのモデルではセマンティック構造の側面を捉えることができるが,完全に正確なセマンティック解析や解析をサポートする能力には重要な制限が残されている。
論文 参考訳（メタデータ） (2023-10-26T21:47:59Z) - 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) - Language Models Are Greedy Reasoners: A Systematic Formal Analysis of
Chain-of-Thought [10.524051272257614]
大規模言語モデル(LLM)は、チェーン・オブ・シークレット・プロンプトが与えられた顕著な推論能力を示している。
本稿では, PrOntoQAと呼ばれる合成質問応答データセットを提案し, それぞれの例を合成世界モデルとして生成する。
これにより、生成された連鎖を形式解析の象徴的な証明に解析することができる。
論文 参考訳（メタデータ） (2022-10-03T21:34:32Z) - multiPRover: Generating Multiple Proofs for Improved Interpretability in
Rule Reasoning [73.09791959325204]
我々は、自然言語の事実と規則の形で明示的な知識を推論することを目的としている言語形式推論の一種に焦点を当てる。
PRoverという名前の最近の研究は、質問に答え、答えを説明する証明グラフを生成することによって、そのような推論を行う。
本研究では,自然言語規則ベースの推論のために複数の証明グラフを生成するという,新たな課題に対処する。
論文 参考訳（メタデータ） (2021-06-02T17:58:35Z) - The Logic for a Mildly Context-Sensitive Fragment of the Lambek-Grishin
Calculus [0.0]
ランベク・グリシン計算に基づく木に隣接した言語の証明論的特徴付けを行う。
純粋に構造的な結合性、有用性、HLGの証明ネットに関するグラフ理論的議論など、いくつかの新しい手法が証明に導入されている。
論文 参考訳（メタデータ） (2021-01-10T22:28:05Z) - Proof-theoretic aspects of NL$\lambda$ [0.0]
論理式 NL$lambda$ の証明理論解析について述べる。
証明ネットの新しい計算を導入し、論理学の逐次計算に関して、それが健全で完備であることを証明する。
2つの形式主義で提案される自然言語分析には,予期せぬ収束があることが示されている。
論文 参考訳（メタデータ） (2020-10-23T08:13:39Z) - The Return of Lexical Dependencies: Neural Lexicalized PCFGs [103.41187595153652]
語彙化PCFGのニューラルモデルを提案する。
実験により、この統一されたフレームワークは、いずれかの形式主義単独で達成されるよりも、両方の表現に対してより強い結果をもたらすことが示された。
論文 参考訳（メタデータ） (2020-07-29T22:12:49Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。