論文の概要: CAFÉ, an automated feedback tool to approach Formal Methods
- arxiv url: http://arxiv.org/abs/2607.03001v1
- Date: Fri, 03 Jul 2026 06:36:02 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-09 13:10:57.833226
- Title: CAFÉ, an automated feedback tool to approach Formal Methods
- Title（参考訳）: CAFÉ - フォーマルメソッドにアプローチするための自動フィードバックツール
- Abstract要約: CAFはコンピュータサイエンスの学生をフォーマルメソッド(FM)に導入するための学習プラットフォームである。
CAFは、図形ループ不変プログラミング(GLIBP)の実践を促進することによって、学生の構造的思考を足場にすることを目的とする
GLIBPアプローチでは、学習者はまず、対応するコードを導出する前にGLI(Graphical Loop Invariant)を構築することでループベースの問題を解決する。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We present CAFÉ, a learning platform designed to introduce computer science students to Formal Methods (FM). CAFÉ aims to scaffold students' structural thinking (in contrast with operational thinking) by promoting the practice of Graphical Loop Invariant Based Programming (GLIBP). In the GLIBP approach, students solve loop-based problems by first constructing a Graphical Loop Invariant (GLI) before deriving the corresponding code. The GLI is an informal diagrammatic representation of the loop invariant. It illustrates the variables involved in the loop, their properties, and the relationships between them. To enable automated feedback, students complete a blank GLI, a box-based version of the GLI. Beyond evaluating the code students submit, CAFÉ provides personalized feedback on students' GLI and its alignment with the code. In this demo, we walk through CAFE from both a student's and a teacher's perspective. We show how the tool supports GLI design and provides feedback. We then present how a teacher can encode programming challenges together with a corresponding blank GLI.
- Abstract（参考訳）: CAFÉは,コンピュータサイエンスの学生をフォーマルメソッド(FM)に導入するための学習プラットフォームである。
CAFÉは、グラフィカルループ不変ベースプログラミング(GLIBP)の実践を促進することによって、学生の構造的思考(運用的思考とは対照的に)を足場にすることを目的としている。
GLIBPアプローチでは、学習者はまず、対応するコードを導出する前にGLI(Graphical Loop Invariant)を構築することでループベースの問題を解決する。
GLI はループ不変量の非公式な図式表現である。
これはループに関わる変数、それらの特性、それらの間の関係を描いている。
自動フィードバックを可能にするため、学生は箱ベースのGLIである空白GLIを完成させる。
CAFÉは、学生が提出するコードの評価以外にも、学生のGLIとそのコードとの整合性に対するパーソナライズされたフィードバックを提供する。
このデモでは、学生の視点と教師の視点の両方からCAFEを通った。
ツールがGLI設計をどのようにサポートし、フィードバックを提供するかを示す。
次に,教師がプログラミング課題を,対応する空白GLIとともにエンコードする方法を示す。
関連論文リスト
- ICLF: An Immersive Code Learning Framework based on Git for Teaching and Evaluating Student Programming Projects [2.030202554182725]
Immersive Code Learning Framework (ICLF)は、学生プログラミングプロジェクトを管理し評価するためのスケーラブルなGitベースの組織パイプラインである。
学生は既存のコードベースから始めます。これは現実世界のソフトウェア開発をミラー化するのに不可欠なプラクティスです。
学生は、この中間リポジトリのプライベートフォークに招待され、教師が親リポジトリを変更するたびに、学期を通して更新される可能性がある。
論文 参考訳（メタデータ） (2026-01-21T09:39:17Z) - Autograder+: A Multi-Faceted AI Framework for Rich Pedagogical Feedback in Programming Education [0.5529795221640363]
Autograder+は、オートグレーディングを純粋に要約的なプロセスからフォーマティブな学習体験に移行するように設計されている。
微調整されたLarge Language Modelを使った自動フィードバック生成と、学習パターンを明らかにするための学生コード提出の可視化だ。
論文 参考訳（メタデータ） (2025-10-30T11:41:50Z) - Can Large Language Models Help Students Prove Software Correctness? An Experimental Study with Dafny [75.55915044740566]
コンピューティング教育の学生は、ChatGPTのような大きな言語モデル(LLM)をますます利用している。
本稿では,Dafny の形式的検証演習において,学生が LLM とどのように相互作用するかを検討する。
論文 参考訳（メタデータ） (2025-06-27T16:34:13Z) - Multimodal Programming in Computer Science with Interactive Assistance Powered by Large Language Model [0.0]
DeepSeek R1をベースとした対話型宿題支援システムを開発した。
生徒の仕事はパーソナライズされたプロンプトで包み、すぐに答えを出すことなく教育目的を前進させる。
論文 参考訳（メタデータ） (2025-03-09T10:48:47Z) - SocialGPT: Prompting LLMs for Social Relation Reasoning via Greedy Segment Optimization [70.11167263638562]
社会的関係推論は、友人、配偶者、同僚などの関係カテゴリを画像から識別することを目的としている。
まず、VFM(Vision Foundation Models)の知覚能力と、モジュラーフレームワーク内でのLLM(Large Language Models)の推論能力を組み合わせた、シンプルだが巧妙な名前のフレームワークを提示する。
論文 参考訳（メタデータ） (2024-10-28T18:10:26Z) - A Picture Is Worth a Thousand Words: Exploring Diagram and Video-Based
OOP Exercises to Counter LLM Over-Reliance [2.1490831374964587]
大規模言語モデル(LLM)は、テキストベースの仕様で、より複雑なオブジェクト指向プログラミング(OOP)の課題を効果的に解決することができる。
これは、学生がこれらのモデルを使って非倫理的に課題を完了させるため、学術的完全性に対する懸念を提起する。
本稿では,OOP の授業において,学生の課題解決を奨励し,学生をコピー・アンド・プロンプト・アプローチから遠ざける方法として,図表やビデオを用いてOOP タスクを定式化する革新的な手法を提案する。
論文 参考訳（メタデータ） (2024-03-13T10:21:29Z) - CLOVA: A Closed-Loop Visual Assistant with Tool Usage and Update [69.59482029810198]
CLOVAは、推論、リフレクション、学習フェーズを含むフレームワーク内で動作するクローズドループビジュアルアシスタントである。
その結果,CLOVAは既存のツール利用手法を5%,知識タグ付けでは10%,画像編集では20%,視覚的質問応答や複数画像推論では5%に上回っていることがわかった。
論文 参考訳（メタデータ） (2023-12-18T03:34:07Z) - Students' Perceptions and Preferences of Generative Artificial
Intelligence Feedback for Programming [15.372316943507506]
そこで我々はChatGPT APIを用いて,導入型コンピュータサイエンスクラスにおける4つの実験室割り当てのための自動フィードバックを生成した。
学生は、フィードバックは、Shuteが確立した形式的なフィードバックガイドラインとよく一致していると感じた。
学生は通常、十分なコード例で特定の修正フィードバックを期待していたが、フィードバックのトーンについて意見が分かれていた。
論文 参考訳（メタデータ） (2023-12-17T22:26:53Z) - From Language Modeling to Instruction Following: Understanding the Behavior Shift in LLMs after Instruction Tuning [63.63840740526497]
そこで本研究では,本質的な変化に着目した事前学習モデルの調整方法について検討する。
次に、事前訓練されたモデルと命令調整されたモデルから導かれた説明を比較することで、命令チューニングの影響について研究する。
この結果から,指導指導の3つの重要な影響が明らかになった。
論文 参考訳（メタデータ） (2023-09-30T21:16:05Z) - Fine-grained Visual-Text Prompt-Driven Self-Training for Open-Vocabulary
Object Detection [87.39089806069707]
オープン語彙検出(VTP-OVD)のための微粒なビジュアルテキストプロンプト駆動型自己学習パラダイムを提案する。
適応段階では、学習可能なテキストプロンプトを用いて細粒度アライメントを可能とし、補助的なピクセルワイズ予測タスクを解決する。
実験の結果,COCO の未確認クラスでは,31.5% mAP など,オープン語彙オブジェクト検出の最先端性能が得られた。
論文 参考訳（メタデータ） (2022-11-02T03:38:02Z) - ProtoTransformer: A Meta-Learning Approach to Providing Student Feedback [54.142719510638614]
本稿では,フィードバックを数発の分類として提供するという課題について考察する。
メタラーナーは、インストラクターによるいくつかの例から、新しいプログラミング質問に関する学生のコードにフィードバックを与えるように適応します。
本手法は,第1段階の大学が提供したプログラムコースにおいて,16,000名の学生試験ソリューションに対するフィードバックの提供に成功している。
論文 参考訳（メタデータ） (2021-07-23T22:41:28Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。