論文の概要: Automated Formalization of Probabilistic Requirements from Structured Natural Language

• arxiv url: http://arxiv.org/abs/2512.15788v1
• Date: Mon, 15 Dec 2025 20:20:27 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-19 18:10:31.713844
• Title: Automated Formalization of Probabilistic Requirements from Structured Natural Language
• Title（参考訳）: 構造化自然言語からの確率的要求の自動形式化
• Authors: Anastasia Mavridou, Marie Farrell, Gricel Vázquez, Tom Pressburger, Timothy E. Wang, Radu Calinescu, Michael Fisher,
• Abstract要約: 我々は、NASAの形式的要求緩和ツール(FRET)を拡張し、曖昧で正確な確率的要求の仕様をサポートする。 本稿では,構造化された自然言語要求を確率論的時間論理式に翻訳するための形式的,構成的,自動的なアプローチを提案し,開発する。
• 参考スコア（独自算出の注目度）: 2.8065951726067726
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Integrating autonomous and adaptive behavior into software-intensive systems presents significant challenges for software development, as uncertainties in the environment or decision-making processes must be explicitly captured. These challenges are amplified in safety- and mission-critical systems, which must undergo rigorous scrutiny during design and development. Key among these challenges is the difficulty of specifying requirements that use probabilistic constructs to capture the uncertainty affecting these systems. To enable formal analysis, such requirements must be expressed in precise mathematical notations such as probabilistic logics. However, expecting developers to write requirements directly in complex formalisms is unrealistic and highly error-prone. We extend the structured natural language used by NASA's Formal Requirement Elicitation Tool (FRET) with support for the specification of unambiguous and correct probabilistic requirements, and develop an automated approach for translating these requirements into logical formulas. We propose and develop a formal, compositional, and automated approach for translating structured natural-language requirements into formulas in probabilistic temporal logic. To increase trust in our formalizations, we provide assurance that the generated formulas are well-formed and conform to the intended semantics through an automated validation framework and a formal proof. The extended FRET tool enables developers to specify probabilistic requirements in structured natural language, and to automatically translate them into probabilistic temporal logic, making the formal analysis of autonomous and adaptive systems more practical and less error-prone.
• Abstract（参考訳）: 自律的かつ適応的な振る舞いをソフトウェア集約システムに統合することは、環境や意思決定プロセスにおける不確実性を明確に把握しなければならないため、ソフトウェア開発にとって大きな課題となる。 これらの課題は、安全とミッションクリティカルなシステムにおいて増幅され、設計と開発の間に厳格な精査を受けなければならない。 これらの課題の鍵となるのは、確率的構造を用いてシステムに影響を及ぼす不確実性を捉える要求を特定することの難しさである。 形式解析を可能にするためには、そのような要件は確率論理のような正確な数学的表記法で表さなければならない。 しかし、開発者が複雑な形式で要求を直接記述することを期待するのは非現実的であり、非常にエラーを起こしやすい。 我々は,NASAの形式的要件抽出ツール(FRET)が使用する構造化自然言語を拡張し,不明瞭で正確な確率的要件の仕様の策定を支援するとともに,これらの要件を論理式に変換するための自動アプローチを開発する。 本稿では,構造化された自然言語要求を確率論的時間論理式に翻訳するための形式的,構成的,自動的なアプローチを提案し,開発する。 形式化の信頼性を高めるため、自動検証フレームワークと形式証明により、生成した公式が適切に形成され、意図した意味に適合することを保証します。 この拡張FRETツールは、開発者は構造化された自然言語の確率的要件を指定でき、それらを確率的時間論理に自動的に変換することで、自律的および適応的なシステムの形式的分析をより実用的でエラーの少ないものにすることができる。

関連論文リスト

• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
  本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。 これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。 実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
  論文  参考訳（メタデータ） (2025-10-28T16:22:54Z)
• 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)
• Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects [0.0]
  VERIFAI1は、このギャップを埋めるための自動化および半自動化アプローチを調査することを目的としている。 本論文では, 課題の繰り返しと今後の研究方向性を明らかにするために, 関連文献の予備的な合成について述べる。
  論文  参考訳（メタデータ） (2025-07-18T19:15:50Z)
• Foundation Models for Logistics: Toward Certifiable, Conversational Planning Interfaces [59.80143393787701]
  大規模言語モデル(LLM)は不確実性に対処し、導入障壁を低くしながら再計画の加速を約束する。 本稿では,自然言語対話のアクセシビリティと目標解釈の検証可能な保証とを組み合わせたニューロシンボリック・フレームワークを提案する。 わずか100個の不確実性フィルタで微調整された軽量モデルは、GPT-4.1のゼロショット性能を上回り、推論遅延を50%近く削減する。
  論文  参考訳（メタデータ） (2025-07-15T14:24:01Z)
• Un marco conceptual para la generación de requerimientos de software de calidad [0.0]
  自然言語処理タスクを強化するために,大規模言語モデル (LLM) が登場した。 この研究は、これらのモデルを使用して自然言語で書かれたソフトウェア要件の品質を改善することを目的としている。
  論文  参考訳（メタデータ） (2025-04-14T19:12:18Z)
• Technical Report on Neural Language Models and Few-Shot Learning for Systematic Requirements Processing in MDSE [1.6286277560322266]
  本論文は,自動車要件のオープンソースセットの分析に基づくものである。 ドメイン固有の言語構造を導き、要求の不明瞭さを回避し、形式性のレベルを上げるのに役立ちます。
  論文  参考訳（メタデータ） (2022-11-16T18:06:25Z)
• Multi-Agent Reinforcement Learning with Temporal Logic Specifications [65.79056365594654]
  本研究では,時間論理仕様を満たすための学習課題を,未知の環境下でエージェントのグループで検討する。 我々は、時間論理仕様のための最初のマルチエージェント強化学習手法を開発した。 主アルゴリズムの正確性と収束性を保証する。
  論文  参考訳（メタデータ） (2021-02-01T01:13:03Z)

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

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