論文の概要: Teaching Simple Constructive Proofs with Haskell Programs

• arxiv url: http://arxiv.org/abs/2208.04699v1
• Date: Tue, 26 Jul 2022 07:46:58 GMT
• ステータス: 処理完了
• システム内更新日: 2023-02-19 10:25:52.849005
• Title: Teaching Simple Constructive Proofs with Haskell Programs
• Title（参考訳）: Haskellプログラムで簡単な構成証明を教える
• Authors: Matthew Farrugia-Roberts (The University of Melbourne), Bryn Jeffries (Grok Academy), Harald S{\o}ndergaard (The University of Melbourne)
• Abstract要約: 我々は、大卒の大学コースで、従来の数学的フォーマリズムとともにHaskellの使用について検討してきた。 インタラクティブな学習プラットフォームを通じて,ほぼすべての形式的かつ要約的な評価を提供することが可能であることが分かりました。 この形式に変換するのに最も難しい課題の1つは、建設的な議論を伝達する伝統的に書かれた証明である。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: In recent years we have explored using Haskell alongside a traditional mathematical formalism in our large-enrolment university course on topics including logic and formal languages, aiming to offer our students a programming perspective on these mathematical topics. We have found it possible to offer almost all formative and summative assessment through an interactive learning platform, using Haskell as a lingua franca for digital exercises across our broad syllabus. One of the hardest exercises to convert into this format are traditional written proofs conveying constructive arguments. In this paper we reflect on the digitisation of this kind of exercise. We share many examples of Haskell exercises designed to target similar skills to written proof exercises across topics in propositional logic and formal languages, discussing various aspects of the design of such exercises. We also catalogue a sample of student responses to such exercises. This discussion contributes to our broader exploration of programming problems as a flexible digital medium for learning and assessment.
• Abstract（参考訳）: 近年私たちは,論理学や形式言語といった話題について,従来の数学的形式主義と並行してhaskellの利用を探求し,これらの数学的トピックに対するプログラミング的視点を提供することを目的としています。 私たちはHaskellを広範囲にわたるデジタルエクササイズのためのラングアフランカとして使用して,インタラクティブな学習プラットフォームを通じて,ほぼすべての形式的かつ要約的なアセスメントを提供することが可能であることに気付きました。 この形式に変換する最も難しい課題の1つは、コンストラクティブな議論を伝える従来の証明である。 本稿では,この種の運動のデジタル化について考察する。 我々は、命題論理や形式言語におけるトピックにまたがる証明演習と同じようなスキルを目標に設計されたHaskellのエクササイズの例を共有し、そのようなエクササイズの設計のさまざまな側面について議論する。 このようなエクササイズに対する学生の反応のサンプルもカタログ化しています。 この議論は、学習と評価のためのフレキシブルなデジタル媒体としてのプログラミング問題の広範な探求に寄与します。

関連論文リスト

• Teaching Type Systems Implementation with Stella, an Extensible Statically Typed Programming Language [0.0]
  このコースは、古典的なコンパイラ構築の基礎、特に抽象構文表現、ビジターパターン、構文解析を前提としている。 このコースは、最小限のコアと小さな拡張セットを備えた言語Stellaを中心に構築されている。
  論文  参考訳（メタデータ） (2024-07-10T23:27:21Z)
• Beyond the Hype: A Cautionary Tale of ChatGPT in the Programming Classroom [0.0]
  本論文は、より困難な演習を創出するためにプログラミングを教える学者や、教室の整合性を促進するためにChatGPTの使用に責任を負う方法についての知見を提供する。 過去のIS演習の実践的プログラミング事例を分析し,教員や講師が大学環境下で作成したメモと比較した。
  論文  参考訳（メタデータ） (2024-06-16T23:52:37Z)
• Lean Workbook: A large-scale Lean problem set formalized from natural language math problems [50.22847430754973]
  大規模な言語モデルは、リーンのような形式言語を使って証明する数学の定理が得意ではありません。 この領域で重要な課題は、これらの形式言語で利用可能なトレーニングデータの不足である。 本稿では,自然言語の数学的問題をリーン4文に変換するために,合成データを反復的に生成・フィルタリングするパイプラインを提案する。
  論文  参考訳（メタデータ） (2024-06-06T08:25:43Z)
