Terence Tao nutzt den groß angelegten Modellbeweisassistenten Lean, um seine Vorliebe zu zeigen

„Ich gehe davon aus, dass KI bei richtiger Anwendung bis 2026 zu einem vertrauenswürdigen Co-Autor in der mathematischen Forschung und vielen anderen Bereichen werden wird“, sagte der Mathematiker Terence Tao in einem früheren Blog.

Tao Zhexuan hat das gesagt und es getan.

Er hat kürzlich mathematische Forschungen mit Tools wie GPT-4, Copilot und Lean durchgeführt und mithilfe von KI auch einen versteckten Fehler in seiner Arbeit entdeckt.

Kürzlich sagte Terence Tao, dass das Lean4-Projekt die Formalisierung des Beweises der Polynom-Freiman-Ruzsa-Vermutung (PFR) erfolgreich abgeschlossen hat, was nur drei Wochen gedauert hat. Gleichzeitig meldet der Lean-Compiler auch, dass die Vermutung den Standardaxiomen entspricht. Dies ist ein großer Erfolg des computer- und KI-gestützten Beweises und es ist aufregend

Weitere Informationen zu der oben genannten Forschung finden interessierte Leser unter „Was ist Tao Zhexuans formaler Beweis mit KI?“ Verstehen Sie die Vergangenheit und Gegenwart der PFR-Vermutung in einem Artikel.

Aufmerksame Leser haben den Hinweis vielleicht schon oft entdeckt, als Meister Tao Lean bei mathematischen Forschungen erwähnte. Einfach ausgedrückt ist Lean eine Programmiersprache, die Mathematikern bei der Überprüfung von Theoremen hilft, wobei Benutzer Beweise schreiben und überprüfen können. Im Vergleich zum ursprünglichen Lean verfügt die neueste Lean 4-Version über zahlreiche Optimierungen, darunter einen schnelleren Compiler, eine verbesserte Fehlerbehandlung und eine bessere Integration mit externen Tools.

Lean ist im Bereich der Mathematik weit verbreitet. Gibt es heute, wo große Modelle (LLM) beliebt sind, eine bessere Möglichkeit, beides zu kombinieren?

Jemand hat es bereits implementiert. Das LeanDojo-Team der offenen Plattform (siehe „Das große KI-Modell hilft Tao Zhexuan, Probleme zu lösen, kann es auch mathematische Theoreme beweisen? “) und die Forschung vom California Institute of Technology Der Autor brachte Lean Copilot auf den Markt, ein Kollaborationstool, das für LLM und menschliche Interaktion entwickelt wurde und darauf abzielt, durch Mensch-Maschine-Zusammenarbeit 100 % genaue formale mathematische Beweise zu liefern.

Es ist erwähnenswert, dass sich die Forschung des LeanDojo-Teams hauptsächlich auf die Verwendung von LLM zur Automatisierung des Theoremnachweises konzentriert. Von diesem Punkt an ist es nicht schwer zu erkennen, dass der von ihnen eingeführte Lean Copilot mit LLM zusammenhängt sei überraschend.

Projektadresse: https://github.com/lean-dojo/LeanCopilot

Für diese Forschung bedeutet es nicht nur cool, sondern auch sehr cool, und die Bewertung ist immer noch sehr hoch.

Verwenden Sie LLM in Lean, um den mathematischen Beweis zu beschleunigen.

Der automatisierte Theorembeweis war traditionell immer mit vielen Schwierigkeiten verbunden und erforderte eine sorgfältige Überprüfung. Mit der Weiterentwicklung der KI haben Forscher nun damit begonnen, künstliche Intelligenz für eingehende Untersuchungen zu nutzen, aber dieses Problem ist unvermeidlich, das heißt, LLM ist bei Mathematik- und Denkaufgaben manchmal nicht sehr zuverlässig und anfällig für Fehler und Halluzinationen.

