論文の概要: ProofBuddy: How it Started, How it's Going
- arxiv url: http://arxiv.org/abs/2505.13474v1
- Date: Fri, 09 May 2025 12:18:32 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-05-25 10:52:49.0576
- Title: ProofBuddy: How it Started, How it's Going
- Title(参考訳): ProofBuddy:スタートの仕方と動き方
- Authors: Nadine Karsten, Kim Jana Eiken, Uwe Nestmann,
- Abstract要約: 本稿では,証明アシスタントIsabelleのサーバサイドインスタンスを利用したWebアプリケーションProofBuddyの開発について報告する。
利点は単純さ、保守性、カスタマイズ性です。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We report on our journey to develop ProofBuddy, a web application that is powered by a server-side instance of the proof assistant Isabelle, for the teaching and learning of proofs and proving. The journey started from an attempt to use just Isabelle in an educational context. Along the way, following the educational design research approach with a series of experiments and their evaluations, we observed that a web application like \ProofBuddy has many advantages over a desktop application, for developers and teachers as well as for students. In summary, the advantages cover simplicity, maintainability and customizability. We particularly highlight the latter by exhibiting the potential of interactive tutorials and their implementation within ProofBuddy.
- Abstract(参考訳): 本稿では,証明アシスタントIsabelleのサーバサイドインスタンスを利用して,証明と証明の指導と学習を行うWebアプリケーションProofBuddyの開発について報告する。
この旅は、イザベルだけを教育的な文脈で利用しようとする試みから始まった。
その過程で、一連の実験と評価による教育設計研究のアプローチに従い、‘ProofBuddy’のようなWebアプリケーションは、開発者や教師だけでなく、学生にとってもデスクトップアプリケーションよりも多くの利点があることを示した。
要約すると、利点は単純さ、保守性、カスタマイズ性である。
特に,ProofBuddyにおける対話型チュートリアルとその実装の可能性を示すことで,後者を強調した。
関連論文リスト
- The "Huh?" Button: Improving Understanding in Educational Videos with Large Language Models [7.237493755167876]
本稿では,大規模言語モデル(LLM)を教育に利用する簡単な方法を提案する。
具体的には、オンラインビデオに新たな機能を追加することで、個人の理解を改善することを目的としている。
論文 参考訳(メタデータ) (2024-12-15T21:02:16Z) - ProofBuddy: A Proof Assistant for Learning and Monitoring [0.0]
証明能力(Proof competence)、すなわち、(数学的な)証明を書き、チェックする能力は、コンピュータ科学において重要なスキルである。
主な問題は、形式言語の正しい使用と証明、特に学生自身の証明が完璧で正しいかどうかの確認である。
多くの著者は、証明能力を教えるのに証明アシスタントを使うことを提案したが、その方法の有効性は明らかではない。
デンマーク工科大学でProofBuddyのユーザビリティに関する予備的な研究を行った。
論文 参考訳(メタデータ) (2023-08-14T07:08:55Z) - Exploring the Benefits of Visual Prompting in Differential Privacy [54.56619360046841]
Visual Prompting (VP)は、よく訓練されたフリーズソースモデルを設計することで、下流タスクへのサンプル効率の適応を可能にする、新しくて強力なテクニックである。
本稿では,VPを標準DPトレーニング手法に統合し,そのシンプルさと効率性を実証する。
論文 参考訳(メタデータ) (2023-03-22T01:01:14Z) - Active Teacher for Semi-Supervised Object Detection [80.10937030195228]
半教師対象検出(SSOD)のための能動教師と呼ばれる新しいアルゴリズムを提案する。
Active Teacherは、教師/学生のフレームワークを反復的なバージョンに拡張し、ラベルセットを部分的に段階的に拡張し、ラベルなし例の3つの重要な要素を評価する。
この設計により、Active Teacherは、擬似ラベルの品質を改善しながら、限られたラベル情報の効果を最大化することができる。
論文 参考訳(メタデータ) (2023-03-15T03:59:27Z) - On Exams with the Isabelle Proof Assistant [0.0]
本稿では,Isabelle証明アシスタントを用いた自動推論のコースにおいて,学生の学習結果をテストするためのアプローチを提案する。
このアプローチにより、様々な論理的証明システムにおける形式的証明の一般的な理解と、イザベル/HOLの高階論理における証明の理解の両方をテストすることができる。
論文 参考訳(メタデータ) (2023-03-10T11:37:09Z) - Benchopt: Reproducible, efficient and collaborative optimization
benchmarks [67.29240500171532]
Benchoptは、機械学習で最適化ベンチマークを自動化、再生、公開するためのフレームワークである。
Benchoptは実験を実行、共有、拡張するための既製のツールを提供することで、コミュニティのベンチマークを簡単にする。
論文 参考訳(メタデータ) (2022-06-27T16:19:24Z) - Multi-Task Learning based Online Dialogic Instruction Detection with
Pre-trained Language Models [34.66425105076059]
コントラッシブ・ロスによりカテゴリ間のマージンを大きくすることで、異なるクラスのインスタンスを識別する能力を向上するマルチタスク・パラダイムを提案する。
実世界のオンライン教育データセットを用いた実験により,本手法が代表的ベースラインよりも優れた性能を発揮することが示された。
論文 参考訳(メタデータ) (2021-07-15T04:57:57Z) - Visual Transformer for Task-aware Active Learning [49.903358393660724]
プールベースのアクティブラーニングのための新しいパイプラインを提案する。
提案手法は,学習中に使用可能なアンラベリング例を利用して,ラベル付き例との相関関係を推定する。
ビジュアルトランスフォーマーは、ラベル付き例と非ラベル付き例の間の非ローカルビジュアル概念依存性をモデル化する。
論文 参考訳(メタデータ) (2021-06-07T17:13:59Z) - Beyond Language: Learning Commonsense from Images for Reasoning [78.33934895163736]
本稿では,限られた原文や高価に構築された知識ベースの代わりに,画像からコモンセンスを学習するための新しいアプローチを提案する。
私たちのモチベーションは、画像が1000ワードの価値があるという事実から来ています。
論文 参考訳(メタデータ) (2020-10-10T13:47:13Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。