論文の概要: Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects

• arxiv url: http://arxiv.org/abs/2507.14330v1
• Date: Fri, 18 Jul 2025 19:15:50 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-07-22 20:51:31.842428
• Title: Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects
• Title（参考訳）: フォーマルなソフトウェア要件のためのLLMの活用 -- 課題と展望
• Authors: Arshad Beg, Diarmuid O'Donoghue, Rosemary Monahan,
• Abstract要約: VERIFAI1は、このギャップを埋めるための自動化および半自動化アプローチを調査することを目的としている。 本論文では, 課題の繰り返しと今後の研究方向性を明らかにするために, 関連文献の予備的な合成について述べる。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Software correctness is ensured mathematically through formal verification, which involves the resources of generating formal requirement specifications and having an implementation that must be verified. Tools such as model-checkers and theorem provers ensure software correctness by verifying the implementation against the specification. Formal methods deployment is regularly enforced in the development of safety-critical systems e.g. aerospace, medical devices and autonomous systems. Generating these specifications from informal and ambiguous natural language requirements remains the key challenge. Our project, VERIFAI^{1}, aims to investigate automated and semi-automated approaches to bridge this gap, using techniques from Natural Language Processing (NLP), ontology-based domain modelling, artefact reuse, and large language models (LLMs). This position paper presents a preliminary synthesis of relevant literature to identify recurring challenges and prospective research directions in the generation of verifiable specifications from informal requirements.
• Abstract（参考訳）: ソフトウェア正当性は形式的検証によって数学的に保証され、形式的な要件仕様を生成し、検証しなければならない実装を持つリソースを含む。 モデルチェッカーや定理証明器のようなツールは、仕様に対する実装を検証することによって、ソフトウェアの正当性を保証する。 フォーマルな方法の展開は、航空宇宙、医療機器、自律システムといった安全クリティカルなシステムの開発において、定期的に実施されている。 これらの仕様を非公式かつ曖昧な自然言語要求から生成することは、依然として重要な課題である。 本研究は,自然言語処理(NLP),オントロジーに基づくドメインモデリング,アーティファクト再利用,大規模言語モデル(LLM)といった手法を用いて,このギャップを埋めるための自動的および半自動的アプローチを検討することを目的とする。 本論文では, 非公式な要件から検証可能な仕様の生成において, 繰り返し発生する課題と今後の研究方向性を特定するために, 関連文献の予備的な合成を行う。

関連論文リスト

• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [68.00108157244952]
  強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。 有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。 生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
  論文  参考訳（メタデータ） (2025-07-22T08:13:01Z)
• Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs [84.30534714651093]
  本稿では,検証を意識したプログラミング言語であるDafnyに対して,革新的なAPRツールを提案する。 プログラム内の各ステートメントの状態を決定するために、Hoare Logicの使用を含む一連のステップを通じて、障害をローカライズします。 実世界のDafnyプログラムのベンチマークであるDafnyBenchを用いて,我々のアプローチを評価する。
  論文  参考訳（メタデータ） (2025-07-04T15:36:12Z)
• Formalising Software Requirements using Large Language Models [0.0]
  プロジェクトは、形式仕様のトレーサビリティと検証における課題に対処する。 システムの実装と検証を通じて、正式な仕様の自動生成と、初期ソフトウェア設計段階からの要求のトレーサビリティをサポートする。
  論文  参考訳（メタデータ） (2025-06-12T13:55:01Z)
• Self-Steering Language Models [113.96916935955842]
  DisCIPLは、"セルフステアリング(self-steering)"言語モデルのメソッドである。 DisCIPLはPlannerモデルを使用してタスク固有の推論プログラムを生成する。 我々の研究は、高度に並列化されたモンテカルロ推論戦略の設計空間を開く。
  論文  参考訳（メタデータ） (2025-04-09T17:54:22Z)
• Search, Verify and Feedback: Towards Next Generation Post-training Paradigm of Foundation Models via Verifier Engineering [51.31836988300326]
  検証工学は、基礎モデルの時代のために特別に設計された新しいポストトレーニングパラダイムである。 検証工学のプロセスは,検索,検証,フィードバックの3段階に分類する。
  論文  参考訳（メタデータ） (2024-11-18T12:04:52Z)
• Benchmarking Uncertainty Quantification Methods for Large Language Models with LM-Polygraph [83.90988015005934]
  不確実性定量化は機械学習アプリケーションにおいて重要な要素である。 最新のUQベースラインの集合を実装した新しいベンチマークを導入する。 我々は、11タスクにわたるUQと正規化技術に関する大規模な実証的研究を行い、最も効果的なアプローチを特定した。
  論文  参考訳（メタデータ） (2024-06-21T20:06:31Z)
• Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
  AutoSpecは、自動プログラム検証のための仕様を合成するための自動化アプローチである。 仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。 実世界のX509パーサプロジェクトでプログラムを検証するためにうまく適用することができる。
  論文  参考訳（メタデータ） (2024-03-31T18:15:49Z)
• Validation of Rigorous Requirements Specifications and Document Automation with the ITLingo RSL Language [0.0]
  ITLingoイニシアチブは、技術的文書の厳密さと一貫性を高めるためにRSLという要求仕様言語を導入した。 本稿では、要求検証と文書自動化の分野における既存の研究・ツールについてレビューする。 我々は、カスタマイズされたチェックと、RSL自体で動的に定義された言語規則に基づいて、仕様の検証によりRSLを拡張することを提案する。
  論文  参考訳（メタデータ） (2023-12-17T21:39:26Z)
• Natural Language Processing for Requirements Formalization: How to Derive New Approaches? [0.32885740436059047]
  我々はNLPの分野における主要な考え方と最先端の方法論について論じる。 我々は2つの異なるアプローチを詳細に議論し、ルールセットの反復的開発を強調した。 提案手法は, 自動車分野と鉄道分野の2つの産業分野において実証された。
  論文  参考訳（メタデータ） (2023-09-23T05:45:19Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。 コントローラと証明書を形式的に合成する自動化手法を提案する。 我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
  論文  参考訳（メタデータ） (2023-09-12T09:37:26Z)
• Technical Report on Neural Language Models and Few-Shot Learning for Systematic Requirements Processing in MDSE [1.6286277560322266]
  本論文は,自動車要件のオープンソースセットの分析に基づくものである。 ドメイン固有の言語構造を導き、要求の不明瞭さを回避し、形式性のレベルを上げるのに役立ちます。
  論文  参考訳（メタデータ） (2022-11-16T18:06:25Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。 このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
  論文  参考訳（メタデータ） (2019-02-02T20:09:32Z)

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

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