論文の概要: Automating the Generation of High School Geometry Proofs using Prolog in an Educational Context

• arxiv url: http://arxiv.org/abs/2002.12551v1
• Date: Fri, 28 Feb 2020 05:23:16 GMT
• ステータス: 処理完了
• システム内更新日: 2022-12-28 02:39:18.893972
• Title: Automating the Generation of High School Geometry Proofs using Prolog in an Educational Context
• Title（参考訳）: Prologを用いた高等学校幾何学証明生成の教育文脈における自動化
• Authors: Ludovic Font (\'Ecole Polytechnique de Montr\'eal), S\'ebastien Cyr (Universit\'e de Montr\'eal), Philippe R. Richard (Universit\'e de Montr\'eal), Michel Gagnon (\'Ecole Polytechnique de Montr\'eal)
• Abstract要約: 我々は、Prologのエンコーディングから証明の完全なセットの生成に至るまで、我々が実装した中核的な概念を提示する。 また、私たちが直面した主な問題と、選択したソリューションも提示します。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: When working on intelligent tutor systems designed for mathematics education and its specificities, an interesting objective is to provide relevant help to the students by anticipating their next steps. This can only be done by knowing, beforehand, the possible ways to solve a problem. Hence the need for an automated theorem prover that provide proofs as they would be written by a student. To achieve this objective, logic programming is a natural tool due to the similarity of its reasoning with a mathematical proof by inference. In this paper, we present the core ideas we used to implement such a prover, from its encoding in Prolog to the generation of the complete set of proofs. However, when dealing with educational aspects, there are many challenges to overcome. We also present the main issues we encountered, as well as the chosen solutions.
• Abstract（参考訳）: 数学教育とその特異性のために設計されたインテリジェントチューターシステムに取り組む場合,次のステップを期待して,学生に適切な支援を提供することが興味深い。 これは、事前に、問題の解決可能な方法を知ることでのみ実現できる。 したがって、学生が書くような証明を提供する自動定理証明器が必要である。 この目的を達成するために、論理プログラミングは推論による数学的証明との推論の類似性から自然なツールである。 本稿では, prolog のエンコーディングから証明の完全集合の生成まで,このような証明器の実装に用いた基本概念について述べる。 しかし、教育的側面を扱う際には克服すべき課題が数多くある。 また、私たちが遭遇した主な問題や選択した解決策も提示します。

関連論文リスト

• Artifical intelligence and inherent mathematical difficulty [0.0]
  まず、計算可能性と複雑性理論による制限的な結果が証明発見が本質的に難しい問題であることを示す従来の議論の更新版を提示する。 次に、人工知能にインスパイアされた最近のいくつかの応用が、数学的な証明の性質に関する新しい疑問を実際に提起する方法について説明する。
  論文  参考訳（メタデータ） (2024-08-01T20:08:31Z)
• Learning Formal Mathematics From Intrinsic Motivation [34.986025832497255]
  ミニモ(Minimo)は、自分自身に問題を起こし、それを解決することを学ぶエージェント(理論実証)である。 制約付き復号法と型指向合成法を組み合わせて、言語モデルから有効な予想をサンプリングする。 我々のエージェントは、ハードだが証明可能な予想を生成することを目標としています。
  論文  参考訳（メタデータ） (2024-06-30T13:34:54Z)
• Autoformalizing Euclidean Geometry [74.72212706513318]
  ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。 1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。 自己形式化定理文の自動意味評価を行う。
  論文  参考訳（メタデータ） (2024-05-27T14:35:10Z)
• Automatic question generation for propositional logical equivalences [6.221146613622175]
  そこで我々は,各学生に対して適切な質問を生成できる手法を開発し,実装する。 従来の研究では、妥当性、ユーザ定義の困難さ、パーソナライズされた問題生成を含む、教育におけるAQGフレームワークについて研究されてきた。 我々の新しいAQGアプローチは、一年生のコンピュータサイエンス学生にとってコアコースである離散数学に論理的等価性問題をもたらす。
  論文  参考訳（メタデータ） (2024-05-09T02:44:42Z)
• Learning Guided Automated Reasoning: A Brief Survey [5.607616497275423]
  これまでに開発されてきたいくつかの自動推論・定理証明領域と学習・AI手法の概要について概説する。 これには、前提選択、いくつかの設定での証明ガイダンス、推論と学習を繰り返すフィードバックループ、象徴的な分類問題が含まれる。
  論文  参考訳（メタデータ） (2024-03-06T19:59:17Z)
• A Rule Based Theorem Prover: an Introduction to Proofs in Secondary Schools [0.0]
  中学校における自動推論システムの導入は、いくつかのボトルネックに直面している。 幾何学的自動定理プローバーの結果と学校での推論と証明の通常の実践との間の不一致は、教育環境においてそのようなツールを広く使用する上で大きな障壁となる。 授業計画が提示され、その目標は幾何学的定理を証明する公式なデモンストレーションの導入であり、その目標に学生を動機付けようとすることである。
  論文  参考訳（メタデータ） (2023-03-10T11:36:10Z)
• UniGeo: Unifying Geometry Logical Reasoning via Reformulating Mathematical Expression [127.68780714438103]
  計算と証明の2つの主要な幾何学問題は、通常2つの特定のタスクとして扱われる。 我々は4,998の計算問題と9,543の証明問題を含むUniGeoという大規模統一幾何問題ベンチマークを構築した。 また,複数タスクの幾何変換フレームワークであるGeoformerを提案し,計算と証明を同時に行う。
  論文  参考訳（メタデータ） (2022-12-06T04:37:51Z)
• NaturalProver: Grounded Mathematical Proof Generation with Language Models [84.2064569475095]
  自然数理言語における定理証明は、数学の進歩と教育において中心的な役割を果たす。 本研究では,背景参照を条件づけて証明を生成する言語モデルであるNaturalProverを開発する。 NaturalProverは、短い(2-6ステップ)証明を必要とするいくつかの定理を証明でき、40%の時間で正しいと評価された次のステップの提案を提供することができる。
  論文  参考訳（メタデータ） (2022-05-25T17:01:18Z)
• NaturalProofs: Mathematical Theorem Proving in Natural Language [132.99913141409968]
  数学的ステートメントの多領域コーパスであるNaturalProofsとその証明を開発した。 NaturalProofsは広範なカバレッジ、深いカバレッジ、低リソースの数学的ソースを統一する。 数式参照検索と生成タスクに関する強力なニューラルネットワーク手法をベンチマークする。
  論文  参考訳（メタデータ） (2021-03-24T03:14:48Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。 実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
  論文  参考訳（メタデータ） (2020-02-17T16:06:02Z)

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

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