Considerations on Approaches and Metrics in Automated Theorem Generation/Finding in Geometry

要約

自動推論プログラムが新しく興味深い定理を生成および発見できるようにするために特定できる特性とは何かを追求することは、興味深い研究目標です (冗談です)。
新しい定理を自動的に発見すること自体が目標であり、特定の領域でさまざまな方法で取り組んできました。
「雑草」である面白くない些細な事実と、新しくて興味深い事実である「小麦」を区別することははるかに困難ですが、これもさまざまな著者によってさまざまなアプローチを用いて取り組まれています。
このホワイトペーパーでは、幾何学に焦点を当てます。
幾何定理 (および特性) を自動的に発見するためのさまざまなアプローチと、生成されたすべての定理の中から興味深い定理を見つけるためのさまざまなメトリクスを提示し、説明します。
この説明の後で、この記事の最初の結果を紹介します。決定不可能性の結果は、定理を生成するすべての可能なチューリング マシンに対して、興味深い定理も生成できるかどうかを決定するアルゴリズム手順を持つことが、決定不可能な問題であることを証明します。
したがって、定理証明者が興味深い定理を生成できるかどうかを判断することは依然として非決定論的なタスクであり、せいぜいヒューリスティック基準に基づいたアルゴリズムに基づいたプログラムによって対処されるタスクであると主張します。
したがって、人間として、この課題を満たすには 2 つのことが必要です。興味深い幾何学定理の定理証明者/発見者が何であるかを明らかにする専門家調査、そして – この分析を可能にする – に関連する指標とアプローチを明らかにする他の調査です。
幾何定理の面白さ。
この記事の終わりに、これらの調査のうち 2 つ (この記事の 2 番目の結果) の構造を紹介し、今後の取り組みについて説明します。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google