論文の概要: Natural Language based Specification and Verification
- arxiv url: http://arxiv.org/abs/2605.11315v1
- Date: Mon, 11 May 2026 23:07:22 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-13 21:48:56.469496
- Title: Natural Language based Specification and Verification
- Title（参考訳）: 自然言語に基づく仕様と検証
- Authors: Zhaorui Li, Chengyu Song,
- Abstract要約: 大規模言語モデル(LLM)は、大規模で成熟したオープンソースシステムのセキュリティ脆弱性を特定する上で、強力なパフォーマンスを示している。
本稿では、LLMを用いて仕様を生成し、その仕様が自然言語で表現されたときに構成的に実装を検証するという、異なるアプローチについて検討する。
- 参考スコア（独自算出の注目度）: 7.776617933367878
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Recent frontier large language models (LLMs) have shown strong performance in identifying security vulnerabilities in large, mature open-source systems. As LLM-generated code becomes increasingly common, a natural goal is to prevent such models from producing vulnerable implementations in the first place. Formal verification offers a principled route to this objective, but existing verification pipelines typically require specifications written in rigid formal languages. Prior work has explored using LLMs to synthesize such specifications, with limited success. In this paper, we investigate a different approach: using LLMs both to generate specifications and to verify implementations compositionally when the specifications are expressed in natural language. Our preliminary results suggest that this approach is promising.
- Abstract（参考訳）: 最近のフロンティア大型言語モデル(LLM)は、大規模で成熟したオープンソースシステムにおけるセキュリティ脆弱性を特定する上で、強力なパフォーマンスを示している。
LLM生成コードがますます一般的になるにつれて、そのようなモデルがそもそも脆弱な実装を生成するのを防ぐことが自然な目標である。
形式的検証は、この目的への原則的な経路を提供するが、既存の検証パイプラインは通常、形式的な形式言語で書かれた仕様を必要とする。
以前の研究では、LLMを使用してそのような仕様を合成し、限られた成功を収めてきた。
本稿では、LLMを用いて仕様を生成し、その仕様が自然言語で表現されたときに構成的に実装を検証するという、異なるアプローチについて検討する。
予備的な結果は、このアプローチが有望であることを示唆している。
関連論文リスト
- 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) - Towards Autoformalization of LLM-generated Outputs for Requirement Verification [0.6015898117103068]
非公式な文を形式論理に翻訳するプロセスであるオートフォーマル化は、強力な大規模言語モデルの出現により、新たな関心を集めている。
本稿では,LLMをベースとした簡易なオートフォーマライザを用いて,LLM生成した出力を少数の自然言語要求に対して検証する。
この結果から, LLM出力の完全性と論理的整合性を確保する上で, 自己形式化が有意な可能性を示唆した。
論文 参考訳（メタデータ） (2025-11-14T19:45:17Z) - Verifying Memoryless Sequential Decision-making of Large Language Models [4.570003973862485]
本稿では,大規模言語モデル(LLM)に基づく政策を逐次意思決定タスクにおいて厳密かつ自動検証するツールを提案する。
逐次意思決定タスクを表すマルコフ決定プロセス(MDP)、LCMポリシー、およびPCTL式として表現される安全要件を考慮し、本手法はMDPの到達可能な部分のみを段階的に構成する。
結果の形式モデルがStormでチェックされ、ポリシーが指定された安全資産を満たすかどうかが決定される。
論文 参考訳（メタデータ） (2025-10-08T08:31:48Z) - How Good LLM-Generated Password Policies Are? [0.1747820331822631]
サイバーセキュリティアクセス制御システムにおける大規模言語モデルの応用について検討する。
具体的には、LLM生成したパスワードポリシーの一貫性と正確性を調べ、自然言語のプロンプトをpwquality.conf設定ファイルに翻訳する。
本研究は,LLM の現世代における重要な課題を浮き彫りにして,アクセス制御システムにおける LLM の展開に関する貴重な知見を提供するものである。
論文 参考訳（メタデータ） (2025-06-10T01:12:31Z) - Type-Constrained Code Generation with Language Models [51.03439021895432]
本稿では,型システムを利用してコード生成を誘導する型制約デコード手法を提案する。
そこで本研究では,新しい接頭辞オートマトンと,在来型を探索する手法を開発し,LLM生成コードに適切な型付けを強制するための健全なアプローチを構築した。
提案手法は,コード合成,翻訳,修復作業において,コンパイルエラーを半分以上削減し,機能的正しさを著しく向上させる。
論文 参考訳（メタデータ） (2025-04-12T15:03:00Z) - Unnatural Languages Are Not Bugs but Features for LLMs [92.8332103170009]
大規模言語モデル(LLM)は、ジェイルブレイクプロンプトなどの非可読テキストシーケンスを処理するために観察されている。
我々はこの認識に挑戦する体系的な調査を行い、非自然言語にはモデルで使用可能な潜在的特徴が含まれていることを示した。
論文 参考訳（メタデータ） (2025-03-02T12:10:17Z) - DECIDER: A Dual-System Rule-Controllable Decoding Framework for Language Generation [57.07295906718989]
制約付き復号法は,事前訓練された大言語(Ms と PLMs)が生成するテキストの意味やスタイルを,推論時に様々なタスクに対して制御することを目的としている。
これらの方法は、しばしば、欲求的かつ明示的にターゲットを選択することによって、もっともらしい連続を導く。
認知二重プロセス理論に着想を得て,新しい復号化フレームワークDECDERを提案する。
論文 参考訳（メタデータ） (2024-03-04T11:49:08Z) - How Effective are Large Language Models in Generating Software Specifications? [14.170320751508502]
大規模言語モデル(LLM)は多くのソフトウェア工学(SE)タスクにうまく適用されている。
ソフトウェアコメントやドキュメンテーションからソフトウェア仕様を生成するためのLCMの能力を評価するための、最初の実証的研究を行う。
論文 参考訳（メタデータ） (2023-06-06T00:28:39Z) - LMPriors: Pre-Trained Language Models as Task-Specific Priors [78.97143833642971]
適切な事前条件でモデルを拡張するための原則的手法を開発した。
これは、世界に対する私たちの理解と相容れない方法で学ぶことを奨励するものです。
我々は,近年の大規模言語モデル(LM)の成功から着想を得た。
論文 参考訳（メタデータ） (2022-10-22T19:09:18Z) - Exploring Software Naturalness through Neural Language Models [56.1315223210742]
ソフトウェア自然性仮説(Software Naturalness hypothesis)は、自然言語処理で使用されるのと同じ手法でプログラミング言語を理解することができると主張している。
この仮説は,事前学習されたトランスフォーマーベース言語モデルを用いて,コード解析タスクを実行することによって検討する。
論文 参考訳（メタデータ） (2020-06-22T21:56:14Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。