論文の概要: GinSign: Grounding Natural Language Into System Signatures for Temporal Logic Translation

• arxiv url: http://arxiv.org/abs/2512.16770v1
• Date: Thu, 18 Dec 2025 17:03:07 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-19 18:10:32.172035
• Title: GinSign: Grounding Natural Language Into System Signatures for Temporal Logic Translation
• Title（参考訳）: GinSign: 時相論理翻訳のための自然言語をシステムシグナチャに接地する
• Authors: William English, Chase Walker, Dominic Simon, Rickard Ewetz,
• Abstract要約: 自然言語(NL)から時間論理(TL)への変換により、エンジニアは、手動で正式な仕様を作成することなく、システムの振る舞いを特定し、検証し、強制することができる。 本稿では,GinSign と呼ばれる時相論理翻訳のための自然言語入力システムシグナチャの枠組みを提案する。
• 参考スコア（独自算出の注目度）: 9.213992122471645
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Natural language (NL) to temporal logic (TL) translation enables engineers to specify, verify, and enforce system behaviors without manually crafting formal specifications-an essential capability for building trustworthy autonomous systems. While existing NL-to-TL translation frameworks have demonstrated encouraging initial results, these systems either explicitly assume access to accurate atom grounding or suffer from low grounded translation accuracy. In this paper, we propose a framework for Grounding Natural Language Into System Signatures for Temporal Logic translation called GinSign. The framework introduces a grounding model that learns the abstract task of mapping NL spans onto a given system signature: given a lifted NL specification and a system signature $\mathcal{S}$, the classifier must assign each lifted atomic proposition to an element of the set of signature-defined atoms $\mathcal{P}$. We decompose the grounding task hierarchically- first predicting predicate labels, then selecting the appropriately typed constant arguments. Decomposing this task from a free-form generation problem into a structured classification problem permits the use of smaller masked language models and eliminates the reliance on expensive LLMs. Experiments across multiple domains show that frameworks which omit grounding tend to produce syntactically correct lifted LTL that is semantically nonequivalent to grounded target expressions, whereas our framework supports downstream model checking and achieves grounded logical-equivalence scores of $95.5\%$, a $1.4\times$ improvement over SOTA.
• Abstract（参考訳）: 自然言語(NL)から時間論理(TL)への変換により、エンジニアは、正式な仕様を手作業で作成することなく、システムの振る舞いを特定し、検証し、強制することができる。 既存のNL-to-TL翻訳フレームワークは、初期結果の促進を実証しているが、これらのシステムは、正確な原子基底へのアクセスを明示的に仮定するか、低い基底翻訳精度に苦しむかのいずれかである。 本稿では,GinSignと呼ばれる時相論理翻訳のための自然言語入力システムシグナチャの枠組みを提案する。 このフレームワークは、与えられたシステムシグネチャにNLをマッピングする抽象的なタスクを学習するグラウンディングモデルを導入する: 持ち上げられたNL仕様とシステムシグネチャが与えられた場合、分類器は、各持ち上げられた原子命題をシグネチャ定義された原子の集合の要素に割り当てなければならない。 基底タスクを階層的に分解し、まず述語ラベルを予測し、次に適切な型付けされた定数引数を選択する。 このタスクを自由形式生成問題から構造化分類問題に分解することで、より小さなマスキング言語モデルの使用が可能になり、高価なLCMへの依存を排除できる。 複数のドメインをまたいだ実験では、グラウンド化を省略するフレームワークは、グラウンド化されたターゲット表現と意味的に等価でない、構文的に正しいリフト付きTLLを生成する傾向を示し、一方、我々のフレームワークはダウンストリームモデルチェックをサポートし、グラウンド化された論理等価スコアである9.5\%$、SOTAよりも1.4\times$改善を達成している。

関連論文リスト

