Das Artificial Intelligence Toolkit definiert die Form der automatischen Theoremprüfer der nächsten Generation und damit die Beziehung zwischen Mathematik und Maschinen.
Es wird gesagt, dass der inzwischen verstorbene Mathematiker Paul Cohen , der einzige Gewinner der Fields-Medaille für seine Arbeit zur mathematischen Logik , 1970 unbegründete Vorhersagen getroffen hat, die die Mathematiker immer noch erfreuen oder irritieren: "Eines Tages wird er die Zukunft der Mathematiker ersetzen." Computers ". Cohen, bekannt für seine gewagten Methoden in der Arbeit mit der Mengenlehre, sagte voraus, dass die gesamte Mathematik automatisiert werden könnte, einschließlich des Schreibens von Beweisen.
Beweis ist eine schrittweise logische Argumentation, die die Wahrheit einer Hypothese oder mathematischen Annahme bestätigt. Nachdem ein Beweis erscheint, wird eine Hypothese zum Theorem. Beides bestätigt die Richtigkeit der Aussage und erklärt, warum sie wahr ist. Aber der Beweis ist seltsam. Es ist abstrakt und nicht an materielle Erfahrung gebunden. "Sie sind das Ergebnis eines wahnsinnigen Kontakts zwischen einer fiktiven, nicht-physischen Welt und Kreaturen, die aus der biologischen Evolution hervorgegangen sind", sagte der Kognitionswissenschaftler Simon Dedeo von der Carnegie Mellon University, der die mathematische Sicherheit durch die Analyse von Evidenzstrukturen untersucht. "Die Evolution hat uns nicht darauf vorbereitet."
Computer sind gut für Bulk-Computing, aber der Beweis erfordert etwas anderes. Hypothesen entstehen aus induktivem Denken - eine besondere Intuition, die mit einem interessanten Problem verbunden ist - und Beweise folgen normalerweise deduktiver, schrittweiser Logik. Sie erfordern oft komplexes kreatives Denken sowie die harte Arbeit, die Lücken zu füllen, und Maschinen können mit dieser Kombination von Fähigkeiten nicht umgehen.
Computergestützte Theoremprüfer lassen sich in zwei Kategorien einteilen. Automatisierte Theoremprüfer (ATPs) verwenden normalerweise Brute-Force-Methoden, um riesige Mengen von Zahlen zu mahlen. Interaktive Theorembeweiser (ITPs) dienen als menschliche Assistenten und können die Richtigkeit von Argumenten überprüfen sowie nach Fehlern in vorhandenen Beweisen suchen. Selbst wenn Sie diese beiden Strategien kombinieren (wie auch modernere Prüfer), entsteht daraus kein automatisches Argumentationssystem.
Der Kognitionswissenschaftler Simon Dedeo von der Carnegie Mellon University hat gezeigt, dass Menschen und Maschinen auf ähnliche Weise mathematische Beweise erstellen.
Darüber hinaus sind diese Tools nur sehr wenige Menschen willkommen, und die meisten Mathematiker verwenden oder genehmigen sie nicht. "Dies ist ein kontroverses Thema für Mathematiker", sagte Dedeo. "Die meisten von ihnen mögen die Idee nicht."
Eines der offenen Probleme in diesem Bereich ist die Frage, wie viel des Proof-Erstellungsprozesses automatisiert werden kann. Wird das System in der Lage sein, eine interessante Hypothese zu erstellen und diese auf eine für Menschen verständliche Weise zu beweisen? Eine Reihe von jüngsten Durchbrüchen aus Labors auf der ganzen Welt bieten Möglichkeiten zur Beantwortung dieser Frage durch künstliche Intelligenz (KI). Joseph Urban vom Tschechischen Institut für Informatik, Robotik und Kybernetik in Prag untersucht verschiedene Ansätze, die maschinelles Lernen nutzen, um die Effektivität bestehender Prüfer zu steigern. Im Juli seine Gruppezeigten eine Reihe von ursprünglichen Hypothesen und Beweisen, die von Maschinen erstellt und validiert wurden. Im Juni veröffentlichte eine Gruppe bei Google Research unter der Leitung von Christian Szegedi die Ergebnisse von Versuchen, die Stärken natürlicher Sprachverarbeitungssysteme zu nutzen, um Computerbeweise in Struktur und Erklärung denen menschlicher ähnlicher zu machen.
Einige Mathematiker betrachten Theorembeweiser als Werkzeuge, die die Art und Weise revolutionieren können, wie Schüler lernen, Beweise zu schreiben. Andere sagen, dass es unnötig und wahrscheinlich unmöglich ist, Computer dazu zu bringen, Beweise für fortgeschrittene Mathematik zu schreiben. Ein System, das eine nützliche Hypothese vorhersagen und einen neuen Satz beweisen kann, kann jedoch etwas Neues erreichen - eine Art Maschinenversion des Verstehens, sagte Szegedi. Und dies legt die Möglichkeit des automatischen Denkens nahe.
Nützliche Maschinen
Mathematiker, Logiker und Philosophen haben lange darüber diskutiert, welcher Teil des Beweises menschlicher Natur ist, und die Debatte über die Mechanisierung der Mathematik geht bis heute weiter - insbesondere dort, wo Informatik mit reiner Mathematik verschmilzt.
Für Informatiker sind Theorembeweiser nicht umstritten. Sie bieten eine klare Möglichkeit, die Funktionsfähigkeit des Programms zu bestätigen, und Argumente zu Intuition und Kreativität sind weniger wichtig als die Suche nach wirksamen Wegen zur Lösung von Problemen. Zum Beispiel hat Adam Chlipala , ein Informatiker am Massachusetts Institute of Technology, Theorembeweisungswerkzeuge entwickelt, die generierenkryptografische Algorithmen, die Transaktionen im Internet schützen - trotz der Tatsache, dass normalerweise solche Algorithmen entwickelt werden. Sein Gruppencode wird bereits in den meisten Mitteilungen im Google Chrome-Browser verwendet.
Emily Riel von der Johns Hopkins University verwendet Theoremprüfer, um Studenten und Computerassistenten auszubilden.
"Sie können jede mathematische Aussage nehmen und mit einem Werkzeug codieren, dann alle Argumente kombinieren und einen Sicherheitsnachweis erhalten", sagte Chlipala.
In der Mathematik halfen Theoremprüfer dabei, komplexe und rechenintensive Beweise zu erstellen, die sonst Tausende von mathematischen Mannjahren gedauert hätten. Ein bemerkenswertes Beispiel ist Keplers Hypotheseüber die dichteste Packung von Kugeln im dreidimensionalen Raum (historisch gesehen waren dies Orangen oder Kanonenkugeln). Im Jahr 1998 vervollständigten Thomas Hales und sein Schüler Sam Ferguson diesen Beweis mit einer Vielzahl computergestützter mathematischer Techniken. Das Ergebnis war so umständlich - der Beweis dauerte 3 GB -, dass 12 Mathematiker es mehrere Jahre lang analysierten, bevor sie bekannt gaben, dass sie sich zu 99% der Wahrheit sicher waren.
Keplers Hypothese ist nicht das einzige berühmte Problem, das von Maschinen gelöst wird. Mit dem VierfarbensatzDie Behauptung, dass vier Farben immer ausreichen, um eine zweidimensionale Karte zu malen, in der es keine zwei sich berührenden Bereiche derselben Farbe gibt, wurde 1977 mit einem Computerprogramm herausgefunden, das fünffarbige Karten verarbeitete und zeigte, dass alle in vier Farben umgewandelt werden können. Im Jahr 2016 verwendeten drei Mathematiker ein Computerprogramm, um das langjährige boolesche Problem der pythagoreischen Drillinge zu beweisen. Die erste Version des Beweises war jedoch 200 TB. Wenn Sie über eine ausreichend schnelle Internetverbindung verfügen, können Sie diese in drei Wochen herunterladen.
Gemischte Gefühle
Diese Beispiele werden oft als Erfolge angepriesen, aber sie verleihen Kontroversen auch ihren eigenen Geschmack. Der Computercode, der vor mehr als 40 Jahren den Vierfarbensatz bewies, konnte vom Menschen nicht verifiziert werden. "Mathematiker haben seitdem darüber diskutiert, ob dies ein Beweis ist oder nicht", sagte der Mathematiker Michael Harris von der Columbia University.
Viele Mathematiker, zusammen mit Michael Harris von der Columbia University, stellen die Notwendigkeit in Frage, computergestützte Theorembeweiser zu erstellen - und dass letztere Mathematiker unnötig machen würden.
Eine weitere Unzufriedenheit der Mathematiker hängt mit der Tatsache zusammen, dass sie, wenn sie Theorembeweiser verwenden möchten, zuerst lernen müssen, wie man programmiert, und dann herausfinden, wie sie ihr Problem in einer computerverständlichen Sprache ausdrücken können - und all dies lenkt von der Mathematik ab. "Wenn ich die Frage so umformuliere, dass sie für diese Technologie geeignet ist, werde ich dieses Problem selbst lösen", sagte Harris.
Viele Menschen sehen einfach keine Notwendigkeit für Theoremlöser. "Sie haben ihr eigenes System, Bleistift und Papier, und es funktioniert", sagte Kevin Buzzard, ein Mathematiker am Imperial College London, der vor drei Jahren die Forschungsrichtung von reiner Mathematik zu Theorembeweisern und formalen Beweisen geändert hat. "Computer machen erstaunliche Berechnungen für uns, aber sie haben ein schwieriges Problem nie alleine gelöst", sagte er. "Und bis das passiert, werden Mathematiker es nicht kaufen."
Aber Buzzard und andere glauben, dass sie sich die Technologie möglicherweise noch genauer ansehen müssen. Zum Beispiel "Computer-Beweise sind möglicherweise nicht so fremd wie wir denken", sagte Dedeo. Kürzlich hat er zusammen mit Scott Viteri, einem Informatiker in Stanford, mehrere berühmte kanonische Beweise (einschließlich einiger der Anfänge) rückentwickeltEuklid) und Dutzende von Beweisen, die von einem Computerprogramm erstellt wurden, um Coq- Theoreme zu beweisen, die nach Ähnlichkeiten suchen. Sie stellten fest, dass die Verzweigungsstruktur von Maschinenbeweisen der von Menschen hergestellten Beweisen bemerkenswert ähnlich war. Diese gemeinsame Eigenschaft könne Forschern helfen, einen Weg zu finden
Lassen Sie die Hilfsprogramme erklären: "Maschinelle Beweise sind möglicherweise nicht so kryptisch, wie sie scheinen", sagte Dedeo.
Andere sagen , Theoremprüfer können nützliche Werkzeuge für den Unterricht in Informatik und Mathematik sein. Emily Riel, Mathematikerin an der Johns Hopkins Universityhat Kurse entwickelt, in denen Studenten Beweise mit Theoremprüfern schreiben. "Es macht sie sehr organisiert und denken klar", sagte sie. "Schüler, die zum ersten Mal einen Beweis schreiben, verstehen möglicherweise nicht sofort, was von ihnen verlangt wird, oder verstehen die logische Struktur nicht."
Riel sagt auch, dass er in letzter Zeit häufiger Theorembeweiser in seiner Arbeit verwendet hat. "Sie müssen nicht ständig verwendet werden und werden niemals Kritzeleien auf einem Blatt Papier ersetzen", sagte sie, "aber die Verwendung von Computerassistenten als Beweismittel hat mein Verständnis für das Schreiben von Beweismitteln verändert."
Theorembeweiser bieten auch eine Möglichkeit, die Mathematik fair zu halten. 1999 sowjetischer, russischer und amerikanischer MathematikerVladimir Alexandrovich Voevodsky , entdeckte einen Fehler in einem seiner Beweise. Von da an bis zu seinem Tod im Jahr 2017 förderte er aktiv den Einsatz von Computern zur Überprüfung von Beweisen. Hales sagte, dass er und Ferguson Hunderte von Fehlern in ihren ursprünglichen Beweisen gefunden hätten, indem sie sie mit Computern getestet hätten. Selbst die allerersten Sätze in Euklids Elementen sind nicht ideal. Wenn eine Maschine Mathematikern helfen kann, solche Fehler zu vermeiden, warum nicht davon profitieren? Harris hat einen praktischen Einwand gegen diesen Vorschlag erhoben, es ist jedoch nicht bekannt, wie vernünftig er ist: Wenn Mathematiker Zeit damit verbringen müssen, Mathematik zu formalisieren, damit ein Computer sie versteht, können sie diese Zeit nicht für neue Mathematik verwenden.
Allerdings Timati GowersDer Mathematiker und Preisträger des Fields Prize aus Cambridge möchte noch weiter gehen: Er stellt sich vor, wie Theorembeweiser künftig menschliche Rezensenten in wichtigen Fachzeitschriften ersetzen werden. "Ich sehe, wie dies zur Standardpraxis werden kann. Wenn Sie möchten, dass Ihre Arbeit akzeptiert wird, müssen Sie sie durch einen automatisierten Prüfer ausführen."
Gespräch mit Computern
Bevor Computer Beweise verifizieren oder entwickeln können, müssen Forscher zunächst eine erhebliche Hürde überwinden: die Kommunikationsbarriere zwischen den Sprachen von Mensch und Computer.
Die heutigen Theorembeweiser wurden ohne Berücksichtigung der Mathematikerfreundlichkeit entwickelt. Der erste Typ, ATP, wurde üblicherweise verwendet, um die Wahrheit einer Aussage zu testen, häufig durch Testen aller möglichen Optionen. Fragen Sie die ATP, ob es möglich ist, von Miami nach Seattle zu reisen, und er wird wahrscheinlich alle Städte durchqueren, in die die Straßen von Miami führen, und schließlich die Stadt finden, die nach Seattle führt.
Timati Gowers von der Universität Cambridge glaubt, dass Theoremprüfer eines Tages menschliche Rezensenten ersetzen werden
Mit ATP kann der Programmierer alle Regeln oder Axiome codieren und dann die Frage stellen, ob eine bestimmte Hypothese diesen Regeln folgt. Und dann erledigt der Computer die ganze Arbeit. "Sie geben einfach die Hypothese ein, die Sie beweisen möchten, und hoffen auf eine Antwort", sagte Daniel Huang, ein Informatiker, der kürzlich die UC Berkeley verlassen hat, um ein Startup zu gründen.
Aber es gibt ein Problem: ATP erklärt seine Arbeit nicht. Alle Berechnungen finden innerhalb der Maschine statt und sehen für eine Person wie eine lange Folge von Nullen und Einsen aus. Huang sagte, es sei unmöglich, die Beweise zu überprüfen und die Argumentation zu überprüfen, da alles wie eine Menge zufälliger Daten aussehe. "Niemand kann sich solche Beweise ansehen und sagen: Alles ist klar", sagte er.
Die zweite Kategorie, das ITP, verfügt über riesige Datensätze mit Zehntausenden von Theoremen und Beweisen, mit denen sie die Richtigkeit eines Beweises überprüfen können. Im Gegensatz zu ATPs, die in einer Black Box arbeiten, in der lediglich Antworten ausgegeben werden, erfordern ITPs Interaktion und manchmal Anweisungen von einer Person, sodass sie nicht so unnahbar sind. "Eine Person kann sich hinsetzen und herausfinden, welche Techniken verwendet werden, um zu beweisen", sagte Huang. Solche Beweise wurden von Dedeo und Viteri untersucht.
In den letzten Jahren sind ITPs immer beliebter geworden. Im Jahr 2017 verwendete die Dreifaltigkeit, die das Boolesche Problem der pythagoreischen Drillinge bewies, ein ITP namens Coq, um eine formale Version ihres Beweises zu erstellen und zu testen. Im Jahr 2005 verwendete Georges Gontier von Microsoft Research Cambridge Coq, um den Vierfarbensatz zu formalisieren. Hales verwendete auch ITPs namens HOL Light und Isabelle, um Keplers Vermutung formal zu beweisen (HOL steht für Logik höherer Ordnung).
Heute versucht die Spitze dieses Bereichs, Lernen mit Denken zu verbinden. ATP wird häufig mit ITP kombiniert, um maschinelles Lernen zu integrieren und die Leistung beider Techniken zu verbessern. Experten glauben, dass ATP / ITP-Programme deduktives Denken verwenden und sogar mathematische Ideen auf die gleiche Weise wie Menschen oder zumindest auf ähnliche Weise austauschen können.
Grenzen des Denkens
Joseph Urban glaubt, dass ein solcher kombinierter Ansatz deduktives und induktives Denken verbinden kann, was notwendig ist, um Beweise zu erhalten. Seine Gruppe entwickelte Theoremprüfer, die auf maschinellem Lernen basieren und es Computern ermöglichen, selbst aus Erfahrungen zu lernen. In den letzten Jahren haben sie die Leistungsfähigkeit neuronaler Netze untersucht - Schichten von Recheneinheiten, mit denen Maschinen Informationen auf eine Art und Weise verarbeiten können, die in etwa der Funktionsweise von Neuronen in unserem Gehirn ähnelt. Im Juli berichtete ihre Gruppe über neue Hypothesen, die von einem neuronalen Netzwerk generiert wurden, das auf Theoremprüfung trainiert wurde.
Zum Teil war Urban von der Arbeit von Andrei Karpaty inspiriert, der vor einigen Jahren ein neuronales Netzwerk trainierte, um mathematischen Unsinn zu produzieren, der für Laien überzeugend aussah. Aber Urban brauchte den Unsinn nicht - er und die Gruppe entwickelten ein eigenes Werkzeug, das nach Beweisen sucht, nachdem sie Millionen von Theoremen trainiert hatten. Sie nutzten das Netzwerk, um neue Hypothesen zu erstellen und ihre Gültigkeit mit einem ATP-Programm namens E zu testen.
Das Netzwerk hat über 50.000 neue Formeln herausgegeben, von denen Zehntausende wiederholt wurden. "Es scheint, dass wir noch keine interessanteren Hypothesen beweisen können", sagte Urban.
Szegedi von Google Research sieht das Problem des automatischen Denkens in Computerbeweisen als Teil eines viel breiteren Feldes: der Verarbeitung natürlicher Sprache, einschließlich des Erkennens von Mustern bei der Verwendung von Wörtern und Sätzen. Die Mustererkennung ist auch eine Kernidee des Computer Vision, an der Szegedi zuvor bei Google gearbeitet hat. Wie andere Gruppen möchte sein Team Theorembeweiser erstellen, die nach nützlichen Beweisen suchen und diese erklären können.
Inspiriert von der rasanten Entwicklung von KI-Tools wie AlphaZero - DeepMinds Software, die Menschen beim Schach, Go und Shogi schlagen kann - möchte die Szegedi-Gruppe die neuesten Fortschritte in der Spracherkennung nutzen, um Beweise aufzuzeichnen. Er sagte, dass Sprachmodelle überraschend genaues mathematisches Denken demonstrieren können.
Seine Gruppe bei Google Research hat kürzlich eine Möglichkeit beschrieben, Sprachmodelle - die häufig von neuronalen Netzen verwendet werden - zu verwenden, um neue Beweise zu generieren. Nachdem sie das Modell trainiert hatten, um die Baumstruktur bewährter Theoreme zu erkennen, starteten sie ein kostenloses Experiment, bei dem sie einfach neuronale Netze aufforderten, Theoreme ohne Aufsicht zu generieren und zu beweisen. Von den Tausenden von generierten Hypothesen erwiesen sich 13% als beweisbar und neu (ohne Wiederholung anderer Theoreme in der Datenbank). Er sagte, dass ein solches Experiment besagt, dass neuronale Netze in gewissem Sinne lernen können, zu verstehen, wie die Beweise aussehen.
"Neuronale Netze können einen künstlichen Anschein von Intuition entwickeln", sagte Szegedi.
Natürlich ist immer noch nicht klar, ob diese Versuche Cohens Prophezeiung vor 40 Jahren erfüllen werden. Gowers sagte, er glaube, dass Computer Mathematiker bis 2099 in ihrer Argumentation übertreffen können. Zunächst, so sagt er, werden Mathematiker ein goldenes Zeitalter erleben: „Wenn sie interessante Dinge tun und Computer langweilig sind. Aber ich denke, es wird nicht lange dauern. "
Wenn sich Maschinen immer weiter entwickeln und Zugriff auf eine große Datenmenge haben, müssen sie schließlich lernen, sehr gute und interessante Dinge zu tun. "Sie werden lernen, ihre eigenen Anfragen zu stellen", sagte Gowers.
Harris ist anderer Meinung. Er glaubt nicht, dass Computerbeweise notwendig sind oder dass sie letztendlich "menschliche Mathematiker unnötig machen". Wenn Informatiker jemals synthetische Intuition programmieren können, wird sie immer noch nicht mit menschlicher Intuition konkurrieren. "Selbst wenn Computer verstehen, werden sie im menschlichen Sinne nicht verstehen."