論文の概要: ProofBuddy: A Proof Assistant for Learning and Monitoring
- arxiv url: http://arxiv.org/abs/2308.06970v1
- Date: Mon, 14 Aug 2023 07:08:55 GMT
- ステータス: 処理完了
- システム内更新日: 2023-08-15 14:05:21.869209
- Title: ProofBuddy: A Proof Assistant for Learning and Monitoring
- Title(参考訳): ProofBuddy: 学習とモニタリングのためのProofアシスタント
- Authors: Nadine Karsten (Technische Universit\"at Berlin), Frederik Krogsdal
Jacobsen (Technical University of Denmark), Kim Jana Eiken (Technische
Universit\"at Berlin), Uwe Nestmann (Technische Universit\"at Berlin),
J{\o}rgen Villadsen (Technical University of Denmark)
- Abstract要約: 証明能力(Proof competence)、すなわち、(数学的な)証明を書き、チェックする能力は、コンピュータ科学において重要なスキルである。
主な問題は、形式言語の正しい使用と証明、特に学生自身の証明が完璧で正しいかどうかの確認である。
多くの著者は、証明能力を教えるのに証明アシスタントを使うことを提案したが、その方法の有効性は明らかではない。
デンマーク工科大学でProofBuddyのユーザビリティに関する予備的な研究を行った。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Proof competence, i.e. the ability to write and check (mathematical) proofs,
is an important skill in Computer Science, but for many students it represents
a difficult challenge. The main issues are the correct use of formal language
and the ascertainment of whether proofs, especially the students' own, are
complete and correct. Many authors have suggested using proof assistants to
assist in teaching proof competence, but the efficacy of the approach is
unclear. To improve the state of affairs, we introduce ProofBuddy: a web-based
tool using the Isabelle proof assistant which enables researchers to conduct
studies of the efficacy of approaches to using proof assistants in education by
collecting fine-grained data about the way students interact with proof
assistants. We have performed a preliminary usability study of ProofBuddy at
the Technical University of Denmark.
- Abstract(参考訳): 証明能力、すなわち(数学的な)証明を書き、チェックする能力は、コンピュータ科学において重要なスキルであるが、多くの学生にとって難しい課題である。
主な問題は、形式言語の正しい使用と、証明、特に学生自身の証明が完全で正しいかどうかの確認である。
多くの著者が証明アシスタントを用いて証明能力を教えることを提案したが、その方法の有効性は明らかでない。
そこで,本研究では,isabelle proof assistant を用いた web ベースのツールである proofbuddy について紹介する。
デンマーク工科大学でProofBuddyのユーザビリティに関する予備的な研究を行った。
関連論文リスト
- Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳(メタデータ) (2024-07-14T01:43:07Z) - Autograding Mathematical Induction Proofs with Natural Language Processing [0.12289361708127876]
本稿では,自由形式の数学的証明を自動分解できる一連のトレーニング手法とモデルを提案する。
モデルは、誘導問題によって4つの異なる証明から収集された証明データを用いて訓練される。
我々は、トレーニングデータと同じ証明を格付けするために、人間のグルーパーを雇い、最高のグルーパーモデルが、ほとんどの人間のグルーパーよりも正確であることに気付きました。
論文 参考訳(メタデータ) (2024-06-11T15:30:26Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳(メタデータ) (2024-02-14T05:57:58Z) - On Exams with the Isabelle Proof Assistant [0.0]
本稿では,Isabelle証明アシスタントを用いた自動推論のコースにおいて,学生の学習結果をテストするためのアプローチを提案する。
このアプローチにより、様々な論理的証明システムにおける形式的証明の一般的な理解と、イザベル/HOLの高階論理における証明の理解の両方をテストすることができる。
論文 参考訳(メタデータ) (2023-03-10T11:37:09Z) - Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal
Proofs [30.57062828812679]
本稿では,形式的証明スケッチに非公式な証明をマッピングするDraft, Sketch, Prove(DSP)を紹介する。
大規模言語モデルでは,形式的証明と同じ推論手順を踏襲して,構造化された形式的スケッチを作成可能であることを示す。
論文 参考訳(メタデータ) (2022-10-21T22:37:22Z) - Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。
NLProofSは仮説に基づいて関連するステップを生成することを学習する。
EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文 参考訳(メタデータ) (2022-05-25T02:22:30Z) - Natural Language Specifications in Proof Assistants [0.0]
既存の証明アシスタント内で自然言語仕様のサポートを構築することができる。
本稿では,既存の証明アシスタント内で自然言語仕様のサポートを構築することが可能であることを論じる。
論文 参考訳(メタデータ) (2022-05-16T17:05:45Z) - Formal Mathematics Statement Curriculum Learning [64.45821687940946]
同じ計算予算、専門家の反復、つまり、学習にインターリーブされた証明検索が、証明検索のみを劇的に上回っていることを示す。
また, 難易度が十分に異なる形式文の集合に適用した場合, 専門家の反復により, ますます困難な問題に対するカリキュラムの発見と解決が可能であることも観察した。
論文 参考訳(メタデータ) (2022-02-03T00:17:00Z) - DialFact: A Benchmark for Fact-Checking in Dialogue [56.63709206232572]
われわれはDialFactという22,245の注釈付き会話クレームのベンチマークデータセットを構築し、ウィキペディアの証拠と組み合わせた。
FEVERのような非対話データでトレーニングされた既存のファクトチェックモデルは、我々のタスクでうまく機能しないことがわかった。
本稿では,対話におけるファクトチェック性能を効果的に向上する,シンプルなデータ効率のソリューションを提案する。
論文 参考訳(メタデータ) (2021-10-15T17:34:35Z) - Proof Blocks: Autogradable Scaffolding Activities for Learning to Write
Proofs [0.4588028371034407]
Proof Blocksは、学生が事前に書かれた証明行を正しい順序にドラッグ&ドロップすることで、証明を書くことができるソフトウェアツールである。
これらの証明は完全に自動的に評価され、学生は自分の証明で何をしているのかを素早くフィードバックすることができる。
問題を構築する際、インストラクターは証明の行の依存性グラフを指定し、行の正しい配置をフルクレジットで受け取れるようにする。
論文 参考訳(メタデータ) (2021-06-07T17:03:58Z) - Conversations with Documents. An Exploration of Document-Centered
Assistance [55.60379539074692]
例えば、個人が文書をすばやくレビューするのを助けるドキュメント中心の支援は、あまり進歩していない。
我々は,文書中心の支援の空間と,人々がこのシナリオで期待する能力を理解するための調査を行う。
a) 文書中心の質問を正確に検出でき、(b) そうした質問に答えるために合理的に正確なモデルを構築することができることを示す。
論文 参考訳(メタデータ) (2020-01-27T17:10:11Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。