論文の概要: LTLGuard: Formalizing LTL Specifications with Compact Language Models and Lightweight Symbolic Reasoning
- arxiv url: http://arxiv.org/abs/2603.05728v1
- Date: Thu, 05 Mar 2026 22:34:45 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-03-09 13:17:44.678401
- Title: LTLGuard: Formalizing LTL Specifications with Compact Language Models and Lightweight Symbolic Reasoning
- Title（参考訳）: LTLGuard: コンパクト言語モデルと軽量シンボリック推論によるLTL仕様の形式化
- Authors: Medina Andresel, Cristinel Mateis, Dejan Nickovic, Spyridon Kounoupidis, Panagiotis Katsaros, Stavros Tripakis,
- Abstract要約: 自然言語のあいまいさと可変性(NL)のため、非公式な要件を形式的な仕様に翻訳することは困難である
本研究では,資源効率の高いオープンウェイトモデルにより,非公式な要件から適切な時間論理(LTL)仕様を生成することに焦点を当てる。
現在Guardは、制約付き生成とフォーマルな一貫性チェックを組み合わせたモジュラーツールチェーンで、非公式な入力からコンフリクトフリー仕様を生成する。
- 参考スコア（独自算出の注目度）: 2.365021420497964
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Translating informal requirements into formal specifications is challenging due to the ambiguity and variability of natural language (NL). This challenge is particularly pronounced when relying on compact (small and medium) language models, which may lack robust knowledge of temporal logic and thus struggle to produce syntactically valid and consistent formal specifications. In this work, we focus on enabling resource-efficient open-weight models (4B--14B parameters) to generate correct linear temporal logic (LTL) specifications from informal requirements. We present LTLGuard, a modular toolchain that combines constrained generation with formal consistency checking to generate conflict-free LTL specifications from informal input. Our method integrates the generative capabilities of model languages with lightweight automated reasoning tools to iteratively refine candidate specifications, understand the origin of the conflicts and thus help in eliminating inconsistencies. We demonstrate the usability and the effectiveness of our approach and perform quantitative evaluation of the resulting framework.
- Abstract（参考訳）: 非公式な要件を形式的な仕様に翻訳することは、自然言語(NL)の曖昧さと可変性のために困難である。
この課題は、時相論理の堅牢な知識が欠けているため、構文的に有効で一貫性のある形式仕様を作成するのに苦労する、コンパクトな(中小の)言語モデルに依存するときに特に顕著である。
本研究では,資源効率の高いオープンウェイトモデル(4B-14Bパラメータ)を,非公式な要件から正しい線形時間論理(LTL)仕様を生成することに注力する。
本稿では、制約付き生成と形式整合性チェックを組み合わせたモジュラーツールチェーンであるLTLGuardを紹介し、非公式な入力からコンフリクトフリーなTLL仕様を生成する。
提案手法は,モデル言語の生成能力と軽量自動推論ツールを統合し,候補仕様を反復的に洗練し,矛盾の原因を理解し,矛盾の解消に役立てる。
提案手法のユーザビリティと有効性を実証し,得られたフレームワークの定量的評価を行う。
関連論文リスト
- 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) - Autoformalizer with Tool Feedback [52.334957386319864]
自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。
既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。
本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
論文 参考訳（メタデータ） (2025-10-08T10:25:12Z) - Data Dependency-Aware Code Generation from Enhanced UML Sequence Diagrams [54.528185120850274]
本稿では,API2Depという新しいステップバイステップコード生成フレームワークを提案する。
まず、サービス指向アーキテクチャに適した拡張Unified Modeling Language (UML) APIダイアグラムを紹介します。
次に、データフローの重要な役割を認識し、専用のデータ依存推論タスクを導入する。
論文 参考訳（メタデータ） (2025-08-05T12:28:23Z) - Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。
有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。
生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
論文 参考訳（メタデータ） (2025-07-22T08:13:01Z) - Self-Steering Language Models [113.96916935955842]
DisCIPL は "self-steering" 言語モデル (LM) の手法である。
DisCIPLは、Followerモデルの集団によって実行されるタスク固有の推論プログラムを生成する。
我々の研究は、高度に並列化されたモンテカルロ推論戦略の設計空間を開く。
論文 参考訳（メタデータ） (2025-04-09T17:54:22Z) - Attribute Controlled Fine-tuning for Large Language Models: A Case Study on Detoxification [76.14641982122696]
本稿では,属性制御付き大規模言語モデル(LLM)の制約学習スキーマを提案する。
提案手法は, ベンチマーク上での競合性能と毒性検出タスクを達成しながら, 不適切な応答を少ないLCMに導出することを示す。
論文 参考訳（メタデータ） (2024-10-07T23:38:58Z) - Boosting the Capabilities of Compact Models in Low-Data Contexts with Large Language Models and Retrieval-Augmented Generation [2.9921619703037274]
本稿では,形態素解析の言語タスクにおいて,より小さなモデルの出力を補正するために,大言語モデル(LLM)を基盤とした検索拡張生成(RAG)フレームワークを提案する。
データ不足や訓練可能なパラメータの不足を補うために,言語情報を活用するとともに,LLMを通して解釈・蒸留された記述文法からの入力を許容する。
コンパクトなRAG支援モデルがデータスカース設定に極めて有効であることを示し、このタスクとターゲット言語に対する新しい最先端技術を実現する。
論文 参考訳（メタデータ） (2024-10-01T04:20:14Z) - Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving [13.485604499678262]
本稿では,Large Language Models(LLMs)とTheorem Provers(TPs)の統合による自然言語説明の検証と改善について検討する。
本稿では, TPとLPMを統合して説明文の生成と定式化を行う, Explanation-Refiner というニューロシンボリック・フレームワークを提案する。
代わりに、TPは説明の論理的妥当性を公式に保証し、その後の改善のためのフィードバックを生成するために使用される。
論文 参考訳（メタデータ） (2024-05-02T15:20:01Z) - Decomposing Uncertainty for Large Language Models through Input Clarification Ensembling [69.83976050879318]
大規模言語モデル(LLM)では、不確実性の原因を特定することが、信頼性、信頼性、解釈可能性を改善するための重要なステップである。
本稿では,LLMのための不確実性分解フレームワークについて述べる。
提案手法は,入力に対する一連の明確化を生成し,それらをLLMに入力し,対応する予測をアンサンブルする。
論文 参考訳（メタデータ） (2023-11-15T05:58:35Z) - nl2spec: Interactively Translating Unstructured Natural Language to
Temporal Logics with Large Language Models [3.1143846686797314]
大規模言語モデル(LLM)を適用するためのフレームワークであるnl2specは、構造化されていない自然言語から正式な仕様を導出する。
本稿では,自然言語におけるシステム要求のあいまいさを検知し,解決する新たな手法を提案する。
ユーザは、これらのサブ翻訳を反復的に追加、削除、編集して、不正なフォーマル化を修正する。
論文 参考訳（メタデータ） (2023-03-08T20:08:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。