ProofBuddyの紹介：教育における証明能力の向上

証明能力、つまり数学的証明を書くことやチェックする能力は、コンピュータサイエンスにおいて重要なスキルなんだけど、多くの学生がこれを難しいと感じてるんだ。彼らが直面する主な問題は、形式的な言語を正しく使うことと、自分の証明が完全で正しいか確認すること。証明支援ツールを使ってこのスキルを教えることを提案する人もいるけど、その効果はまだはっきりしていないんだ。

そこで、私たちはProofBuddyというツールを紹介するよ。これはIsabelle証明支援ツールを使ったウェブベースのツールで、研究者が学生がそれを使う様子を詳しくデータとして集めて、教育における証明支援ツールの効果を調べることができるんだ。

私たちはデンマークの技術大学でProofBuddyの予備調査を行ったよ。コンピュータサイエンスの学士課程では、プログラミングやコンピュータに関する技術的スキル、理論的知識、数学が含まれていて、特に後の二つが学生にとって難しいことが多いんだ。コースは形式的な言語や論理、証明に重点を置いてる。学生は多くのコースで証明を書いて検証しなきゃいけないから、証明能力が必要で、それには4つの具体的なスキルが含まれてるんだ。

1. 専門的能力: これは作成する必要がある証明の文脈についての知識なんだ。
2. 表現能力: これは形式的な言語を使って証明を書くこと。
3. コミュニケーション能力: これは証明プロセスや解決策について話したり説明したりすること。
4. 方法論的能力: これは証明に使われる方法をまとめたもので、その構造や論理的結論の連鎖を含む。

これらのスキルは入門コースで教えられるけど、証明能力はカリキュラムの明確な目標になってることはほとんどないんだ。そのせいで、学生は講師が提示した証明を通して作業し、それを再現しようとすることが多いけど、残念ながら多くの学生がこの方法で苦労してるんだ。

ある研究では、調査者が入門コースの宿題や試験を分析したんだけど、証明に関する演習で学生が最も多くの間違いを犯すことがわかったよ。これは全体の成績とは関係なく発生したんだ。問題は主に形式的な言語の使用と、証明が正しいかどうかを評価することから来てるんだ。それが初歩的な証明コースでの高い失敗率につながってる。

証明支援ツールは証明能力の向上を図る手段として提案されてるよ。証明支援ツールは、関数型プログラミング言語の機能とプログラムに関する推論のためのツールを組み合わせたものなんだ。このセットアップで、ユーザーはより形式的に証明を書き、証明チェッカーからその正しさについて即座にフィードバックを受け取ることができる。

支持者たちは教育における証明支援ツールの多くの利点を強調してるけど、残念ながらこれらの主張には強い証拠が不足してることが多いんだ。批評家たちは、証明支援ツールを使って得たスキルが伝統的なペンと紙の証明にうまく移行しないかもしれないと懸念してる。彼らは、これらのツールが「 brute-force proving」を助長するかもしれないことを心配していて、つまり学生が成功するまで試し続けるだけで、証明がなぜ機能するのか理解しないかもしれないと懸念してる。また、証明支援ツールの導入によって貴重な授業時間が奪われるかもしれないともね。

この主張を調査するために、私たちはIsabelle証明支援ツールの拡張版であるProofBuddyを開発したよ。ProofBuddyの目的は、学生が証明支援ツールとどのように相互作用するかについての詳細なデータを集めて、研究者がさまざまな教育方法を研究するのを助けることなんだ。

私たちの初期評価では、ProofBuddyの使いやすさとそれが集めるデータの種類を調べたよ。私たちはこのデータが将来の研究が提起するかもしれない多くの質問に答えるのに十分だと考えてる。

全体的に、私たちはいくつかの貢献を提供するよ：