Die Funktion von Lean Copilot besteht darin, Benutzern die Verwendung großer Sprachmodelle zu ermöglichen, um den Beweisprozess in Lean zu automatisieren und die Geschwindigkeit der Beweissynthese zu erhöhen. Benutzer können bei Bedarf auch nahtlos eingreifen und Änderungen vornehmen, um eine ausgewogene Zusammenarbeit zwischen maschineller Intelligenz und menschlicher Intelligenz zu erreichen Benutzer können wählen, ob sie die integrierten Modelle von LeanDojo verwenden oder ihre eigenen Modelle importieren möchten. Diese Modelle können lokal (mit oder ohne GPU) oder in der Cloud ausgeführt werden

Kurz gesagt: Lean Copilot bietet Benutzern eine flexible Möglichkeit, die Theorembeweisführung in Lean durch die Einführung von LLM zu verbessern und zu optimieren.

Die Hauptfunktionen von Lean Copilot lassen sich wie folgt zusammenfassen:

• LLM ist in der Lage, Beweisschritte vorzuschlagen, nach Beweisen zu suchen und nützliche Lemmata aus einer großen mathematischen Bibliothek auszuwählen.
• Lean Copilot kann als Lean-Paket eingerichtet werden und läuft nahtlos im VS-Code-Workflow von Lean.
• Benutzer können die integrierten Modelle in LeanDojo verwenden oder ihre eigenen Modelle verwenden, die lokal (mit oder ohne GPU) oder in der Cloud ausgeführt werden können.
• Dieses Tool läuft auf verschiedenen Plattformen, einschließlich Linux, macOS und Windows WSL.

Um LLM für Lean-Anwender zugänglicher zu machen, hofft Lean Copilot, eine positive Rückkopplungsschleife in Gang zu setzen und zu beweisen, dass Automatisierung zu besseren Daten führt und letztendlich die mathematische Leistung von LLM verbessert.

Demonstration des Copilot-Effekts

Sie können Lean Copilot gemäß dem offiziellen Tutorial konfigurieren. Nachdem die Konfiguration abgeschlossen ist, können Sie das Experiment starten. Der Autor des Projekts stellt auch einige offizielle Beispiele als Referenz zur Verfügung

empfohlene Lösungen. Nach dem Import von LeanCopilot können Sie suggest_tactics verwenden, um empfohlene Lösungen zu generieren. Während der Verwendung können Sie auch auf die empfohlene Lösung klicken und diese im Beweis verwenden (siehe Bild unten)

Sie können ein Präfix wie simp verwenden, um die generierte Strategie einzuschränken

Nach Beweisen suchen. Verwenden Sie search_proof, um LLM-generierte Richtlinien mit Aesop (dem White-Box-Automatisierungsprojekt von Lean 4) zu kombinieren, um nach mehreren Richtliniennachweisen zu suchen. Sobald Sie den Beweis gefunden haben, können Sie auf die Strategie klicken, um sie in den Editor einzufügen

Neu geschriebener Inhalt: Die Wahl einer Prämisse ist eine wichtige Strategie. Der Zweck dieser Strategie besteht darin, eine Liste potenziell nützlicher Räumlichkeiten abzurufen. Derzeit verwendet Lean Copilot das Suchtool in LeanDojo, um Prämissen aus dem festen Snapshot von Lean und mathlib4 (d. h. der Lean 4-Mathebibliothek) auszuwählen.

Sie können LLM ausführen. Ganz gleich, ob es um die Beweisführung von Theoremen oder andere Argumentationen geht, Sie können LLM in Lean betreiben. Sie können jedes Modell lokal oder remote ausführen (siehe Bring Your Own Model)

Einige fortgeschrittene Verwendungsmöglichkeiten werden auch im Projekt erwähnt, um mehr zu erfahren.

Das obige ist der detaillierte Inhalt vonTerence Tao nutzt den groß angelegten Modellbeweisassistenten Lean, um seine Vorliebe zu zeigen. Für weitere Informationen folgen Sie bitte anderen verwandten Artikeln auf der PHP chinesischen Website!