Fugu-MT 論文翻訳(概要): Automatized Evaluation of Formalization Exercises in Mathematics

論文の概要: Automatized Evaluation of Formalization Exercises in Mathematics

arxiv url: http://arxiv.org/abs/2006.01800v2
Date: Thu, 9 Jul 2020 16:28:54 GMT
ステータス: 処理完了
システム内更新日: 2022-11-26 00:46:51.771935
Title: Automatized Evaluation of Formalization Exercises in Mathematics
Title（参考訳）: 数学における形式化演習の自動評価
Authors: Merlin Carl
Abstract要約: 本稿では,初級述語論理の形式的記述における基礎的スキル獲得を支援する2つのシステムについて述べる。第1は"math dictations"と呼ばれ、与えられた自然言語文を形式化するタスクをユーザに提示するが、第2は"Game of Def"と呼ばれ、ユーザに対して幾何学的パターンの集合を形式的に記述するよう要求する。
参考スコア（独自算出の注目度）: 0.0
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: We describe two systems for supporting beginner students in acquiring basic skills in expressing statements in the formalism of first-order predicate logic; the first, called "math dictations", presents users with the task of formalizing a given natural-language sentence, while the second, called "Game of Def", challenges users to give a formal description of a set of a geometric pattern displayed to them. In both cases, an automatic checking takes place.
Abstract（参考訳）: 初級述語論理の形式化における文の表現における基礎的スキルの獲得を支援する2つのシステムについて述べる。第1のシステムは「数学ディクテーション」と呼ばれ、ユーザに与えられた自然言語文の形式化タスクを与え、第2のシステムは「defのゲーム」と呼ばれ、ユーザに表示された幾何学的パターンの組の形式的記述を与える。どちらの場合でも自動チェックが行われる。

関連論文リスト

LLM Critics Help Catch Bugs in Mathematics: Towards a Better Mathematical Verifier with Natural Language Feedback [71.95402654982095]
本研究では,自然言語フィードバック型検証器Math-Minosを提案する。実験の結果,少量の自然言語フィードバックが検証器の性能を大幅に向上させることがわかった。
論文参考訳（メタデータ） (2024-06-20T06:42:27Z)
A Hybrid System for Systematic Generalization in Simple Arithmetic Problems [70.91780996370326]
本稿では,記号列に対する合成的および体系的推論を必要とする算術的問題を解くことができるハイブリッドシステムを提案する。提案システムは,最も単純なケースを含むサブセットでのみ訓練された場合においても,ネストした数式を正確に解くことができることを示す。
論文参考訳（メタデータ） (2023-06-29T18:35:41Z)
Using Large Language Models for (De-)Formalization and Natural Argumentation Exercises for Beginner's Students [0.0]
現在開発中の2つのシステムは、自然言語と命題論理と一階述語論理の言語を相互に翻訳する際の(i)エクササイズの自動修正に大規模な言語モデルを使用している。
論文参考訳（メタデータ） (2023-04-12T23:05:02Z)
Hierarchical Phrase-based Sequence-to-Sequence Learning [94.10257313923478]
本稿では、学習中の帰納バイアスの源として階層的フレーズを取り入れ、推論中の明示的な制約として、標準的なシーケンス・ツー・シーケンス(seq2seq)モデルの柔軟性を維持するニューラルトランスデューサについて述べる。本手法では,木が原文と対象句を階層的に整列するブラケット文法に基づく識別的導出法と,整列した句を1対1で翻訳するニューラルネットワークセク2セックモデルという2つのモデルを訓練する。
論文参考訳（メタデータ） (2022-11-15T05:22:40Z)
Formal Mathematics Statement Curriculum Learning [64.45821687940946]
同じ計算予算、専門家の反復、つまり、学習にインターリーブされた証明検索が、証明検索のみを劇的に上回っていることを示す。また, 難易度が十分に異なる形式文の集合に適用した場合, 専門家の反復により, ますます困難な問題に対するカリキュラムの発見と解決が可能であることも観察した。
論文参考訳（メタデータ） (2022-02-03T00:17:00Z)
Applying Second-Order Quantifier Elimination in Inspecting G\"odel's Ontological Proof [0.0]
フォーミュラマクロは複雑な公式やタスクを構成するのに使用される。 G"odelの存在論的証明とバリエーションは形式化され、自動ツールで分析される。
論文参考訳（メタデータ） (2021-10-21T12:50:23Z)
Refining Labelled Systems for Modal and Constructive Logics with Applications [0.0]
この論文は、モーダル論理や構成論理のセマンティクスを「経済的な」証明システムに変換する手段として機能する。精製法は、ラベル付きおよびネストされたシーケント計算の2つの証明理論パラダイムを結合する。導入された洗練されたラベル付き電卓は、デオン性STIT論理に対する最初の証明探索アルゴリズムを提供するために使用される。
論文参考訳（メタデータ） (2021-07-30T08:27:15Z)
Compositional Generalization via Semantic Tagging [81.24269148865555]
本稿では,シーケンス・ツー・シーケンスモデルの表現性と一般性を保存するための新しいデコードフレームワークを提案する。提案手法は, モデルアーキテクチャ, ドメイン, セマンティックフォーマリズム間の構成一般化を一貫して改善することを示す。
論文参考訳（メタデータ） (2020-10-22T15:55:15Z)
Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文参考訳（メタデータ） (2020-09-07T19:50:10Z)
Using Automated Theorem Provers for Mistake Diagnosis in the Didactics of Mathematics [0.0]
Diproche システムは、Koepke や Schr"oder 、 Cramer などによる Naproche システムに似た初心者学生の運動の文脈に特化している。本稿では,このようなアンチATPの概念を簡潔に解説し,その実装における基本技術について解説する。
論文参考訳（メタデータ） (2020-02-12T16:36:59Z)

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