論文の概要: LLM-Based Static Verification of Code Against Natural-Language Requirements: An Industrial Experience Report
- arxiv url: http://arxiv.org/abs/2605.17926v1
- Date: Mon, 18 May 2026 06:34:03 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-19 17:57:48.922135
- Title: LLM-Based Static Verification of Code Against Natural-Language Requirements: An Industrial Experience Report
- Title（参考訳）: LLMに基づく天然資源要求に対するコードの静的検証:産業経験報告
- Authors: Zhi Quan Zhou, Dave Towey, Tsong Yueh Chen,
- Abstract要約: 本稿では,この課題に対処するための2段階のLLMベースのワークフローを,インテリジェント車両サイバーセキュリティケーススタディで紹介する。
第一段階では、AIベースのルールマイナーが自然言語要求から検証可能なルールを抽出する。
第2段階では、AIベースのコード監査者が、抽出されたルールに対する実装証拠をチェックする。
- 参考スコア（独自算出の注目度）: 3.5867640049033054
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Large language models (LLMs) are increasingly used to generate requirements specifications, design documents, code, and test cases. In contrast, much less attention has been given to a more difficult assurance problem: statically verifying whether implemented code satisfies requirements written in natural language. Conventional static analysis tools are effective at detecting coding defects and known vulnerability patterns, but they cannot determine whether program behavior matches intended business logic. Detecting such defects requires reasoning over the specification rather than the code alone. Software testing can expose some of these mismatches, but its effectiveness depends heavily on test design, executable artifacts, and runtime environments. This article presents a two-stage LLM-based workflow for addressing this challenge in an intelligent-vehicle cybersecurity case study. In the first stage, an AI-based rule miner extracts verifiable rules from natural-language requirements while explicitly identifying ambiguity, self-contradiction, and other non-verifiable statements. In the second stage, an AI-based code auditor checks implementation evidence against the extracted rules. Instead of asking a single LLM to directly verify code against lengthy natural-language specifications, the workflow introduces a structured intermediate representation to reduce hallucination, output variability, limited explainability, and context loss. The resulting approach is a requirement-aware and semantics-aware form of static analysis that complements software testing. By analyzing requirements and source code without requiring compilation, execution, or runtime environments, the method shifts verification and validation activities left in the development lifecycle. This LLM-based static analysis is also a new approach to addressing the test oracle problem.
- Abstract（参考訳）: 大規模言語モデル(LLM)は、要求仕様、設計文書、コード、テストケースを生成するためにますます使われています。
対照的に、より難しい保証問題に対して、より少ない注意が向けられている: 実装されたコードが自然言語で書かれた要求を満たすかどうかを静的に検証する。
従来の静的解析ツールは、コーディング欠陥や既知の脆弱性パターンを検出するのに効果的だが、プログラムの振る舞いが意図したビジネスロジックと一致するかどうかを判断することはできない。
このような欠陥を検出するには、コードのみではなく仕様を推論する必要がある。
ソフトウェアテストはこれらのミスマッチの一部を露呈するが、その効果はテスト設計、実行可能アーティファクト、実行環境に大きく依存する。
本稿では,この課題に対処するための2段階のLLMベースのワークフローを,インテリジェント車両サイバーセキュリティケーススタディで紹介する。
第一段階では、AIベースのルールマイナーが自然言語要求から検証可能なルールを抽出し、曖昧さ、自己矛盾、その他の検証不可能なステートメントを明確に識別する。
第2段階では、AIベースのコード監査者が、抽出されたルールに対する実装証拠をチェックする。
1つのLLMに、長い自然言語仕様のコードを直接検証するように要求する代わりに、このワークフローは幻覚、出力変数、限定的な説明可能性、コンテキスト損失を減らすための構造化された中間表現を導入する。
結果として生じるアプローチは、ソフトウェアテストを補完する要件対応とセマンティクス対応の静的分析形式である。
コンパイル、実行、実行環境を必要とせずに要求とソースコードを分析することで、このメソッドは開発ライフサイクルに残っている検証と検証のアクティビティをシフトする。
このLSMベースの静的解析は、テストオラクル問題に対処する新しいアプローチでもある。
関連論文リスト
- From I/O to Code with Discovery Agent [103.88427301265669]
IO2Codeの発見エージェントであるDIO-Agentを提案する。
本手法は,プログラム空間上の進化的探索としてIO2Codeをフレーム化する。
大規模な実験により、DIO-Agentは従来のプログラムバイサンプル法とSOTA進化エージェントベースラインの両方を一貫して上回っていることが示された。
論文 参考訳（メタデータ） (2026-05-14T18:57:32Z) - LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。
CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
論文 参考訳（メタデータ） (2026-05-02T11:31:33Z) - Assessing the Impact of Requirement Ambiguity on LLM-based Function-Level Code Generation [14.755517753769837]
Orchidは、曖昧な要求で特別に設計された最初のコード生成ベンチマークです。
これは、語彙、構文、意味、曖昧さの4つの異なる種類の曖昧さをカバーする1,304の関数レベルタスクからなる。
この結果から,高度モデルにおいて最も顕著な負の効果が観察され,不明瞭さは全ての評価LCMの性能を常に低下させることが示された。
論文 参考訳（メタデータ） (2026-04-23T10:07:33Z) - Are LLMs Reliable Code Reviewers? Systematic Overcorrection in Requirement Conformance Judgement [8.059802912761919]
我々は,大規模言語モデル(LLM)が自然言語要求にマッチするコードの体系的失敗を明らかにする。
より詳細なプロンプト設計、特に説明や修正提案を必要とするものは、より高い誤判定率をもたらす。
そこで本稿では,提案した修正を実効的証拠として扱う固定誘導検証フィルタを提案する。
論文 参考訳（メタデータ） (2026-02-28T08:35:25Z) - Operational Robustness of LLMs on Code Generation [2.9232837969697965]
現在、大規模言語モデル(LLM)のためのソフトウェア開発において、プログラムコードを生成するために使われるのが一般的である。
本稿では,LLMがコーディングタスクの記述の変化にどれほど敏感であるかを考察する。
このロバスト性を評価するための既存の技術は、自然言語記述の入力データ空間が離散的であるため、コード生成には適さない。
論文 参考訳（メタデータ） (2026-02-21T11:21:13Z) - Environment-Aware Code Generation: How far are We? [52.69113158357018]
大規模言語モデル(LLM)がユーザの特定の環境に適した実行可能コードを確実に生成できるかどうかは不明である。
本稿では,環境対応コード生成(EACG)の最初の体系的研究について述べる。
その結果,現在のLLMは環境固有のコード生成に苦しむ一方で,環境の適合性や実行性も向上していることがわかった。
論文 参考訳（メタデータ） (2026-01-18T04:58:15Z) - Rethinking Testing for LLM Applications: Characteristics, Challenges, and a Lightweight Interaction Protocol [83.83217247686402]
大言語モデル(LLM)は、単純なテキストジェネレータから、検索強化、ツール呼び出し、マルチターンインタラクションを統合する複雑なソフトウェアシステムへと進化してきた。
その固有の非決定主義、ダイナミズム、文脈依存は品質保証に根本的な課題をもたらす。
本稿では,LLMアプリケーションを3層アーキテクチャに分解する: textbftextitSystem Shell Layer, textbftextitPrompt Orchestration Layer, textbftextitLLM Inference Core。
論文 参考訳（メタデータ） (2025-08-28T13:00:28Z) - Uncovering Systematic Failures of LLMs in Verifying Code Against Natural Language Specifications [0.6813925418351435]
大規模言語モデル(LLM)はソフトウェア開発において不可欠なツールとなり、要求工学、コード生成、レビュータスクに広く利用されている。
本稿では,LLMが自然言語の要求に適合するかどうかを評価する上で,体系的に失敗していることを明らかにする。
以上の結果から,LCMは要件を満たすことのできないコード実装や潜在的な欠陥を含むコード実装を誤って分類することが多いことが判明した。
論文 参考訳（メタデータ） (2025-08-17T13:07:26Z) - FaultLine: Automated Proof-of-Vulnerability Generation Using LLM Agents [17.658431034176065]
FaultLineはエージェントワークフローで、自動的にPoVテストケースを生成する。
言語固有の静的または動的分析コンポーネントは使用せず、プログラミング言語間で使用することができる。
Java、C、C++プロジェクトの既知の100の脆弱性のデータセット上で、FaultLineは16プロジェクトのPoVテストを生成することができる。
論文 参考訳（メタデータ） (2025-07-21T04:55:34Z) - Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。
実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
論文 参考訳（メタデータ） (2025-05-28T17:57:47Z) - Exploring Software Naturalness through Neural Language Models [56.1315223210742]
ソフトウェア自然性仮説(Software Naturalness hypothesis)は、自然言語処理で使用されるのと同じ手法でプログラミング言語を理解することができると主張している。
この仮説は,事前学習されたトランスフォーマーベース言語モデルを用いて,コード解析タスクを実行することによって検討する。
論文 参考訳（メタデータ） (2020-06-22T21:56:14Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。