Lecture: AUTOMATED REASONING: FROM SEARCH-BASED TECHNIQUES TO PLANNING
Author: Jörg Siekman
1. Automated (mathematical) concept formation and discovery 2. Automated theory formation (in mathematics)
Anna Ingolfsdottir, Reykjavik U.
Antonio Chella, U. Palermo, Italy
Bas Steunebrink, IDSIA, Switzerland
Deon Garrett, IIIM, Iceland
Conclusions: Prolog is an example of theorem prover, but a automated system has to discover what to prove.
Examples from genetics: you don't know what are you looking for - unsupervised search is needed. Similar in robotics: a real autonomous robot doesn't need to have its own goals.
A robot should be curiosity driven.
This challenge has some point in common with self programming systems: a novel theory is like a novel program.
A main point is how to formalize creativity.
Complexity how to reduce NP to P
Sometimes, as in proving of the Fermat last theorem, it is necessary to change the problem and solve another problems in order to solve the original one.
The discovery of new concepts is based on paradigm shifts, in order to solve problems in the original paradigm: negative numbers have been discovered to solve problems in natural numbers, real numbers have been discovered to solve problems in rational numbers, imaginary numbers are discovered to solve problems in real numbers and so on.
A completely new truth expand an existent theory.
Eric Baum, USA
Eric Nivel, Reykjavik U.
Gudny R. Jonsdottir, IIIM, Iceland
Hamid Pourvatan, IIIM, Iceland
Where does intelligence come from? Can a system „come up with“ a concept?
A concept is a piece of knowledge, that, when computed serves a purpose (it has a meaning)
In the example of the limit function? What is the concept we want to formulate it?
Concept is „things that implies the concept and things that the concept implies“
We dont just want to find a concept, we want to find meaningful concept that serve a purpose, this purpose is defined by a goal
Automated theory formation = Finding useful actions
Hannes Högni Vilhjalmsson, Reykjavik U.
Haris Dindo, U. Palermo, Italy
Helgi Páll Helgason, Reykjavik U.
Hrafn Th. Thorisson, IIIM, Iceland
Ricardo Sanz, U. Madrid
Team Conclusions: There is no external environment to perform experiments in the mathematical domain. Any new knowledge we must actively generate ourselves from existing knowledge.
Relation between challenges - in order to discover a concept, a proven theory of its existence may be a precondition (if the concept was not directly supplied).
Space of possible theories is potentially huge - depending on known concepts/axioms. Interestingness / usefulness is a possible heuristic to guide this search.
Posing interesting questions (theories) likely to lead to interesting (concepts) Measure of interestingness (heuristics) is key.
Related to constructivism. Machine will generate own concepts. Generate the concepts it needs or fall into the world of infinite abstraction. Where should we stop in the abstraction? (going further and further will create concepts harder to match with reality)
James Bonaiuto, Cal Tech, USA
John-Jules Meyer, U. of Utrecht, the Netherlands
Jörg Siekman, DFKI, Germany
Kristinn R. Thórisson, Reykjavik U. / IIIM, Iceland
Luca Aceto, Reykjavik U.
Team Conclusions: There are two views: one says to feed the system with mathematical knowledge. Concepts are not isolated, so you need to represent some web of knowledge over and above these, so that needs to be part of the information you give the system. And then you would need algortihms that enable it to infer commonalities among concepts, using the web of knowledge. That is one view. This, however, might help us automate discovery, but is unlikely to enable automatic theory formation. For creation of new ideas: the system must be able to propose ideas and then evaluate. They must be able to form abstract notions and make analogies. For this the present methods fall short. The other view is thus that this is not enough, or even the wrong focus, that we rather need to build the system so that it can learn to understand mathematics from more basic principles, involving, among other things, non-symbolic representations.
An even more general comment is that in order to guide the system you need to provide it (either via training or direct “feeding”) with more general knowledge that enables it to understand guiding principles and worthy tasks to work on given by its human creators, because after all the system is intended to serve humans, or humanity in some way. There is the question of whether we want to create a “human mathematician's assistant system” or an “automated mathematician”. The above becomes even more important in this light, because if you want an automated mathematician some connection to societal issues might be necessary.