論文の概要: Can ChatGPT support software verification?

• arxiv url: http://arxiv.org/abs/2311.02433v1
• Date: Sat, 4 Nov 2023 15:25:18 GMT
• ステータス: 処理完了
• システム内更新日: 2023-11-07 17:45:53.268763
• Title: Can ChatGPT support software verification?
• Title（参考訳）: ChatGPTはソフトウェア検証をサポートできるか?
• Authors: Christian Jan{\ss}en, Cedric Richter, Heike Wehrheim
• Abstract要約: ループ不変量で106個のCプログラムにアノテートするようChatGPTに依頼する。 本稿では,Frama-C と CPA Checker の2つの検証器に渡すことで,生成した不変量の妥当性と有用性を確認する。 評価の結果,ChatGPTはFrama-Cがこれまで解決できなかったタスクを検証できる有効かつ有用な不変量を生成することができることがわかった。
• 参考スコア（独自算出の注目度）: 0.9668407688201361
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Large language models have become increasingly effective in software engineering tasks such as code generation, debugging and repair. Language models like ChatGPT can not only generate code, but also explain its inner workings and in particular its correctness. This raises the question whether we can utilize ChatGPT to support formal software verification. In this paper, we take some first steps towards answering this question. More specifically, we investigate whether ChatGPT can generate loop invariants. Loop invariant generation is a core task in software verification, and the generation of valid and useful invariants would likely help formal verifiers. To provide some first evidence on this hypothesis, we ask ChatGPT to annotate 106 C programs with loop invariants. We check validity and usefulness of the generated invariants by passing them to two verifiers, Frama-C and CPAchecker. Our evaluation shows that ChatGPT is able to produce valid and useful invariants allowing Frama-C to verify tasks that it could not solve before. Based on our initial insights, we propose ways of combining ChatGPT (or large language models in general) and software verifiers, and discuss current limitations and open issues.
• Abstract（参考訳）: 大規模な言語モデルは,コード生成やデバッグ,修復といったソフトウェアエンジニアリングタスクにおいて,ますます効果的になっています。 chatgptのような言語モデルはコードを生成するだけでなく、内部動作や特に正確性を説明することができる。 これにより、ChatGPTを使って正式なソフトウェア検証をサポートできるかという疑問が持ち上がる。 本稿では,この質問に答える第一歩を踏み出す。 具体的には,ChatGPTがループ不変量を生成できるかどうかを検討する。 ループ不変量生成はソフトウェア検証における中核的なタスクであり、有効な不変量の生成は形式的検証に役立つ可能性が高い。 この仮説に関する最初の証拠を与えるため、ChatGPT にループ不変量を持つ 106 C プログラムにアノテートを依頼する。 frama-c と cpachecker の2つの検証器に渡して生成した不変量の有効性と有用性を確認した。 評価の結果,ChatGPTはFrama-Cがこれまで解決できなかったタスクを検証できる有効かつ有用な不変量を生成することができることがわかった。 最初の知見に基づいて,ChatGPT(あるいは大規模言語モデル)とソフトウェア検証器を組み合わせる方法を提案し,現状の限界とオープンな問題について議論する。

関連論文リスト

• Fight Fire with Fire: How Much Can We Trust ChatGPT on Source Code-Related Tasks? [10.389763758883975]
  近年の研究では、ChatGPTを開発者とテスターの両方に活用することを提案した。 コード生成,コード補完,プログラム修復におけるChatGPTの自己検証能力を評価するための総合的な実証的研究を行う。
  論文  参考訳（メタデータ） (2024-05-21T09:47:33Z)
• Investigating the Utility of ChatGPT in the Issue Tracking System: An Exploratory Study [5.176434782905268]
  本研究は,ChatGPTと開発者間の相互作用を分析し,それらの活動を分析し,解決するものである。 私たちの調査によると、開発者は主にブレインストーミングソリューションにChatGPTを使用しているが、しばしばChatGPT生成コードを使う代わりにコードを書くことを選ぶ。
  論文  参考訳（メタデータ） (2024-02-06T06:03:05Z)
