論文の概要: Towards an Agentic LLM-based Approach to Requirement Formalization from Unstructured Specifications
- arxiv url: http://arxiv.org/abs/2604.18228v1
- Date: Mon, 20 Apr 2026 13:12:04 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-21 21:52:52.889063
- Title: Towards an Agentic LLM-based Approach to Requirement Formalization from Unstructured Specifications
- Title（参考訳）: エージェントLCMによる非構造仕様からの要求形式化へのアプローチ
- Authors: Alberto Tagliaferro, Bruno Guindani, Livia Lestingi, Matteo Rossi,
- Abstract要約: 本稿では,非構造化仕様から検証可能なプロパティを自動的に抽出するエージェント手法を提案する。
パイプラインは77.8%の精度で構文的および意味論的に整列された形式特性を生成する。
- 参考スコア（独自算出の注目度）: 1.0071849243353403
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Early-stage specifications of safety-critical systems are typically expressed in natural language, making it difficult to derive formal properties suitable for verification and needed to guarantee safety. While recent Large Language Model (LLM)-based approaches can generate formal artifacts from text, they mainly focus on syntactic correctness and do not ensure semantic alignment between informal requirements and formally verifiable properties. We propose an agentic methodology that automatically extracts verification-ready properties from unstructured specifications. The modular pipeline combines requirement extraction, compatibility filtering with respect to a target formalism, and translation into formal properties. Experimental results across three scenarios show that the pipeline generates syntactically and semantically aligned formal properties with a 77.8% accuracy. By explicitly accounting for modeling and verification constraints, the approach is a paving step towards exploiting Artificial Intelligence (AI) to bridge the gap between informal descriptions and semantically meaningful formal verification.
- Abstract（参考訳）: 安全クリティカルシステムの初期段階の仕様は、一般的に自然言語で表現されるため、検証に適した形式的特性を導き出すことが困難であり、安全性を保証する必要がある。
最近のLarge Language Model(LLM)ベースのアプローチはテキストから形式的アーティファクトを生成することができるが、それらは主に構文的正しさに焦点を当てており、非公式な要件と形式的検証可能なプロパティ間のセマンティックアライメントを保証しない。
本稿では,非構造化仕様から検証可能なプロパティを自動的に抽出するエージェント手法を提案する。
モジュールパイプラインは、要求抽出、ターゲット形式に関する互換性フィルタリング、形式的特性への変換を組み合わせたものである。
3つのシナリオにわたる実験結果は、パイプラインが77.8%の精度で構文的および意味的に整合した形式特性を生成することを示している。
モデリングと検証の制約を明示的に説明することにより、非公式な記述と意味論的に意味のある形式的検証の間のギャップを埋めるために人工知能(AI)を活用するための一歩となる。
関連論文リスト
- Understanding Contextual Recall in Transformers: How Finetuning Enables In-Context Reasoning over Pretraining Knowledge [50.009682083079205]
我々は,文脈的リコールが単独で事前学習から生じるかどうかを検討する。
ICL評価とは異なる暗黙的推論を必要とするタスクの微調整は、文脈的リコールの出現を誘発することを示す。
メカニカル・インサイト(メカニカル・インサイト)では,現実から文脈への遷移を再現するアテンションオンリー・トランスフォーマーの構成を導出する。
論文 参考訳（メタデータ） (2026-03-21T22:46:55Z) - Formal Evidence Generation for Assurance Cases for Robotic Software Models [1.8145248907978841]
保証ケースは、証拠によって支持される構造化された議論を提供する。
この証拠の生成と維持は、労働集約的で、エラーを起こし、システムが進化するにつれて一貫性を維持するのが困難である。
本稿では,保証ワークフローに形式検証を組み込むことにより,AC証拠を体系的に生成するモデルに基づく手法を提案する。
論文 参考訳（メタデータ） (2026-02-03T14:01:30Z) - Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification [49.506412445511934]
大きな言語モデル(LLM)は目覚ましい能力を示すが、その次は論理的不整合と報奨ハックを生み出す。
本稿では,自然言語生成プロセスと形式的記号的検証を動的にインターリーブする形式論理検証誘導フレームワークを提案する。
我々はこのフレームワークを,形式論理検証誘導制御による微調整とポリシー最適化の相乗効果を生かした,新しい2段階のトレーニングパイプラインを通じて運用する。
論文 参考訳（メタデータ） (2026-01-30T07:01:25Z) - Structured Decomposition for LLM Reasoning: Cross-Domain Validation and Semantic Web Integration [0.0]
ルールベースの推論は、決定が監査可能で正当化可能な領域で発生します。
このような入力にルールを適用するには、解釈の柔軟性と形式的な保証の両方が必要である。
本稿では,これらの強みを組み合わせた統合パターンを提案する。
論文 参考訳（メタデータ） (2026-01-04T17:19:20Z) - ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。
これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。
実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
論文 参考訳（メタデータ） (2025-10-28T16:22:54Z) - Autoformalizer with Tool Feedback [52.334957386319864]
自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。
既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。
本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
論文 参考訳（メタデータ） (2025-10-08T10:25:12Z) - PAT-Agent: Autoformalization for Model Checking [17.082027022913998]
PAT-Agentは自然言語の自動形式化と形式モデル修復のためのエンドツーエンドフレームワークである。
これは、大きな言語モデルの生成能力と形式的検証の厳密さを組み合わせたものである。
論文 参考訳（メタデータ） (2025-09-28T06:32:14Z) - Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects [0.0]
VERIFAI1は、このギャップを埋めるための自動化および半自動化アプローチを調査することを目的としている。
本論文では, 課題の繰り返しと今後の研究方向性を明らかにするために, 関連文献の予備的な合成について述べる。
論文 参考訳（メタデータ） (2025-07-18T19:15:50Z) - Measuring Association Between Labels and Free-Text Rationales [60.58672852655487]
解釈可能なNLPでは、説明された例に対するモデルの意思決定プロセスを反映した忠実な理性が必要です。
情報抽出型タスクに対する忠実な抽出合理化のための既存のモデルであるパイプラインは、自由テキスト合理化を必要とするタスクに確実に拡張されないことを示す。
我々は、信頼が確立されていない自由文合理化のための、広く使われている高性能モデルのクラスである、共同予測と合理化のモデルに目を向ける。
論文 参考訳（メタデータ） (2020-10-24T03:40:56Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。