論文の概要: Coherency through formalisations of Structured Natural Language, A case study on FRETish
- arxiv url: http://arxiv.org/abs/2605.10462v1
- Date: Mon, 11 May 2026 12:30:53 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-13 02:24:05.562208
- Title: Coherency through formalisations of Structured Natural Language, A case study on FRETish
- Title（参考訳）: 構造化自然言語の形式化によるコヒーレンシー : FRETishを事例として
- Authors: Joost J. Joosten, Marina López Chamosa, Sofía Santiago Fernández,
- Abstract要約: 形式化とは、システム要件を形式言語で記述するプロセスである。
本稿では,ホルマライゼーションによるコヒーレンシ(コヒーレンシー)の新たなガイドラインを提案する。
本稿では,NASA の形式的要求抽出ツール FRET を分析し,制御された自然言語 FRETish を MTL の形式言語に自動翻訳する手法を提案する。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by-nc-sa/4.0/
- Abstract: Formalisation is the process of writing system requirements in a formal language. These requirements mostly originate in Natural Language. In the field of Formal Methods, formalisation is often identified as one of the most delicate and complicated steps in the verification process. Not seldomly, formalisation tools and environments choose various levels of requirement descriptions: Natural Language, Technical Language, Diagram Representations and Formal Language, to mention a few. In the literature, there are various maxims and principles of good practice to guide the process of requirement formalisation. In this paper we propose a new guideline: Coherency through Formalisations. The guideline states that the different levels of formalisation mentioned above should roughly follow the same logical structure. The principle seems particularly relevant in the setting where LLMs are prompted to perform reasoning tasks that can be checked by formal tools using Structured Natural Language to act as an intermediate layer bridging both paradigms. In the light of coherency, we analyze NASA's Formal Requirement Elicitation Tool FRET and propose an alternative automated translation of the Controlled Natural Language FRETish to the formal language of MTL. We compare our translation to the original translation and prove equivalence using model checking. Some statistics are performed which seem to favor the new translation. As expected, the translation process yielded interesting reflections and revealed inconsistencies which we present and discuss.
- Abstract（参考訳）: 形式化とは、システム要件を形式言語で記述するプロセスである。
これらの要件は主に自然言語に起因している。
形式的手法の分野では、形式化は検証プロセスにおいて最もデリケートで複雑なステップの1つとして認識されることが多い。
形式化ツールや環境は、自然言語、テクニカル言語、ダイアグラム表現、フォーマル言語など、さまざまなレベルの要件記述を選択します。
文献には、要求の定式化のプロセスを導くための善行の極大さと原則が多岐にわたる。
本稿では,ホルマライゼーションによるコヒーレンシ(コヒーレンシー)の新たなガイドラインを提案する。
ガイドラインでは、上記の形式化の異なるレベルは、大まかに同じ論理構造に従うべきであるとしている。
LLMは、構造化自然言語を使って、両方のパラダイムをブリッジする中間層として機能するために、形式的なツールでチェックできる推論タスクを実行するように促される。
整合性の観点から,NASAの形式的要求抽出ツールFRETを分析し,制御された自然言語FRETishをMTLの形式言語に自動翻訳する手法を提案する。
我々は,翻訳を原翻訳と比較し,モデル検査を用いて等価性を証明した。
新しい翻訳が好まれる統計もある。
予想通り、翻訳プロセスは興味深いリフレクションをもたらし、我々が提示し議論する不整合を明らかにした。
関連論文リスト
- Shaping Schema via Language Representation as the Next Frontier for LLM Intelligence Expanding [88.11781604392606]
本稿では,言語表現を実世界の地図化とモデル化に使用される言語的・象徴的構造として定義する。
我々は、高度な言語表現によるスキーマ形成が、大規模言語モデルの拡張の次のフロンティアであると主張している。
論文 参考訳（メタデータ） (2026-05-10T02:42:29Z) - NILE: Formalizing Natural-Language Descriptions of Formal Languages [0.0]
本稿では,形式言語の自然言語記述を形式表現と比較し,意味的差異を説明する。
本研究では,ナイル表現が自然言語記述の構文構造を反映するようにデザインされた形式言語であるナイルの表現言語を提案する。
論文 参考訳（メタデータ） (2026-02-23T11:42:56Z) - 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) - Trustworthy Formal Natural Language Specifications [3.8073142980733]
本稿では、自然言語の表現的サブセットで書かれた仕様を構築できることを示す。
モジュール的に形式化された英語のサブセットで仕様を提供する手段を実装し、それらを形式的なクレームに自動的に変換する。
我々は,各単語の解釈方法と文の構造を用いて意味を計算したことを示す証明証明書を作成した。
論文 参考訳（メタデータ） (2023-10-05T20:41:47Z) - nl2spec: Interactively Translating Unstructured Natural Language to
Temporal Logics with Large Language Models [3.1143846686797314]
大規模言語モデル(LLM)を適用するためのフレームワークであるnl2specは、構造化されていない自然言語から正式な仕様を導出する。
本稿では,自然言語におけるシステム要求のあいまいさを検知し,解決する新たな手法を提案する。
ユーザは、これらのサブ翻訳を反復的に追加、削除、編集して、不正なフォーマル化を修正する。
論文 参考訳（メタデータ） (2023-03-08T20:08:53Z) - Detecting Text Formality: A Study of Text Classification Approaches [78.11745751651708]
本研究は,統計的,ニューラルベース,トランスフォーマーベースの機械学習手法に基づく形式性検出手法の体系的研究を初めて行う。
単言語,多言語,言語横断の3種類の実験を行った。
本研究は,モノリンガルおよび多言語形式分類タスクのためのトランスフォーマーベースモデルに対するChar BiLSTMモデルの克服を示す。
論文 参考訳（メタデータ） (2022-04-19T16:23:07Z) - Learning Symbolic Rules for Reasoning in Quasi-Natural Language [74.96601852906328]
我々は,ルールを手作業で構築することなく,自然言語入力で推論できるルールベースシステムを構築した。
本稿では,形式論理文と自然言語文の両方を表現可能な"Quasi-Natural"言語であるMetaQNLを提案する。
提案手法は,複数の推論ベンチマークにおける最先端の精度を実現する。
論文 参考訳（メタデータ） (2021-11-23T17:49:00Z) - From English to Signal Temporal Logic [7.6398837478968025]
本稿では,サイバー物理システムのための公式な仕様言語であるSignal Temporal Logic (STL) に,自由英語文として与えられる非公式な要件を翻訳するためのツールおよびテクニックであるDeepSTLを提案する。
このような翻訳を考案する上での大きな課題は、公式な非公式な要件と公式な仕様の欠如である。
2番目のステップでは、最先端のトランスフォーマーベースのニューラル翻訳技術を用いて、英語からSTLへの正確な注意翻訳を訓練する。
論文 参考訳（メタデータ） (2021-09-21T16:13:29Z) - A Matter of Framing: The Impact of Linguistic Formalism on Probing
Results [69.36678873492373]
BERT (Delvin et al.) のような事前訓練されたコンテキスト化エンコーダは、下流タスクで顕著なパフォーマンスを示す。
調査における最近の研究は、事前学習中にこれらのモデルによって暗黙的に学習された言語知識について調査している。
形式主義の選択は調査結果に影響を及ぼすか?
BERTによる意味的役割情報とプロトロール情報のエンコーディングにおける言語学的意義の相違は,形式主義に依存している。
論文 参考訳（メタデータ） (2020-04-30T17:45:16Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。