• Exploring ChatGPT's Capabilities on Vulnerability Management [56.4403395100589]
  我々は、70,346のサンプルを含む大規模なデータセットを用いて、完全な脆弱性管理プロセスを含む6つのタスクでChatGPTの機能を探求する。 注目すべき例として、ChatGPTのソフトウェアバグレポートのタイトル生成などのタスクにおける熟練度がある。 以上の結果から,ChatGPTが抱える障害が明らかとなり,将来的な方向性に光を当てた。
  論文  参考訳（メタデータ） (2023-11-11T11:01:13Z)
• Primacy Effect of ChatGPT [69.49920102917598]
  本稿では,ChatGPTの優位性について検討する。 実験と分析により、より信頼性の高いChatGPTベースのソリューションを構築する上で、さらなる洞察が得られればと思っています。
  論文  参考訳（メタデータ） (2023-10-20T00:37:28Z)
• Automatic Code Summarization via ChatGPT: How Far Are We? [10.692654700225411]
  CSN-Pythonと呼ばれる広く使われているPythonデータセット上でChatGPTを評価する。 BLEUとROUGE-Lでは、ChatGPTのコード要約性能は3つのSOTAモデルと比べて著しく劣っている。 この結果に基づき、ChatGPTベースのコード要約におけるいくつかのオープンな課題と機会を概説する。
  論文  参考訳（メタデータ） (2023-05-22T09:43:40Z)
• ChatLog: Carefully Evaluating the Evolution of ChatGPT Across Time [54.18651663847874]
  ChatGPTは大きな成功をおさめ、インフラ的な地位を得たと考えられる。 既存のベンチマークでは,(1)周期的評価の無視,(2)きめ細かい特徴の欠如という2つの課題に直面する。 2023年3月から現在まで,21のNLPベンチマークに対して,さまざまな長文ChatGPT応答を大規模に記録した常時更新データセットであるChatLogを構築している。
  論文  参考訳（メタデータ） (2023-04-27T11:33:48Z)
• Is ChatGPT the Ultimate Programming Assistant -- How far is it? [11.943927095071105]
  ChatGPTは非常に注目されており、ソースコードを議論するためのボットとして使用できる。 完全自動プログラミングアシスタントとしてのChatGPTの可能性について実証的研究を行った。
  論文  参考訳（メタデータ） (2023-04-24T09:20:13Z)
• When do you need Chain-of-Thought Prompting for ChatGPT? [87.45382888430643]
  CoT(Chain-of-Thought)は,大規模言語モデル(LLM)から複雑な多段階推論を効果的に引き出すことができる CoT がChatGPT などの最近の命令微調整 (IFT) LLM に対してまだ有効であるかどうかは不明である。
  論文  参考訳（メタデータ） (2023-04-06T17:47:29Z)
• ChatGPT or Grammarly? Evaluating ChatGPT on Grammatical Error Correction Benchmark [11.36853733574956]
  ChatGPTはOpenAIが開発した最先端の人工知能言語モデルである。 商用のGEC製品(例:Grammarly)や最先端のモデル(例:GECToR)と比較する。 また,ChatGPTは,自動評価指標の基準値ほど性能が良くないことがわかった。
  論文  参考訳（メタデータ） (2023-03-15T00:35:50Z)
• Can ChatGPT Understand Too? A Comparative Study on ChatGPT and Fine-tuned BERT [103.57103957631067]
  チャットGPTは、人間の質問に対する流動的で高品質な応答を生成できるため、大きな注目を集めている。 そこで我々は,ChatGPTの理解能力を,最も人気のあるGLUEベンチマークで評価し,より詳細な4種類のBERTスタイルのモデルと比較した。 2)ChatGPTは,感情分析や質問応答タスクにおいて,BERTと同等のパフォーマンスを達成している。
  論文  参考訳（メタデータ） (2023-02-19T12:29:33Z)
• Is ChatGPT a General-Purpose Natural Language Processing Task Solver? [113.22611481694825]
  大規模言語モデル(LLM)は、さまざまな自然言語処理(NLP)タスクをゼロショットで実行できることを実証している。 近年、ChatGPTのデビューは自然言語処理(NLP)コミュニティから大きな注目を集めている。 ChatGPTが多くのNLPタスクをゼロショットで実行できるジェネラリストモデルとして機能するかどうかはまだ分かっていない。
  論文  参考訳（メタデータ） (2023-02-08T09:44:51Z)

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

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