論文の概要: NeuroNL2LTL: A Neurosymbolic Framework for Natural Language Translation of Linear Temporal Logic
- arxiv url: http://arxiv.org/abs/2605.22874v1
- Date: Wed, 20 May 2026 03:31:51 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-25 17:29:20.013936
- Title: NeuroNL2LTL: A Neurosymbolic Framework for Natural Language Translation of Linear Temporal Logic
- Title（参考訳）: NeuroNL2LTL : リニア時相論理の自然言語翻訳のためのニューロシンボリックフレームワーク
- Authors: Paapa Kwesi Quansah, Ernest Bonnah,
- Abstract要約: 本稿では,学習翻訳と形式的検証を一体化したニューロシンボリックアーキテクチャであるNeuroNL2LTLを提案する。
航空宇宙、ロボティクス、自動運転車、さらに10のドメインにまたがる20万以上の要件に対して、NeuroNL2LTLは基準仕様と28%のセマンティックな等価性を達成している。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Effectively translating between natural language (NL) and formal logics like Linear Temporal Logic (LTL) requires expertise that limits formal verification's reach in safety-critical development. Template-based approaches sacrifice expressiveness for reliability; neural methods achieve fluency but provide no correctness guarantees. We present NeuroNL2LTL, a neurosymbolic architecture unifying learned translation with formal verification. NeuroNL2LTL routes translation through an intermediate representation whose mapping to LTL is structure-preserving by construction. Generated specifications undergo satisfiability and non-triviality checking; a minimal-edit repair mechanism corrects near-miss outputs before they reach downstream tools. The central innovation is verifier-in-the-loop training: verification outcomes serve as reward signals for reinforcement learning, producing neural components that optimize directly for formal correctness. On 200,000+ requirements spanning aerospace, robotics, autonomous vehicles, and ten additional domains, NeuroNL2LTL achieves 28\% semantic equivalence with reference specifications while ensuring 86\% of outputs are verified satisfiable. The system also generates contextually grounded explanations from LTL, enabling domain experts to validate specifications without specialized training. This work demonstrates that formal verification can function as both training objective and runtime filter for neural specification systems, allowing us to build neural-based tools whose reliability derives from logical guarantees rather than statistical confidence.
- Abstract（参考訳）: 自然言語(NL)とLTL(Linear Temporal Logic)のような形式論理を効果的に翻訳するには、安全クリティカルな開発における形式検証の範囲を制限する専門知識が必要である。
テンプレートベースのアプローチでは、信頼性の表現性を犠牲にしている。
本稿では,学習翻訳と形式的検証を一体化したニューロシンボリックアーキテクチャであるNeuroNL2LTLを提案する。
NeuroNL2LTLは、LTLへのマッピングが構造保存されている中間表現を通して翻訳を行う。
生成した仕様は満足度と非自明性チェックを受けており、最小限の修正機構により、下流のツールに到達する前にニアミス出力を補正する。
検証結果は強化学習の報奨信号として機能し、形式的正当性を直接最適化するニューラルネットワークコンポーネントを生成する。
航空宇宙、ロボティクス、自動運転車、さらに10のドメインにまたがる20万以上の要件に対して、NeuroNL2LTLは基準仕様と28倍のセマンティックな等価性を達成し、出力の86倍が満足できることを保証している。
また、LTLからコンテキストベースによる説明を生成することで、ドメインの専門家が特別なトレーニングをすることなく仕様を検証できる。
この研究は、形式的検証がニューラルネットワーク仕様システムのトレーニング目標とランタイムフィルタの両方として機能することを示し、信頼性が統計的信頼性ではなく論理的保証から導かれるニューラルネットワークベースのツールを構築することができる。
関連論文リスト
- ReasonSTL: Bridging Natural Language and Signal Temporal Logic via Tool-Augmented Process-Rewarded Learning [5.961092142323502]
textscReasonSTLは、自然言語からSTL生成にローカルのオープンソース言語モデルを適用するツール拡張フレームワークである。
textscReasonSTLは、翻訳プロセスを明示的な推論、決定論的ツール呼び出し、構造化された公式構成に分解する。
実験により、textscReasonSTLでトレーニングされた4Bモデルは、自動測定と人的評価の両方で最先端のパフォーマンスを達成することが示された。
論文 参考訳（メタデータ） (2026-05-07T16:07:30Z) - LTLGuard: Formalizing LTL Specifications with Compact Language Models and Lightweight Symbolic Reasoning [2.365021420497964]
自然言語のあいまいさと可変性(NL)のため、非公式な要件を形式的な仕様に翻訳することは困難である
本研究では,資源効率の高いオープンウェイトモデルにより,非公式な要件から適切な時間論理(LTL)仕様を生成することに焦点を当てる。
現在Guardは、制約付き生成とフォーマルな一貫性チェックを組み合わせたモジュラーツールチェーンで、非公式な入力からコンフリクトフリー仕様を生成する。
論文 参考訳（メタデータ） (2026-03-05T22:34:45Z) - VIRO: Robust and Efficient Neuro-Symbolic Reasoning with Verification for Referring Expression Comprehension [51.76841625486355]
Referring Expression (REC) は、自然言語クエリに対応する画像領域をローカライズすることを目的としている。
最近のニューロシンボリックRECアプローチは、大規模言語モデル(LLM)と視覚言語モデル(VLM)を利用して構成推論を行う。
推論ステップ内に軽量な演算子レベルの検証器を組み込む,ニューロシンボリックなフレームワークであるVIROを紹介する。
論文 参考訳（メタデータ） (2026-01-19T07:21:19Z) - Training LLMs with LogicReward for Faithful and Rigorous Reasoning [75.30425553246177]
定理証明器を用いてステップレベルの論理的正しさを強制することでモデルトレーニングを指導する報酬システムであるLogicRewardを提案する。
LogicRewardで構築されたデータに基づいてトレーニングされた8Bモデルは、GPT-4oとo4-miniを11.6%、自然言語推論と論理的推論タスクで2%超えた。
論文 参考訳（メタデータ） (2025-12-20T03:43:02Z) - Bridging Natural Language and Formal Specification--Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs [10.958536923155101]
Req2LTLは、NLとLinear Temporal Logicをブリッジするモジュラーフレームワークである。
実世界の航空要求に対して88.4%のセマンティック精度と100%の構文的正確性を達成する。
論文 参考訳（メタデータ） (2025-12-19T08:25:54Z) - ProSLM : A Prolog Synergized Language Model for explainable Domain Specific Knowledge Based Question Answering [0.0]
ニューロシンボリックアプローチは説明可能なシンボル表現を取り入れることで、不透明な神経系に堅牢性を加えることができる。
本稿では,大規模言語モデルの堅牢性と信頼性を向上させるために,ニューロシンボリックな新しいフレームワークであるシステム名を提案する。
我々の研究は、ニューロシンボリックな生成AIテキスト検証とユーザパーソナライゼーションの新しい領域を開く。
論文 参考訳（メタデータ） (2024-09-17T22:34:33Z) - Neuro-Symbolic Inductive Logic Programming with Logical Neural Networks [65.23508422635862]
我々は最近提案された論理ニューラルネットワーク(LNN)を用いた学習規則を提案する。
他のものと比較して、LNNは古典的なブール論理と強く結びついている。
標準ベンチマークタスクの実験では、LNNルールが極めて解釈可能であることを確認した。
論文 参考訳（メタデータ） (2021-12-06T19:38:30Z) - FF-NSL: Feed-Forward Neural-Symbolic Learner [70.978007919101]
本稿では,Feed-Forward Neural-Symbolic Learner (FF-NSL) と呼ばれるニューラルシンボリック学習フレームワークを紹介する。
FF-NSLは、ラベル付き非構造化データから解釈可能な仮説を学習するために、Answer Setセマンティクスに基づく最先端のICPシステムとニューラルネットワークを統合する。
論文 参考訳（メタデータ） (2021-06-24T15:38:34Z) - NSL: Hybrid Interpretable Learning From Noisy Raw Data [66.15862011405882]
本稿では,ラベル付き非構造データから解釈可能なルールを学習するニューラルシンボリック学習フレームワークNSLを提案する。
NSLは、機能抽出のためのトレーニング済みニューラルネットワークと、解集合セマンティクスに基づくルール学習のための最先端のILPシステムであるFastLASを組み合わせる。
NSLは、MNISTデータから堅牢なルールを学び、ニューラルネットワークやランダムフォレストベースラインと比較して、比較または優れた精度を達成できることを実証します。
論文 参考訳（メタデータ） (2020-12-09T13:02:44Z) - Logical Natural Language Generation from Open-Domain Tables [107.04385677577862]
本稿では,その事実に関連付けられた自然言語文をモデルで生成するタスクを提案する。
提案した論理的 NLG 問題の研究を容易にするために,幅広い論理的・記号的推論を特徴とする既存の TabFact データセットcitechen 2019tabfact を用いる。
新しいタスクは、シーケンス順序と論理順序のミスマッチのため、既存のモノトニック生成フレームワークに課題をもたらす。
論文 参考訳（メタデータ） (2020-04-22T06:03:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。