Fugu-MT 論文翻訳(概要): On Exams with the Isabelle Proof Assistant

論文の概要: On Exams with the Isabelle Proof Assistant

arxiv url: http://arxiv.org/abs/2303.05866v1
Date: Fri, 10 Mar 2023 11:37:09 GMT
ステータス: 処理完了
システム内更新日: 2023-03-13 15:11:43.046670
Title: On Exams with the Isabelle Proof Assistant
Title（参考訳）: Isabelle Proof Assistantを用いた実験
Authors: Frederik Krogsdal Jacobsen (Technical University of Denmark), J{\o}rgen Villadsen (Technical University of Denmark)
Abstract要約: 本稿では,Isabelle証明アシスタントを用いた自動推論のコースにおいて,学生の学習結果をテストするためのアプローチを提案する。このアプローチにより、様々な論理的証明システムにおける形式的証明の一般的な理解と、イザベル/HOLの高階論理における証明の理解の両方をテストすることができる。
参考スコア（独自算出の注目度）: 0.0
License: http://creativecommons.org/licenses/by/4.0/
Abstract: We present an approach for testing student learning outcomes in a course on automated reasoning using the Isabelle proof assistant. The approach allows us to test both general understanding of formal proofs in various logical proof systems and understanding of proofs in the higher-order logic of Isabelle/HOL in particular. The use of Isabelle enables almost automatic grading of large parts of the exam. We explain our approach through a number of example problems, and explain why we believe that each of the kinds of problems we have selected are adequate measures of our intended learning outcomes. Finally, we discuss our experiences using the approach for the exam of a course on automated reasoning and suggest potential future work.
Abstract（参考訳）: 本稿では,Isabelle証明アシスタントを用いた自動推論のコースにおいて,学生の学習結果をテストするためのアプローチを提案する。このアプローチにより、様々な論理証明システムにおける形式的証明の一般的な理解と、特にイザベル/ホルの高階論理における証明の理解の両方をテストすることができる。イザベルの使用により、試験の大部分をほぼ自動的に段階付けすることができる。我々は,このアプローチをいくつかの事例問題を通じて説明し,選択した問題のそれぞれが意図した学習結果の適切な尺度であると考える理由を説明する。最後に, 自動推論試験におけるアプローチを用いた経験を考察し, 今後の課題を示唆する。

関連論文リスト

MathGAP: Out-of-Distribution Evaluation on Problems with Arbitrarily Complex Proofs [80.96119560172224]
大規模言語モデル(LLM)は、高い精度で算術語問題を解くことができるが、訓練された言語よりも複雑な問題にどのように一般化するかは、ほとんど分かっていない。本研究では、任意に複雑な算術証明問題に対する LLM の評価フレームワーク、MathGAP を提案する。
論文参考訳（メタデータ） (2024-10-17T12:48:14Z)
Prompt Optimization with EASE? Efficient Ordering-aware Automated Selection of Exemplars [66.823588073584]
大規模言語モデル(LLM)は、現実世界のアプリケーションで印象的な機能を示している。これらの卓越した作品の品質は、パフォーマンスに大きな影響を与えます。既存の方法は、先行注文がパフォーマンスに与える影響を適切に説明できない。
論文参考訳（メタデータ） (2024-05-25T08:23:05Z)
Automatic question generation for propositional logical equivalences [6.221146613622175]
そこで我々は,各学生に対して適切な質問を生成できる手法を開発し,実装する。従来の研究では、妥当性、ユーザ定義の困難さ、パーソナライズされた問題生成を含む、教育におけるAQGフレームワークについて研究されてきた。我々の新しいAQGアプローチは、一年生のコンピュータサイエンス学生にとってコアコースである離散数学に論理的等価性問題をもたらす。
論文参考訳（メタデータ） (2024-05-09T02:44:42Z)
Teaching Higher-Order Logic Using Isabelle [0.0]
我々はイザベル証明アシスタントにおいて高階論理の形式化を示す。これは、高階論理と証明アシスタントについて学ぼうとする人にとっては、良い紹介になるはずだ。
論文参考訳（メタデータ） (2024-04-08T12:40:27Z)
Learning Guided Automated Reasoning: A Brief Survey [5.607616497275423]
これまでに開発されてきたいくつかの自動推論・定理証明領域と学習・AI手法の概要について概説する。これには、前提選択、いくつかの設定での証明ガイダンス、推論と学習を繰り返すフィードバックループ、象徴的な分類問題が含まれる。
論文参考訳（メタデータ） (2024-03-06T19:59:17Z)
ProofBuddy: A Proof Assistant for Learning and Monitoring [0.0]
証明能力(Proof competence)、すなわち、(数学的な)証明を書き、チェックする能力は、コンピュータ科学において重要なスキルである。主な問題は、形式言語の正しい使用と証明、特に学生自身の証明が完璧で正しいかどうかの確認である。多くの著者は、証明能力を教えるのに証明アシスタントを使うことを提案したが、その方法の有効性は明らかではない。デンマーク工科大学でProofBuddyのユーザビリティに関する予備的な研究を行った。
論文参考訳（メタデータ） (2023-08-14T07:08:55Z)
UKP-SQuARE: An Interactive Tool for Teaching Question Answering [61.93372227117229]
質問応答の指数的増加(QA)は、あらゆる自然言語処理(NLP)コースにおいて必須のトピックとなっている。本稿では、QA教育のプラットフォームとしてUKP-SQuAREを紹介する。学生は様々な視点から様々なQAモデルを実行、比較、分析することができる。
論文参考訳（メタデータ） (2023-05-31T11:29:04Z)
elBERto: Self-supervised Commonsense Learning for Question Answering [131.51059870970616]
本稿では、市販QAモデルアーキテクチャと互換性のあるコモンセンスフレームワークの自己教師型双方向表現学習を提案する。このフレームワークは5つの自己教師型タスクから構成されており、リッチコモンセンスを含むコンテキストから追加のトレーニング信号を完全に活用するようモデルに強制する。 elBERtoは、単純な語彙的類似性比較が役に立たないような、アウト・オブ・パラグラフや非エフェクトな問題に対して、大幅に改善されている。
論文参考訳（メタデータ） (2022-03-17T16:23:45Z)
Formal Mathematics Statement Curriculum Learning [64.45821687940946]
同じ計算予算、専門家の反復、つまり、学習にインターリーブされた証明検索が、証明検索のみを劇的に上回っていることを示す。また, 難易度が十分に異なる形式文の集合に適用した場合, 専門家の反復により, ますます困難な問題に対するカリキュラムの発見と解決が可能であることも観察した。
論文参考訳（メタデータ） (2022-02-03T00:17:00Z)
Online Active Model Selection for Pre-trained Classifiers [72.84853880948894]
我々は,任意のラウンドにおいて高い確率で最良のモデルをラベル付けし,出力する情報的サンプルを積極的に選択するオンライン選択的サンプリング手法を設計する。我々のアルゴリズムは、敵とストリームの両方のオンライン予測タスクに利用できる。
論文参考訳（メタデータ） (2020-10-19T19:53:15Z)
Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description) [6.85316573653194]
そこで本研究では,400k以上の証明手法を応用したデータと,100以上の特徴を抽出したデータを含む,簡単なデータセットを提案する。我々の単純なデータフォーマットにより、機械学習の実践者は、論理学の専門知識を必要とせずに、機械学習ツールを使ってIsabelle/HOLの証明メソッドを予測できます。
論文参考訳（メタデータ） (2020-04-21T12:00:11Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。