論文の概要: Considerations on Approaches and Metrics in Automated Theorem Generation/Finding in Geometry

• arxiv url: http://arxiv.org/abs/2401.11905v1
• Date: Mon, 22 Jan 2024 12:51:19 GMT
• ステータス: 処理完了
• システム内更新日: 2024-01-23 14:12:05.982506
• Title: Considerations on Approaches and Metrics in Automated Theorem Generation/Finding in Geometry
• Title（参考訳）: 幾何学における自動定理生成/フィンディングのアプローチと計量に関する考察
• Authors: Pedro Quaresma (University of Coimbra), Pierluigi Graziani (University of Urbino), Stefano M. Nicoletti (University of Twente)
• Abstract要約: 我々は、幾何定理(と性質)の自動発見のための異なるアプローチを提示し、議論する。 定理証明者が興味深い定理を生成できるかどうかを判断することは、決定論的でない課題である。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The pursue of what are properties that can be identified to permit an automated reasoning program to generate and find new and interesting theorems is an interesting research goal (pun intended). The automatic discovery of new theorems is a goal in itself, and it has been addressed in specific areas, with different methods. The separation of the "weeds", uninteresting, trivial facts, from the "wheat", new and interesting facts, is much harder, but is also being addressed by different authors using different approaches. In this paper we will focus on geometry. We present and discuss different approaches for the automatic discovery of geometric theorems (and properties), and different metrics to find the interesting theorems among all those that were generated. After this description we will introduce the first result of this article: an undecidability result proving that having an algorithmic procedure that decides for every possible Turing Machine that produces theorems, whether it is able to produce also interesting theorems, is an undecidable problem. Consequently, we will argue that judging whether a theorem prover is able to produce interesting theorems remains a non deterministic task, at best a task to be addressed by program based in an algorithm guided by heuristics criteria. Therefore, as a human, to satisfy this task two things are necessary: an expert survey that sheds light on what a theorem prover/finder of interesting geometric theorems is, and - to enable this analysis - other surveys that clarify metrics and approaches related to the interestingness of geometric theorems. In the conclusion of this article we will introduce the structure of two of these surveys - the second result of this article - and we will discuss some future work.
• Abstract（参考訳）: 自動推論プログラムが新しく興味深い定理を生成、発見できるようにするために特定できる性質の追求は興味深い研究目標である(punは意図している)。 新しい定理の自動発見はそれ自体が目標であり、異なる方法で特定の領域で解決されてきた。 雑草(weeds)、興味がなく、自明な事実、新しい興味深い事実(wheat)、そして興味深い事実の分離は、はるかに困難であるが、異なるアプローチを用いて、異なる著者によって対処されている。 本稿では幾何学に焦点をあてる。 幾何学的定理(および性質)の自動発見のための異なるアプローチと、生成された全ての定理の中で興味深い定理を見つけるために異なるメトリクスを提示し、議論する。 この記述の後、この論文の最初の結果を紹介します: 興味深い定理を生成できるかどうかに関わらず、定理を生成する可能なチューリングマシンを全て決定するアルゴリズム的な手順を持つことは、決定不可能な問題である。 したがって、定理証明者が興味深い定理を生成できるかどうかを判断することは決定論的でない課題であり、少なくともヒューリスティックス基準で導かれたアルゴリズムに基づいてプログラムによって対処すべきタスクである。 それゆえ、人間として、このタスクを満足させるには、2つのことが必要である: 興味深い幾何学的定理の定理証明者/ファインダーについて光を当てるエキスパートサーベイと、この分析を可能にするために - 幾何学的定理の興味深い性質に関連するメトリクスとアプローチを明らかにする他のサーベイ。 本稿の結論では、この2つの調査(この記事の2番目の結果)の構造について紹介し、今後の課題について検討する。

関連論文リスト

• Learning Formal Mathematics From Intrinsic Motivation [34.986025832497255]
  ミニモ(Minimo)は、自分自身に問題を起こし、それを解決することを学ぶエージェント(理論実証)である。 制約付き復号法と型指向合成法を組み合わせて、言語モデルから有効な予想をサンプリングする。 我々のエージェントは、ハードだが証明可能な予想を生成することを目標としています。
  論文  参考訳（メタデータ） (2024-06-30T13:34:54Z)
• 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)
• TheoremQA: A Theorem-driven Question Answering dataset [100.39878559382694]
  GPT-4のこれらの問題を解決する能力は非並列であり、Program-of-Thoughts Promptingの精度は51%である。 TheoremQAは、350の定理をカバーする800の高品質な質問を含むドメインの専門家によってキュレートされる。
  論文  参考訳（メタデータ） (2023-05-21T17:51:35Z)
• Representer Theorems for Metric and Preference Learning: A Geometric Perspective [0.0]
  計量学習と選好学習を同時に行うための新しい代表者定理を得る。 本稿では,三重項比較によるメートル法学習の課題に対して,本フレームワークが適用可能であることを示す。 カーネル・ヒルベルト・スペースを再現する場合、学習問題の解をカーネル用語で表現できることを実証する。
  論文  参考訳（メタデータ） (2023-04-07T16:34:25Z)
• A singular Riemannian geometry approach to Deep Neural Networks I. Theoretical foundations [77.86290991564829]
  ディープニューラルネットワークは、音声認識、機械翻訳、画像解析など、いくつかの科学領域で複雑な問題を解決するために広く使われている。 我々は、リーマン計量を備えた列の最後の多様体で、多様体間の写像の特定の列を研究する。 このようなシーケンスのマップの理論的性質について検討し、最終的に実践的な関心を持つニューラルネットワークの実装間のマップのケースに焦点を当てる。
  論文  参考訳（メタデータ） (2021-12-17T11:43:30Z)
• Inter-GPS: Interpretable Geometry Problem Solving with Formal Language and Symbolic Reasoning [123.06420835072225]
  3,002の幾何学的問題と密接なアノテーションを形式言語に含む新しい大規模ベンチマークGeometry3Kを構築します。 我々は、Interpretable Geometry Problemsolvr (Inter-GPS)と呼ばれる形式言語と記号推論を用いた新しい幾何学的解法を提案する。 イントラGPSは定理の知識を条件付き規則として取り入れ、記号的推論を段階的に行う。
  論文  参考訳（メタデータ） (2021-05-10T07:46:55Z)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。 実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
  論文  参考訳（メタデータ） (2020-02-17T16:06:02Z)

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

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