1. 教育における証明支援ツールの効果を評価する際の現在の課題の概要。
2. インタラクションデータを集めるIsabelle証明支援ツールのバージョンであるProofBuddyの紹介。
3. 学生の視点からのProofBuddyの使いやすさの初期評価。
4. ProofBuddyが集めたインタラクションデータが研究質問にどれだけ答えられるかの評価。

次に、教育における証明支援ツールの既存の使用方法について、その利点や欠点、ProofBuddyの設計に影響を与えた関数型プログラミングのツールを含めて議論するよ。また、観察された欠点に対処するための潜在的な方法と教育分野での証明支援ツールの使用の利点をさらに調査する方法についても概説するよ。

#関連研究

証明支援ツールを教育に使うことは新しいアイデアではないけど、これらの取り組みから得られた結果のほとんどは、効果の徹底的な評価ではなく経験報告なんだ。さまざまなアプローチの簡単な概要を提供するよ。

いくつかのコースは、さらに進んだ学習者を対象としていて、すでに証明能力や関数型プログラミングスキルを持っていることを前提にしてる。例えば、研究者たちはCoq証明支援ツールを使って証明能力を高めるために報告してる。学生たちはコースの後にCoqを使って定理を証明できるようになったけど、ペンと紙の証明を書く能力はわずかにしか向上しなかった。

他の研究では、証明支援ツールを1年目のコースに統合しようとしたものもある。ある試みでは、論理コースでLeanという証明支援ツールを使って数学的な証明と自然言語の証明を組み合わせたんだ。Leanは自発的なワークショップでは人気だったけど、必須ではなく、すでにコースでうまくやっている学生だけがそれを使うことを選んでいた。

ベルリン工科大学のいくつかのコースでは、学生が論理に取り組む演習でIsabelleを取り入れたけど、この使用はオプションだった。多くの学生はそれを楽しんでいたけど、時間がかかりすぎると感じていた。

他にも証明や論理を教えるために設計されたツールがある。例えばWaterproofは、ユーザーが自然言語と並行してCoq証明を書くことを可能にする。AProSプロジェクトもあり、インタラクティブな環境を用いて論理や証明を教えることに焦点を当てたコースやツールを開発しようとしている。

多くの証明支援ツールが存在し、一部は有望な結果を示しているけど、構造化された研究によって徹底的に検証されたものは少ないんだ。

#証明支援ツールの利点と欠点

証明支援ツールが教育に与える利点はよく文書化されていて、以下のようなものがあるよ：

• 数学を教えるのに役立つ。
• 関数型プログラミングを学ぶのに有用。
• 形式的な推論のルールを明確にする。
• 学生に証明の構造の仕方を教える。
• 証明の進捗に関する即時フィードバックを提供する。
• 学生が形式的な定義を参照し、それに取り組むことを奨励する。
• 学生が証明アイデアを試すのを助ける。
• 証明支援ツールでチェックされた課題の修正を簡略化する。

しかし、証明支援ツールを使う際に学生が直面する顕著な課題もあるよ。そのいくつかには：

• 構文を学ぶのが難しいこと。
• エラーメッセージが混乱を招くこと。
• 証明支援ツールから得たスキルがペンと紙の証明にうまく移行しないこと。
• インストールや使用中に技術的な問題が起こること。
• 一部の学生は形式的な証明ルールを覚えるのに苦労すること。

講師も証明支援ツールを導入するための時間が必要で、演習を設計することが課題になることもある。電子的なツールが課題の回避を容易にすることから、盗用についての懸念もあるんだ。

いくつかの著者は、証明支援ツールに関する主張に関して強固な証拠を提供することの問題を指摘しているよ。証明能力を定量的に測定する適切な方法がないため、学生がこれらのツールとどのように相互作用しているかに関する証拠を集めるのが難しいんだ。

#証明支援ツールを学びやすくする方法

証明支援ツールは一般的に専門的ユーザー向けに作られていて、初心者にとっては学習曲線が急になるんだ。形式的な言語は新しい学生には難易度が高いことがあるから、講師は言語を段階的に紹介して、学生が学ぶプロセスをガイドするツールを使うことでこの課題を軽減できるかもしれない。