• Connecting the Dots: Training-Free Visual Grounding via Agentic Reasoning [63.109585527799005]
  GroundingAgentは、タスク固有の微調整なしで動作するビジュアルグラウンドティングフレームワークである。 広く使用されているベンチマークでは、平均ゼロショットグラウンドの精度は65.1%である。 また、強い解釈可能性を提供し、各推論ステップを透過的に照らす。
  論文  参考訳（メタデータ） (2025-11-24T03:11:08Z)
• Integrating Symbolic Natural Language Understanding and Language Models for Word Sense Disambiguation [0.7967000209136494]
  本稿では,統計的言語モデルを用いて曖昧さを解消する手法を提案する。 記号的NLUシステムによって生成される複数の候補意味は、区別可能な自然言語代替語に変換される。 本手法の有効性を実証するため,本手法の評価を行った。
  論文  参考訳（メタデータ） (2025-11-20T17:32:15Z)
• Verifiable Natural Language to Linear Temporal Logic Translation: A Benchmark Dataset and Evaluation Suite [8.325455397285873]
  時相論理(TL)翻訳システムに対する最先端自然言語(NL)の実証評価は,既存のベンチマークにおいてほぼ完全な性能を示す。 本稿では,自動NL-to-LTL翻訳の検証と妥当性を評価する統一ベンチマークであるVerifiable Linear Temporal Logic Benchmark (VLTL-Bench)を紹介する。
  論文  参考訳（メタデータ） (2025-07-01T15:41:57Z)
• Robust Hypothesis Generation: LLM-Automated Language Bias for Inductive Logic Programming [3.641087660577424]
  大規模言語モデル(LLM)とインダクティブ論理プログラミング(ILP)を組み合わせたマルチエージェントシステムを統合する新しいフレームワークを提案する。 我々のLLMエージェントは、構造化されたシンボル語彙(述語)と関係テンプレートを自律的に定義する。 多様な、挑戦的なシナリオの実験は、優れたパフォーマンスを検証し、自動化され、説明可能で、検証可能な仮説生成のための新しいパスを舗装する。
  論文  参考訳（メタデータ） (2025-05-27T17:53:38Z)
• $\texttt{SEM-CTRL}$: Semantically Controlled Decoding [53.86639808659575]
  $texttSEM-CTRL$は、LLMデコーダに直接、リッチなコンテキスト依存制約とタスクおよびインスタンス固有のセマンティクスを強制する統一的なアプローチである。 texttSEM-CTRL$は、小さな訓練済みのLLMがより大きな変種や最先端の推論モデルよりも効率的に性能を向上することを可能にする。
  論文  参考訳（メタデータ） (2025-03-03T18:33:46Z)
• Physics of Language Models: Part 1, Learning Hierarchical Language Structures [51.68385617116854]
  トランスフォーマーベースの言語モデルは効率的だが複雑であり、内部の動作や推論メカニズムを理解することは大きな課題である。 本稿では,長文を生成可能な階層規則を生成する合成CFGのファミリーを紹介する。 我々は、GPTのような生成モデルがCFG定義階層を正確に学習し、推論し、それに基づいて文を生成することを実証する。
  論文  参考訳（メタデータ） (2023-05-23T04:28:16Z)
• nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models [3.1143846686797314]
  大規模言語モデル(LLM)を適用するためのフレームワークであるnl2specは、構造化されていない自然言語から正式な仕様を導出する。 本稿では,自然言語におけるシステム要求のあいまいさを検知し,解決する新たな手法を提案する。 ユーザは、これらのサブ翻訳を反復的に追加、削除、編集して、不正なフォーマル化を修正する。
  論文  参考訳（メタデータ） (2023-03-08T20:08:53Z)
• Infusing Finetuning with Semantic Dependencies [62.37697048781823]
  シンタックスとは異なり、セマンティクスは今日の事前訓練モデルによって表面化されないことを示す。 次に、畳み込みグラフエンコーダを使用して、タスク固有の微調整にセマンティック解析を明示的に組み込む。
  論文  参考訳（メタデータ） (2020-12-10T01:27:24Z)

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

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