論文の概要: Hazel Prover: A Classroom Proof Assistant for Learning Structural Induction
- arxiv url: http://arxiv.org/abs/2608.23309v1
- Date: Mon, 24 Aug 2026 14:29:41 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-25 13:29:44.152646
- Title: Hazel Prover: A Classroom Proof Assistant for Learning Structural Induction
- Title（参考訳）: Hazel Prover: 構造的誘導を学習するためのクラスルーム証明アシスタント
- Abstract要約: Hazel Proverは、方程式と帰納的推論を教えるための教室証明アシスタントである。
本稿では,ツールの使いやすさ,基礎となる数学的アイデアへの学生の関与,ペン・アンド・ペーパーの証明への移転,教室のロジスティクスといった基準に照らした設計を提案する。
分析の結果,学生はツールを効果的に活用できるようになり,課題の進行とともに帰納的証明の能力も向上した。
- 参考スコア（独自算出の注目度）: 0.7733046964560364
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Proof assistants offer instant feedback and incremental proof scaffolding to users. Both of these features have long held promise in improving mathematics education in classroom settings, where manual grading is costly, and students often struggle with knowing how to proceed in their proof. However, they have been difficult to deploy in classroom settings due to two main concerns: (i) students struggle with the intricacies of full-scale proof assistants; and (ii) proof assistants are ineffective in support of student learning, and knowledge transfer to on-paper assessments without the tool. We present Hazel Prover, a classroom proof assistant for teaching equational and inductive reasoning, with a design informed by criteria encompassing ease-of-use of the tool, student engagement with underlying mathematical ideas, transfer to pen-and-paper proof, and classroom logistics. We synthesized these criteria from observations made in prior deployments of proof assistants to the classroom. We engaged in an iterative design and evaluation process, deploying Hazel Prover in two different classes and conducting in-depth analyses of fine-grained usage logs, survey data, and student exam responses. Our analysis demonstrates that students were able to learn to use the tool effectively, and that students became more capable with inductive proof as they progressed through problems. However, the first design did not effectively achieve transfer to pen-and-paper proofs. We hypothesized that this was due to the tool offering too much help to students in the equational reasoning steps. Based on this negative result, we enforced more manual student engagement with equational steps, which led to more effective transfer in the second deployment. We believe that our analyses offer generalizable insights relevant to the designers of future classroom proof assistants for a variety of mathematical domains.
- Abstract（参考訳）: Proofアシスタントは、即時フィードバックとインクリメンタルな証明の足場をユーザに提供します。
これら2つの機能は、手動のグルーピングが高価である教室環境での数学教育の改善に長年にわたって期待されており、学生は証明の進め方を知るのに苦労することが多い。
しかし,2つの主要な懸念から,教室環境での展開は困難であった。
一 学生が実力証明助手の複雑さに苦しむこと。
二 証明アシスタントは、学生の学習を支援するのに効果がなく、そのツールを使わずに、紙上での評価に知識を伝達する。
本稿では,方程式的および帰納的推論を指導するための教室証明アシスタントであるHazel Proverを紹介し,ツールの使いやすさ,基礎となる数学的アイデアへの学生の関与,ペン・アンド・ペーパーの証明への移動,教室のロジスティクスといった基準を取り入れた設計を提示する。
本研究では,これらの基準を,教室への証明助手の事前配備時の観察結果から合成した。
本研究では,2つのクラスにHazel Proverを配置し,詳細な使用ログ,調査データ,学生試験結果の詳細な分析を行った。
分析の結果,学生はツールを効果的に活用することができ,課題の進行とともに帰納的証明の能力も向上した。
しかし、最初の設計はペンと紙の証明への移転を効果的に達成しなかった。
これは、方程式推論ステップの学生に過剰な支援を提供するツールが原因である、という仮説を立てた。
この否定的な結果に基づいて、より手動の学生参加を方程式的なステップで実施し、第2のデプロイメントにおいてより効果的な移行を実現した。
この分析は、将来の数学分野における教室証明アシスタントの設計者に対して、一般化可能な洞察を与えるものであると信じている。
関連論文リスト
- AgentBrew: Lifelong Knowledge Brewing from Strong Teachers to Weak LLM Agents [8.847692192802343]
LLMエージェントは通常、訓練中により強い教師が利用できる場合でも、コンパクトなテストタイムの学生を必要とします。
この設定には2つの課題がある: 環境はスパースのみを提供し、二進的なフィードバックを提供し、教師によって書かれたノートは、実質的に、より弱い学生によって具体的に実行可能なように調整されなければならない。
本稿では,2つの複合コンポーネントからなるエージェントブリューを提案する。まず,学生の失敗を環境に配慮したノートに変換することで,学習者からのフィードバックを緩やかにする。
第二に、学生認識合成は教師の知識を弱い実行者の操作的粒度に分類し、モデル固有で行動可能な指導を与える。
論文 参考訳（メタデータ） (2026-07-18T15:23:45Z) - Alice: Proactive Learning with Teacher's Demonstrations for Weak-to-Strong Generalization [69.96794098855938]
Weak-to-strong Generalization (W2SG)は、ますます有能な言語モデル(LLM)を監督するための有望なフレームワークを提供する。
伝統的なW2SG手法は受動的学習に依存しており、弱い教師は強い生徒を訓練するためにノイズの多いデモを提供する。
教師と生徒の相補的な知識を活用して学習プロセスを強化するフレームワークであるAliceを紹介した。
論文 参考訳（メタデータ） (2025-04-09T22:33:06Z) - LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
証明の進捗を予測する手法であるLeanProgressを紹介します。
実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
論文 参考訳（メタデータ） (2025-02-25T07:46:36Z) - Autograding Mathematical Induction Proofs with Natural Language Processing [0.12289361708127876]
本稿では,自由形式の数学的証明を自動分解できる一連のトレーニング手法とモデルを提案する。
モデルは、誘導問題によって4つの異なる証明から収集された証明データを用いて訓練される。
我々は、トレーニングデータと同じ証明を格付けするために、人間のグルーパーを雇い、最高のグルーパーモデルが、ほとんどの人間のグルーパーよりも正確であることに気付きました。
論文 参考訳（メタデータ） (2024-06-11T15:30:26Z) - Representational Alignment Supports Effective Machine Teaching [81.19197059407121]
GRADEは、教育と表現的アライメントを研究するための新しい制御された実験環境である。
学生との表現的整合性が向上し,生徒の学習成果が向上することがわかった。
しかし、この効果は、教えられているクラスのサイズと表現の多様性によって中和される。
論文 参考訳（メタデータ） (2024-06-06T17:48:24Z) - ProofBuddy: A Proof Assistant for Learning and Monitoring [0.0]
証明能力(Proof competence)、すなわち、(数学的な)証明を書き、チェックする能力は、コンピュータ科学において重要なスキルである。
主な問題は、形式言語の正しい使用と証明、特に学生自身の証明が完璧で正しいかどうかの確認である。
多くの著者は、証明能力を教えるのに証明アシスタントを使うことを提案したが、その方法の有効性は明らかではない。
デンマーク工科大学でProofBuddyのユーザビリティに関する予備的な研究を行った。
論文 参考訳（メタデータ） (2023-08-14T07:08:55Z) - Can Language Models Teach Weaker Agents? Teacher Explanations Improve
Students via Personalization [84.86241161706911]
教師のLLMは、実際に生徒の推論に介入し、パフォーマンスを向上させることができることを示す。
また,マルチターンインタラクションでは,教師による説明が一般化され,説明データから学習されることを示す。
教師のミスアライメントが学生の成績をランダムな確率に低下させることを、意図的に誤解させることで検証する。
論文 参考訳（メタデータ） (2023-06-15T17:27:20Z) - Distantly-Supervised Named Entity Recognition with Adaptive Teacher
Learning and Fine-grained Student Ensemble [56.705249154629264]
NERモデルの堅牢性を改善するために,自己学習型教員学生フレームワークを提案する。
本稿では,2つの教員ネットワークからなる適応型教員学習を提案する。
微粒な学生アンサンブルは、教師モデルの各フラグメントを、生徒の対応するフラグメントの時間移動平均で更新し、各モデルフラグメントのノイズに対する一貫した予測を強化する。
論文 参考訳（メタデータ） (2022-12-13T12:14:09Z) - Computationally Identifying Funneling and Focusing Questions in
Classroom Discourse [24.279653100481863]
本稿では,授業談話におけるファネリングと集中型質問を計算的に検出するタスクを提案する。
ファネリングと集中型質問にラベル付けされた2,348の教師発話の注釈付きデータセットをリリースする。
我々の最高のモデルである教師付きRoBERTaモデルは、データセットに微調整され、人間の専門家ラベルと.76の強い線形相関と、ポジティブな教育結果を持つ。
論文 参考訳（メタデータ） (2022-07-08T01:28:29Z) - ProtoTransformer: A Meta-Learning Approach to Providing Student Feedback [54.142719510638614]
本稿では,フィードバックを数発の分類として提供するという課題について考察する。
メタラーナーは、インストラクターによるいくつかの例から、新しいプログラミング質問に関する学生のコードにフィードバックを与えるように適応します。
本手法は,第1段階の大学が提供したプログラムコースにおいて,16,000名の学生試験ソリューションに対するフィードバックの提供に成功している。
論文 参考訳（メタデータ） (2021-07-23T22:41:28Z) - Proof Blocks: Autogradable Scaffolding Activities for Learning to Write
Proofs [0.4588028371034407]
Proof Blocksは、学生が事前に書かれた証明行を正しい順序にドラッグ&ドロップすることで、証明を書くことができるソフトウェアツールである。
これらの証明は完全に自動的に評価され、学生は自分の証明で何をしているのかを素早くフィードバックすることができる。
問題を構築する際、インストラクターは証明の行の依存性グラフを指定し、行の正しい配置をフルクレジットで受け取れるようにする。
論文 参考訳（メタデータ） (2021-06-07T17:03:58Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。