Fugu-MT 論文翻訳(概要): Using Automated Theorem Provers for Mistake Diagnosis in the Didactics of Mathematics

論文の概要: Using Automated Theorem Provers for Mistake Diagnosis in the Didactics of Mathematics

arxiv url: http://arxiv.org/abs/2002.05083v1
Date: Wed, 12 Feb 2020 16:36:59 GMT
ステータス: 処理完了
システム内更新日: 2023-01-01 20:22:12.036791
Title: Using Automated Theorem Provers for Mistake Diagnosis in the Didactics of Mathematics
Title（参考訳）: 数学教育における誤用診断のための自動定理証明器
Authors: Merlin Carl
Abstract要約: Diproche システムは、Koepke や Schr"oder 、 Cramer などによる Naproche システムに似た初心者学生の運動の文脈に特化している。本稿では,このようなアンチATPの概念を簡潔に解説し,その実装における基本技術について解説する。
参考スコア（独自算出の注目度）: 0.0
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: The Diproche system, an automated proof checker for natural language proofs specifically adapted to the context of exercises for beginner's students similar to the Naproche system by Koepke, Schr\"oder, Cramer and others, uses a modification of an automated theorem prover which uses common formal fallacies intead of sound deduction rules for mistake diagnosis. We briefly describe the concept of such an `Anti-ATP' and explain the basic techniques used in its implementation.
Abstract（参考訳）: Diprocheシステム(英語版)は、Koepke, Schr\oder, Cramerらによる初心者学生の運動の文脈に特化して適応した自然言語証明のための自動証明チェッカーであり、誤り診断に一般的な形式的推論規則の誤用を用いた自動定理証明器の修正を使用している。このような「アンチATP」の概念を簡潔に説明し、その実装における基本技術について説明する。

関連論文リスト

TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
論文参考訳（メタデータ） (2023-10-16T08:42:39Z)
A Hybrid System for Systematic Generalization in Simple Arithmetic Problems [70.91780996370326]
本稿では,記号列に対する合成的および体系的推論を必要とする算術的問題を解くことができるハイブリッドシステムを提案する。提案システムは,最も単純なケースを含むサブセットでのみ訓練された場合においても,ネストした数式を正確に解くことができることを示す。
論文参考訳（メタデータ） (2023-06-29T18:35:41Z)
A Rule Based Theorem Prover: an Introduction to Proofs in Secondary Schools [0.0]
中学校における自動推論システムの導入は、いくつかのボトルネックに直面している。幾何学的自動定理プローバーの結果と学校での推論と証明の通常の実践との間の不一致は、教育環境においてそのようなツールを広く使用する上で大きな障壁となる。授業計画が提示され、その目標は幾何学的定理を証明する公式なデモンストレーションの導入であり、その目標に学生を動機付けようとすることである。
論文参考訳（メタデータ） (2023-03-10T11:36:10Z)
Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI [60.142926537264714]
本稿では, 忠実度スルー・カウンタファクトの方法論について紹介する。これは、説明に表される論理述語に基づいて、反実仮説を生成する。そして、そのモデルが表現された論理と反ファクトの予測が一致しているかどうかを評価する。
論文参考訳（メタデータ） (2022-05-25T03:40:59Z)
Learning Symbolic Rules for Reasoning in Quasi-Natural Language [74.96601852906328]
我々は,ルールを手作業で構築することなく,自然言語入力で推論できるルールベースシステムを構築した。本稿では,形式論理文と自然言語文の両方を表現可能な"Quasi-Natural"言語であるMetaQNLを提案する。提案手法は,複数の推論ベンチマークにおける最先端の精度を実現する。
論文参考訳（メタデータ） (2021-11-23T17:49:00Z)
Refining Labelled Systems for Modal and Constructive Logics with Applications [0.0]
この論文は、モーダル論理や構成論理のセマンティクスを「経済的な」証明システムに変換する手段として機能する。精製法は、ラベル付きおよびネストされたシーケント計算の2つの証明理論パラダイムを結合する。導入された洗練されたラベル付き電卓は、デオン性STIT論理に対する最初の証明探索アルゴリズムを提供するために使用される。
論文参考訳（メタデータ） (2021-07-30T08:27:15Z)
Neural Proof Nets [0.8379286663107844]
本稿では,Sinkhorn ネットワークをベースとした証明ネットのニューラルバリアントを提案する。 AEThelでは,テキスト文の正しい書き起こしを線形ラムダ計算の証明や用語として70%の精度で行うことができる。
論文参考訳（メタデータ） (2020-09-26T22:48:47Z)
Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文参考訳（メタデータ） (2020-09-07T19:50:10Z)
Verification of ML Systems via Reparameterization [6.482926592121413]
確率的プログラムを定理証明器で自動的に表現する方法を示す。また、ベイズ仮説テストで用いられるヌルモデルは、人口統計学的パリティ(英語版)と呼ばれる公平性基準を満たすことを証明した。
論文参考訳（メタデータ） (2020-07-14T02:19:25Z)
Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文参考訳（メタデータ） (2020-02-17T16:06:02Z)

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