論文の概要: Can Large Language Models Help Students Prove Software Correctness? An Experimental Study with Dafny

• arxiv url: http://arxiv.org/abs/2506.22370v1
• Date: Fri, 27 Jun 2025 16:34:13 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-06-30 21:12:23.286693
• Title: Can Large Language Models Help Students Prove Software Correctness? An Experimental Study with Dafny
• Title（参考訳）: 大規模言語モデルは学生にソフトウェアの正確性を証明するのに役立つか?Dafnyを用いた実験的検討
• Authors: Carolina Carreira, Álvaro Silva, Alexandre Abreu, Alexandra Mendes,
• Abstract要約: コンピューティング教育の学生は、ChatGPTのような大きな言語モデル(LLM)をますます利用している。 本稿では,Dafny の形式的検証演習において,学生が LLM とどのように相互作用するかを検討する。
• 参考スコア（独自算出の注目度）: 79.56218230251953
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Students in computing education increasingly use large language models (LLMs) such as ChatGPT. Yet, the role of LLMs in supporting cognitively demanding tasks, like deductive program verification, remains poorly understood. This paper investigates how students interact with an LLM when solving formal verification exercises in Dafny, a language that supports functional correctness, by allowing programmers to write formal specifications and automatically verifying that the implementation satisfies the specification. We conducted a mixed-methods study with master's students enrolled in a formal methods course. Each participant completed two verification problems, one with access to a custom ChatGPT interface, that logged all interactions, and the other without. We identified strategies used by successful students and assessed the level of trust students place in LLMs. %\todo{Our findings show that something here} Our findings show that students perform significantly better when using ChatGPT; however, performance gains are tied to prompt quality. We conclude with practical recommendations for integrating LLMs into formal methods courses more effectively, including designing LLM-aware challenges that promote learning rather than substitution.
• Abstract（参考訳）: コンピューティング教育の学生は、ChatGPTのような大きな言語モデル(LLM)をますます利用している。 しかし、認知的に要求されるタスクを支援する上でLLMが果たす役割は、演能的プログラム検証のように、まだよく理解されていない。 本稿では,プログラマが形式仕様を書けるようにし,実装が仕様を満たすことを自動検証することで,機能的正当性をサポートする言語であるDafnyにおける形式的検証演習の解決において,学生がLLMとどのように相互作用するかを検討する。 本研究は,修士課程に入学した学生を対象に,混合メソドス実験を行った。 各参加者は2つの検証問題を完成させた。1つはカスタムのChatGPTインターフェースにアクセスでき、もう1つはすべてのインタラクションをログし、もう1つは不要だった。 我々は,成功した学生が使用する戦略を特定し,LLMにおける信頼度を評価した。 %\todo{Our findings show that something here</a> 以上の結果から,ChatGPTを用いた場合,学生の成績は有意に向上したが,性能向上は即時性に結びついていることがわかった。 LLMを形式的方法のコースに統合する実践的な推奨事項として,代替よりも学習を促進するLLM対応の課題を設計する。

関連論文リスト

• LLMs are Imperfect, Then What? An Empirical Study on LLM Failures in Software Engineering [38.20696656193963]
  非自明なソフトウェアエンジニアリングタスクにおいて,ChatGPTをコーディングアシスタントとして使用した22名の参加者を対象に,観察的研究を行った。 そこで我々は,ChatGPTが失敗した事例,その根本原因,およびユーザが使用する緩和ソリューションを特定した。
  論文  参考訳（メタデータ） (2024-11-15T03:29:41Z)
• Exploring Knowledge Tracing in Tutor-Student Dialogues using LLMs [49.18567856499736]
  本研究では,大規模言語モデル(LLM)が対話学習を支援することができるかどうかを検討する。 我々は,学習者の知識レベルを対話全体にわたって追跡するために,ラベル付きデータに知識追跡(KT)手法を適用した。 我々は,2つの学習対話データセットの実験を行い,従来のKT手法よりも学生の反応の正しさを予測できる新しいLCM-based method LLMKTが優れていることを示す。
  論文  参考訳（メタデータ） (2024-09-24T22:31:39Z)
• The GPT Surprise: Offering Large Language Model Chat in a Massive Coding Class Reduced Engagement but Increased Adopters Exam Performances [26.688772122455745]
  大規模言語モデル(LLM)は、幅広い学習経験において急速に採用されている。 我々は,146カ国から5,831人の学生を対象に,大規模ランダム化制御試験を行った。 受験者, 受験者, 受験者, 受験者に対して, GPT-4の広告が有意な減少を招いた。
  論文  参考訳（メタデータ） (2024-04-25T15:39:22Z)
• Rethinking the Roles of Large Language Models in Chinese Grammatical Error Correction [62.409807640887834]
  中国語の文法的誤り訂正(CGEC)は、入力文中のすべての文法的誤りを修正することを目的としている。 CGECの修正器としてのLLMの性能は、課題の焦点が難しいため不満足なままである。 CGECタスクにおけるLCMの役割を再考し、CGECでよりよく活用し、探索できるようにした。
  論文  参考訳（メタデータ） (2024-02-18T01:40:34Z)
• Why and When LLM-Based Assistants Can Go Wrong: Investigating the Effectiveness of Prompt-Based Interactions for Software Help-Seeking [5.755004576310333]
  大規模言語モデル(LLM)アシスタントは、ユーザーがソフトウェアをナビゲートするための検索方法の潜在的な代替手段として登場した。 LLMアシスタントは、ドメイン固有のテキスト、ソフトウェアマニュアル、コードリポジトリからの膨大なトレーニングデータを使用して、人間のようなインタラクションを模倣する。
  論文  参考訳（メタデータ） (2024-02-12T19:49:58Z)
• AlignedCoT: Prompting Large Language Models via Native-Speaking Demonstrations [52.43593893122206]
  Alignedcotは、大規模言語モデルを呼び出すためのコンテキスト内学習技術である。 ゼロショットシナリオでは、一貫した正しいステップワイズプロンプトを達成する。 数学的推論とコモンセンス推論の実験を行う。
  論文  参考訳（メタデータ） (2023-11-22T17:24:21Z)
• ICL-D3IE: In-Context Learning with Diverse Demonstrations Updating for Document Information Extraction [56.790794611002106]
  大規模言語モデル(LLM)は、様々な自然言語処理(NLP)タスクにおいて、文脈内学習による顕著な結果を示している。 ICL-D3IEと呼ばれるシンプルだが効果的なテキスト内学習フレームワークを提案する。 具体的には、ハードトレーニング文書から最も困難で独特なセグメントをハードデモとして抽出する。
  論文  参考訳（メタデータ） (2023-03-09T06:24:50Z)

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

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