Search

Eines der Ziele künstlicher Intelligenz ist die Fähigkeit, Probleme durch Lernen und automatische Deduktion zu lösen. Bekannte Beispiele intelligenter Systeme sind in Chemie und Spielen wie Schach und Go zu finden. Die aktuell erfolgreichsten Ansätze in diesen Bereichen kombinieren Suchstrategien mit von maschinellen Lernmethoden gelernten statistischen Modellen. Allerdings involvieren mathematische Probleme abstraktere Prinzipien wie Induktion, die automatisierte logische Deduktion erschweren. Der Beweis neuer Theoreme erfordert häufig die Ausnutzung von Mustern, die in komplexen Strukturen eingebettet sind. Das Ziel unseres Projektes ist die Verbesserung automatischer Beweissuchmethoden in der Mathematik. Diese ermöglicht die Reduktion der Zeit, die zum formalen Beweisen komplexer Theoreme wie der Keplerschen Vermutung benötigt wird. Um unser System von einer großen Menge an Beispielen lernen zu lassen, identifizieren wir ähnliche Konzepte in verschiedenen formellen Bibliotheken von interaktiven Theorembeweisern (ITP). Das kombinierte Wissen wird von einem statistischen Modell verarbeitet, welches Beziehungen zwischen mathematischen Objekten ableitet. Wir nutzen diese Beziehungen aus, um bessere Strategien zum Beweis von Theoremen zu erzeugen. Unser System kombiniert Wissen von ITPs mit der Suchfähigkeit von automatischen Theorembeweisern (ATPs). Dies erlaubt es, die Beziehung zwischen neuen Vermutungen und vorhergegangenem formalisierten Wissen mittels des statistischen Modells zu verstehen. Unser System wählt für den Beweis einer Vermutung relevante Theoreme aus, vereinfacht den Beweis durch die Annahme von Lemmata und lenkt die Beweissuche durch den Vorschlag von erfolgversprechenden Beweisschritten. Wenn das System erfolgreich ist, erzeugt es einen automatisch verifizierten Beweis der Vermutung., One of the aims of artificial intelligence is to be able to solve problems through learning and automated reasoning. Famous examples of intelligent systems can be found in molecular chemistry and games such as chess and Go. The current most successful approaches in these domains combine statistical models trained by machine learning methods with search strategies. However, more abstract problems, generally out of reach of current methods, constructed from abstract principles such as induction appear commonly in mathematics. And proving new theorems often requires to exploit patterns hidden in complex structures. The aim of this thesis is to improve automated reasoning techniques in mathematics. This would help to reduce the time needed for formally proving complex theorems such as the Kepler conjecture. In order for our system to learn from a large number of examples, we align the formal libraries of interactive theorem provers (ITPs) by recognizing similar concepts. The shared knowledge is processed by a statistical model which infers relations between mathematical objects. We exploit those links to produce better strategies for proving theorems. In practice, our project combines ITP knowledge with the search power of automated theorem provers (ATPs). Therefore, if a mathematician states a conjecture in an ITP, our system understands through the statistical model the relation of the conjecture to previously formalized knowledge. It selects theorems relevant for proving the conjecture, simplifies the proof by conjecturing intermediate lemmas and may also guide the proof search by choosing suitable reasoning methods. If successful, it produces a computer- verified proof of the conjecture., by Thibault Gauthier, Kumulative Dissertation aus sechs Artikeln, in deutscher und französischer Sprache, University of Innsbruck, Dissertation, 2018, OeBB, (VLID)2759666