論文の概要: Learning Formal Mathematics From Intrinsic Motivation

• arxiv url: http://arxiv.org/abs/2407.00695v2
• Date: Tue, 05 Nov 2024 01:40:45 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-11-06 14:56:03.705750
• Title: Learning Formal Mathematics From Intrinsic Motivation
• Title（参考訳）: 固有モチベーションから形式数学を学ぶ
• Authors: Gabriel Poesia, David Broman, Nick Haber, Noah D. Goodman,
• Abstract要約: ミニモ(Minimo)は、自分自身に問題を起こし、それを解決することを学ぶエージェント(理論実証)である。 制約付き復号法と型指向合成法を組み合わせて、言語モデルから有効な予想をサンプリングする。 我々のエージェントは、ハードだが証明可能な予想を生成することを目標としています。
• 参考スコア（独自算出の注目度）: 34.986025832497255
• License:
• Abstract: How did humanity coax mathematics from the aether? We explore the Platonic view that mathematics can be discovered from its axioms - a game of conjecture and proof. We describe Minimo (Mathematics from Intrinsic Motivation): an agent that jointly learns to pose challenging problems for itself (conjecturing) and solve them (theorem proving). Given a mathematical domain axiomatized in dependent type theory, we first combine methods for constrained decoding and type-directed synthesis to sample valid conjectures from a language model. Our method guarantees well-formed conjectures by construction, even as we start with a randomly initialized model. We use the same model to represent a policy and value function for guiding proof search. Our agent targets generating hard but provable conjectures - a moving target, since its own theorem proving ability also improves as it trains. We propose novel methods for hindsight relabeling on proof search trees to significantly improve the agent's sample efficiency in both tasks. Experiments on 3 axiomatic domains (propositional logic, arithmetic and group theory) demonstrate that our agent can bootstrap from only the axioms, self-improving in generating true and challenging conjectures and in finding proofs.
• Abstract（参考訳）: 人類はどのようにしてエーテルから数学を粗末にしたのか。 数学はその公理(予想と証明のゲーム)から発見できるというプラトン的見解を探求する。 ミニモ(intrinsic Motivation, 内在的モチベーションの数学)は, 自己に挑戦的な問題を提起し, 解決するために共同で学習するエージェントである。 依存型理論で公理化された数学的領域が与えられたとき、まず制約付き復号法と型指向合成法を組み合わせて、言語モデルから有効な予想をサンプリングする。 提案手法は, ランダムに初期化モデルから始める場合であっても, 構成によるよく整形された予想を保証する。 我々は同じモデルを用いて、証明探索を導くためにポリシーと値関数を表現している。 我々のエージェントは、ハードだが証明可能な予想を生成することを目標としています。 本稿では,両タスクにおいてエージェントのサンプル効率を著しく向上させるため,実証探索木に隠れたラベリングを行う新しい手法を提案する。 3つの公理的領域(命題論理、算術、群論)の実験は、我々のエージェントが公理のみからブートストラップできることを示した。

関連論文リスト

• ATG: Benchmarking Automated Theorem Generation for Generative Language Models [83.93978859348313]
  人間はより広範に複雑な数学的結果を探求するために新しい定理を開発することができる。 現在の生成言語モデル(LM)は、定理の自動証明において著しく改善されている。 本稿では,エージェントが価値ある(あるいは新しい)定理を自動生成できるかどうかを評価する自動定理生成ベンチマークを提案する。
  論文  参考訳（メタデータ） (2024-05-05T02:06:37Z)
• Machine learning and information theory concepts towards an AI Mathematician [77.63761356203105]
  人工知能の現在の最先端技術は、特に言語習得の点で印象的だが、数学的推論の点ではあまり重要ではない。 このエッセイは、現在のディープラーニングが主にシステム1の能力で成功するという考えに基づいている。 興味深い数学的ステートメントを構成するものについて質問するために、情報理論的な姿勢を取る。
  論文  参考訳（メタデータ） (2024-03-07T15:12:06Z)
• Mathematical conjecture generation using machine intelligence [0.0]
  f の型 f の厳密な不等式に焦点をあて、それらをベクトル空間に関連付ける。 我々は、この多様体の線型自己同型を研究することによって、この予想空間の構造的理解を発展させる。 幾何勾配勾配を用いた新しい予想を生成するアルゴリズムパイプラインを提案する。
  論文  参考訳（メタデータ） (2023-06-12T17:58:38Z)
• Peano: Learning Formal Mathematical Reasoning [35.086032962873226]
  一般的な数学的推論は計算不可能であるが、人間は新しい問題を常に解決している。 両パズルの中心は、数学の基礎となる手続き的抽象の構造であると仮定する。 カーン・アカデミー・プラットフォーム上の始点代数の5つの部分に関するケーススタディにおいて、このアイデアを探求する。
  論文  参考訳（メタデータ） (2022-11-29T01:42:26Z)
• Towards a Mathematics Formalisation Assistant using Large Language Models [5.485439959027125]
  リーン定理証明器の形式化を支援するために,大規模な言語モデル(Codex)の能力について検討する。 コーデックスは、短い数学的ステートメントを120ドルの定理ステートメントに対して75%近い精度でアンダーグレードレベルで定式化することができる。 新たなプロンプト戦略により、コーデックスはこれらの証明を自然言語で定式化することができ、12のコーデックスのうち少なくとも1つの完備化は、完全な証明に容易に修正できることが示される。
  論文  参考訳（メタデータ） (2022-11-14T16:52:32Z)
• NaturalProver: Grounded Mathematical Proof Generation with Language Models [84.2064569475095]
  自然数理言語における定理証明は、数学の進歩と教育において中心的な役割を果たす。 本研究では,背景参照を条件づけて証明を生成する言語モデルであるNaturalProverを開発する。 NaturalProverは、短い(2-6ステップ)証明を必要とするいくつかの定理を証明でき、40%の時間で正しいと評価された次のステップの提案を提供することができる。
  論文  参考訳（メタデータ） (2022-05-25T17:01:18Z)
• Noisy Deductive Reasoning: How Humans Construct Math, and How Math Constructs Universes [0.5874142059884521]
  本稿では,数学が基本的な過程である数学的推論の計算モデルを提案する。 この枠組みが数学的実践のいくつかの側面について説得力のある説明を与えることを示す。
  論文  参考訳（メタデータ） (2020-10-28T19:43:14Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)
• Epistemic Phase Transitions in Mathematical Proofs [0.0]
  我々は,認知的に証明可能な信念形成機構の下では,数学的議論に対する信念は,不確実性からほぼ完全に近い信頼まで,合理的なクレーム・トゥ・クレーム・トゥ・フレーム・エラー・レートで劇的かつ急激な飛躍を経験できることを示した。 我々の結果は、証明を理解する方法に関する数学の歴史と哲学における最近の研究と、複雑な信念を正当化する方法に関する基本的な認知科学に関する疑問の両方に関係している。
  論文  参考訳（メタデータ） (2020-03-31T18:39:56Z)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。 実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
  論文  参考訳（メタデータ） (2020-02-17T16:06:02Z)

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

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