学生はしばしばエラーメッセージが曖昧で混乱すると感じることがあるから、教育目的で証明支援ツールの言語を簡略化することが誤解を減らすのに役立つかもね。

技術的な問題も発生することがあるから、ウェブベースのプラットフォームはツールへのアクセスを容易にし、更新もしやすくするんだ。

#証拠を集める

教育における証明支援ツールに関する主要な課題の一つは、彼らが証明能力をどのように改善するかについての証拠が不足していることなんだ。証明支援ツールを使って作成されたコースがより良い成果をもたらすかどうかを理解することがまだ疑問で、一般的な証明能力を開発することが目標なのか、特にペンと紙の証明スキルを育成することが目標なのかを正確に指定することが重要だよ。

学生が証明支援ツールとどのように相互作用するかについての客観的かつ定量的なデータを集めることは、効果的な研究のために重要なんだ。ほとんどの報告は、学生に経験について尋ねるアンケートや、平均成績に基づく曖昧な指標に依存しているんだ。

#ProofBuddyの評価

私たちは、ProofBuddyを2つの観点から評価することを目指しているよ。研究者が教育的研究を行うのをどれだけ支援するかと、学生の視点からの使いやすさだね。

2023年春に、デンマークの技術大学で自動推論に関する上級コースで評価を行ったよ。このコースではIsabelleの使い方を学ぶことに重点を置いていた。私たちは、このコースの学生たちがペンと紙の証明を理解しているだろうと予想してたんだ。

参加者はProofBuddyを使って演習に取り組み、その後短いアンケートに答えたよ。評価の間、学生がツールとどのように相互作用するか観察し、講師への質問を記録したんだ。

学生たちはみんなProofBuddyを使って演習セッションをスタートしたよ。最初はインターフェースについて多くの質問をしていた。ほとんどの質問は論理演習に集中していて、プログラミングタスクを始めた学生もいたんだ。

セッション中に、証明作成の難しさやIsabelleと論理の構文の理解に関する問題を含む、さまざまなカテゴリに分類された質問を収集したよ。学生はProofBuddyに対して積極的に取り組んでいたけど、フィードバックの応答時間が遅いと感じる学生もいた。

使いやすさの問題にもかかわらず、データ収集機能は意図した通りに機能したよ。私たちはProofBuddyを利用する学生の行動を分析するために必要なデータをすべて集めることができたんだ。

#今後の作業

ProofBuddyを改善する計画があるよ。まず、フロントエンドでIsabelleの理論を評価することで応答時間を最適化し、文法エラーをチェックする前に捕まえることができるようにする予定なんだ。

また、学習目標をサポートするためにリンター、ドロップダウンメニュー、シンボルキーボードを追加の演習と連動させて、コース管理機能を拡張することも計画しているよ。

さらに、収集したデータを自動的に分析することを考えてる。これによって、学生がどのようなフィードバックを必要としているのか、どの証明分野で苦労しているのかをよりよく理解できるようになるんだ。

また、ベルリン工科大学での証明の作成と記述の教育に焦点を当てた新しいコースも開発中なんだ。このコースは、学生にリアルタイムでより多くのフィードバックを提供し、教材への関与を高め、理解を深めることを目指しているよ。

結論として、私たちはProofBuddyを紹介したんだ。これは学生の教育におけるIsabelleの使用を導き、監視するためのウェブベースのツールなんだ。Isabelleのような証明支援ツールは、関数型プログラムについての証明を書くのを簡単にしてくれる。ただ、教育的な影響を効果的に評価するためには、より厳密な研究が必要だよ。ProofBuddyは学生の相互作用に関するデータを収集するためのプラットフォームとして機能して、彼らの学習プロセスに関する貴重な洞察を提供し、教育者が指導を改善する方法を理解するのを助けるんだ。