論文の概要: Enhancing Formal Software Specification with Artificial Intelligence

• arxiv url: http://arxiv.org/abs/2601.09745v1
• Date: Sun, 11 Jan 2026 13:53:22 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-01-16 19:43:18.830421
• Title: Enhancing Formal Software Specification with Artificial Intelligence
• Title（参考訳）: 人工知能による形式的ソフトウェア仕様の強化
• Authors: Antonio Abu Nassar, Eitan Farchi,
• Abstract要約: 形式的ソフトウェア仕様は、早期エラー検出と明示的な不変性を可能にすることが知られている。 表記のオーバーヘッドが高く、伝統的な形式言語を使うのに必要な専門知識があるため、工業的採用が限られている。 近年の人工知能の進歩は、これらのコストを大幅に削減しつつ、形式仕様の利点の多くを維持することができる。
• 参考スコア（独自算出の注目度）: 1.4217721366366873
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal software specification is known to enable early error detection and explicit invariants, yet it has seen limited industrial adoption due to its high notation overhead and the expertise required to use traditional formal languages. This paper presents a case study showing that recent advances in artificial intelligence make it possible to retain many of the benefits of formal specification while substantially reducing these costs. The necessity of a clear distinction between what is controlled by the system analyst and can highly benefits from the rigor of formal specification and what need not be controlled is demonstrated. We use natural language augmented with lightweight mathematical notation and written in \LaTeX\ as an intermediate specification language, which is reviewed and refined by AI prior to code generation. Applied to a nontrivial simulation of organizational knowledge growth, this approach enables early validation, explicit invariants, and correctness by design, while significantly reducing development effort and producing a correct implementation on the first attempt.
• Abstract（参考訳）: 形式的ソフトウェア仕様は、早期のエラー検出と明示的な不変性を可能にすることが知られているが、表記のオーバーヘッドの高さと従来の形式言語の使用に必要な専門知識のために、工業的採用は限られている。 本稿では,近年の人工知能の進歩が,これらのコストを大幅に削減しつつ,形式仕様の利点の多くを維持できることを示すケーススタディを提案する。 システムアナリストが制御するものと、正式な仕様の厳密さと制御する必要のないものとの明確な区別の必要性を実証する。 我々は、軽量な数学的表記法で拡張された自然言語を中間仕様言語として記述し、コード生成の前にAIによってレビューされ、洗練される。 組織的知識成長の非自明なシミュレーションに適用すると、このアプローチは、初期検証、明示的な不変性、設計による正当性を実現すると同時に、開発労力を大幅に削減し、最初の試みに対する正しい実装を生成する。

関連論文リスト

• Fast Thinking for Large Language Models [67.7238685892317]
  我々は、訓練中にのみ簡潔なCoTスケッチを使用して個別戦略事前のコードブックを学習するフレームワークであるLatent Codebooks for Fast Thinkingを紹介した。 推論では、コードブックから抽出した少数の連続的思考スイッチのモデル条件を1パスにすることで、明確な推論トークンを生成することなく、戦略レベルのガイダンスを可能にする。
  論文  参考訳（メタデータ） (2025-09-28T04:19:48Z)
• 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)
• Prompting Encoder Models for Zero-Shot Classification: A Cross-Domain Study in Italian [75.94354349994576]
  本稿では,より小型のドメイン固有エンコーダ LM と,特殊なコンテキストにおける性能向上手法の併用の可能性について検討する。 本研究は, イタリアの官僚的・法的言語に焦点をあて, 汎用モデルと事前学習型エンコーダのみのモデルの両方を実験する。 その結果, 事前学習したモデルでは, 一般知識の頑健性が低下する可能性があるが, ドメイン固有のタスクに対して, ゼロショット設定においても, より優れた適応性を示すことがわかった。
  論文  参考訳（メタデータ） (2024-07-30T08:50:16Z)
• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
  本稿では,検証対応言語における仕様の質を評価するための指標を提案する。 MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。 また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
  論文  参考訳（メタデータ） (2024-06-14T06:52:08Z)
• nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models [3.1143846686797314]
  大規模言語モデル(LLM)を適用するためのフレームワークであるnl2specは、構造化されていない自然言語から正式な仕様を導出する。 本稿では,自然言語におけるシステム要求のあいまいさを検知し,解決する新たな手法を提案する。 ユーザは、これらのサブ翻訳を反復的に追加、削除、編集して、不正なフォーマル化を修正する。
  論文  参考訳（メタデータ） (2023-03-08T20:08:53Z)
• Lexically-constrained Text Generation through Commonsense Knowledge Extraction and Injection [62.071938098215085]
  我々は、ある入力概念のセットに対して妥当な文を生成することを目的としているcommongenベンチマークに焦点を当てる。 生成したテキストの意味的正しさを高めるための戦略を提案する。
  論文  参考訳（メタデータ） (2020-12-19T23:23:40Z)

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

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