論文の概要: Peano: Learning Formal Mathematical Reasoning

• arxiv url: http://arxiv.org/abs/2211.15864v1
• Date: Tue, 29 Nov 2022 01:42:26 GMT
• ステータス: 処理完了
• システム内更新日: 2022-11-30 16:14:01.562806
• Title: Peano: Learning Formal Mathematical Reasoning
• Title（参考訳）: Peano: フォーマルな数学的推論を学ぶ
• Authors: Gabriel Poesia and Noah D. Goodman
• Abstract要約: 一般的な数学的推論は計算不可能であるが、人間は新しい問題を常に解決している。 両パズルの中心は、数学の基礎となる手続き的抽象の構造であると仮定する。 カーン・アカデミー・プラットフォーム上の始点代数の5つの部分に関するケーススタディにおいて、このアイデアを探求する。
• 参考スコア（独自算出の注目度）: 35.086032962873226
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: General mathematical reasoning is computationally undecidable, but humans routinely solve new problems. Moreover, discoveries developed over centuries are taught to subsequent generations quickly. What structure enables this, and how might that inform automated mathematical reasoning? We posit that central to both puzzles is the structure of procedural abstractions underlying mathematics. We explore this idea in a case study on 5 sections of beginning algebra on the Khan Academy platform. To define a computational foundation, we introduce Peano, a theorem-proving environment where the set of valid actions at any point is finite. We use Peano to formalize introductory algebra problems and axioms, obtaining well-defined search problems. We observe existing reinforcement learning methods for symbolic reasoning to be insufficient to solve harder problems. Adding the ability to induce reusable abstractions ("tactics") from its own solutions allows an agent to make steady progress, solving all problems. Furthermore, these abstractions induce an order to the problems, seen at random during training. The recovered order has significant agreement with the expert-designed Khan Academy curriculum, and second-generation agents trained on the recovered curriculum learn significantly faster. These results illustrate the synergistic role of abstractions and curricula in the cultural transmission of mathematics.
• Abstract（参考訳）: 一般的な数学的推論は計算不可能であるが、人間は新しい問題を常に解決している。 また、何世紀にもわたって開発された発見は、後世に迅速に伝えられる。 どのような構造がこれを可能とし、どのようにして自動数学的推論を通知するのか? 両パズルの中心は、数学の基礎となる手続き的抽象の構造である。 このアイデアを,khan academyプラットフォーム上で開始代数の5つのセクションをケーススタディとして検討する。 計算基礎を定義するために,任意の点における有効な作用の集合が有限である定理提示環境 peano を導入する。 我々はpeanoを用いて導入代数学の問題と公理を定式化し,よく定義された探索問題を得る。 シンボル推論のための既存の強化学習手法は,難解な問題解決には不十分である。 独自のソリューションから再利用可能な抽象化("戦術")を誘導する機能を追加することで、エージェントは安定した進歩をし、すべての問題を解決することができる。 さらに、これらの抽象化は、トレーニング中にランダムに見られる問題に対する順序を誘導する。 回収命令は、専門家が設計したカーン・アカデミーのカリキュラムと大きく一致しており、回収されたカリキュラムで訓練された第二世代エージェントは、かなり早く学習する。 これらの結果は、数学の文化伝達における抽象概念とカリキュラムの相乗的役割を示している。

関連論文リスト

• LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
  フォーマルな定理証明のための新しい生涯学習フレームワークであるLeanAgentを紹介する。 LeanAgentは継続的に一般化し、拡張可能な数学的知識を改善します。 以前、23のリーンリポジトリで人間が公式に証明していなかった155の定理の証明に成功した。
  論文  参考訳（メタデータ） (2024-10-08T17:11:24Z)
• Machine learning and information theory concepts towards an AI Mathematician [77.63761356203105]
  人工知能の現在の最先端技術は、特に言語習得の点で印象的だが、数学的推論の点ではあまり重要ではない。 このエッセイは、現在のディープラーニングが主にシステム1の能力で成功するという考えに基づいている。 興味深い数学的ステートメントを構成するものについて質問するために、情報理論的な姿勢を取る。
  論文  参考訳（メタデータ） (2024-03-07T15:12:06Z)
• Symbolic Equation Solving via Reinforcement Learning [9.361474110798143]
  シンボリックスタック計算機を操作する強化学習エージェントを含む新しい深層学習インタフェースを提案する。 構築によって、このシステムは正確な変換と幻覚への免疫が可能である。
  論文  参考訳（メタデータ） (2024-01-24T13:42:24Z)
• A Survey of Deep Learning for Mathematical Reasoning [71.88150173381153]
  我々は過去10年間の数学的推論とディープラーニングの交差点における重要なタスク、データセット、方法についてレビューする。 大規模ニューラルネットワークモデルの最近の進歩は、新しいベンチマークと、数学的推論にディープラーニングを使用する機会を開放している。
  論文  参考訳（メタデータ） (2022-12-20T18:46:16Z)
• LEMMA: Bootstrapping High-Level Mathematical Reasoning with Learned Symbolic Abstractions [13.69691843677107]
  学習数学抽象化(Learning Mathematical Abstractions,LEMMA)は、数学領域における強化学習エージェントのためのアルゴリズムである。 LEMMAを2つの数学的推論タスク(方程式解法と分数単純化法)で段階的に評価する。
  論文  参考訳（メタデータ） (2022-11-16T04:59:08Z)
• JiuZhang: A Chinese Pre-trained Language Model for Mathematical Problem Understanding [74.12405417718054]
  本稿では,中国初の数学的事前学習言語モデル(PLM)を提示することにより,機械の数学的知性向上を目指す。 他の標準のNLPタスクとは異なり、数学的テキストは問題文に数学的用語、記号、公式を含むため理解が難しい。 基礎課程と上級課程の両方からなる数学PLMの学習を改善するための新しいカリキュラム事前学習手法を設計する。
  論文  参考訳（メタデータ） (2022-06-13T17:03:52Z)
• NaturalProofs: Mathematical Theorem Proving in Natural Language [132.99913141409968]
  数学的ステートメントの多領域コーパスであるNaturalProofsとその証明を開発した。 NaturalProofsは広範なカバレッジ、深いカバレッジ、低リソースの数学的ソースを統一する。 数式参照検索と生成タスクに関する強力なニューラルネットワーク手法をベンチマークする。
  論文  参考訳（メタデータ） (2021-03-24T03:14:48Z)

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

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