• Investigating the Performance of Language Models for Completing Code in Functional Programming Languages: a Haskell Case Study [2.792812922172466]
  関数型プログラミング言語Haskell上で、コードのための2つの言語モデル、CodeGPTとUniXcoderを評価した。 HuggingFace上で公開されているHaskellデータセットから得られたHaskell関数のモデルを微調整し、評価する。 我々の自動評価では, LLMの事前学習における命令型プログラミング言語の知識は, 関数型言語にうまく移行しない可能性が示唆された。
  論文  参考訳（メタデータ） (2024-03-22T13:13:13Z)
• Large Language Models as Analogical Reasoners [155.9617224350088]
  CoT(Chain-of- Thought)は、言語モデルのプロンプトとして、推論タスク全体で素晴らしいパフォーマンスを示す。 そこで本稿では,大規模言語モデルの推論プロセスを自動的にガイドする,新たなプロンプト手法であるアナログプロンプトを導入する。
  論文  参考訳（メタデータ） (2023-10-03T00:57:26Z)
• Natural Language Embedded Programs for Hybrid Language Symbolic Reasoning [84.12154024070024]
  本研究では,数学・記号的推論,自然言語理解,後続の課題に対処するための統合フレームワークとして,自然言語組み込みプログラム(NLEP)を提案する。 我々のアプローチは,構造化知識の自然言語表現を含むデータ構造上の関数を定義する完全なPythonプログラムを生成するよう,言語モデルに促す。 Pythonインタープリタが生成されたコードを実行し、出力をプリントする。
  論文  参考訳（メタデータ） (2023-09-19T17:54:21Z)
• Enhancing Programming eTextbooks with ChatGPT Generated Counterfactual-Thinking-Inspired Questions [1.933681537640272]
  学生はプログラミングの教科書を最大限に活用するのに苦労している。 本研究は,知的教科書のナビゲート性を,対実的質問を用いて向上させるという考え方を探求するものである。
  論文  参考訳（メタデータ） (2023-06-01T11:14:15Z)
• Tree-Based Representation and Generation of Natural and Mathematical Language [77.34726150561087]
  科学コミュニケーションと教育シナリオにおける数学的言語は重要であるが、比較的研究されている。 数学言語に関する最近の研究は、スタンドアローンな数学的表現や、事前訓練された自然言語モデルにおける数学的推論に焦点をあてている。 テキストと数学を共同で表現・生成するために,既存の言語モデルに対する一連の修正を提案する。
  論文  参考訳（メタデータ） (2023-02-15T22:38:34Z)
• JiuZhang: A Chinese Pre-trained Language Model for Mathematical Problem Understanding [74.12405417718054]
  本稿では,中国初の数学的事前学習言語モデル(PLM)を提示することにより,機械の数学的知性向上を目指す。 他の標準のNLPタスクとは異なり、数学的テキストは問題文に数学的用語、記号、公式を含むため理解が難しい。 基礎課程と上級課程の両方からなる数学PLMの学習を改善するための新しいカリキュラム事前学習手法を設計する。
  論文  参考訳（メタデータ） (2022-06-13T17:03:52Z)
• Chain of Thought Prompting Elicits Reasoning in Large Language Models [56.811278668446825]
  本稿では,コヒーレントな思考連鎖を生成する言語モデルについて考察する。 実験により、プロンプトによって思考の連鎖を誘導することで、十分な大きな言語モデルが推論タスクをよりよく実行できるようになることが示されている。
  論文  参考訳（メタデータ） (2022-01-28T02:33:07Z)
• Prompt Programming for Large Language Models: Beyond the Few-Shot Paradigm [0.0]
  自然言語のレンズを通してプロンプトを考えることの有用性を強調しながら,プロンプトプログラミングの手法について論じる。 モデルに種を付けて、さまざまなタスクのための独自の自然言語プロンプトを生成するメタプロンプトのアイデアを紹介します。
  論文  参考訳（メタデータ） (2021-02-15T05:27:55Z)

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

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。