Lean4 half dabei, einen kleinen Fehler in einer aktuellen Arbeit von Terence Tao zu entdecken

 (mathstodon.xyz/@tao)
3 Punkte von GN⁺ 2023-10-28 | 1 Kommentare | Auf WhatsApp teilen
  • Terence Tao entdeckte während seines Lean4-Formalisierungsprojekts einen kleinen, aber nicht belanglosen Fehler in einer Arbeit
  • Der Fehler zeigte sich in der Argumentation auf Seite 6 des arXiv-Papers 2310.05328, wobei 1/2 log((n - 1)/(n - k - 1)) für n = 3, k = 2 divergiert
  • Das Problem ist auf kleine n-Werte beschränkt; für n >= 8 funktioniert die bisherige Argumentation, und kleine n können direkt mit einer gröberen Methode behandelt werden
  • Lean verlangte einen Beweis für 0 < n - 3, aber als Annahme lag nur n > 2 vor, sodass die Taktik linarith den nötigen Widerspruch nicht herleiten konnte
  • Tao will einige numerische Konstanten anpassen, um die Argumentation zu korrigieren, und in der neuen Version eine Fußnote ergänzen, dass die Ungenauigkeit der früheren Argumentation beim Versuch der Lean-Formalisierung entdeckt wurde

Ein durch die Lean4-Formalisierung aufgedeckter Fehler

  • Terence Tao entdeckte im Zuge seines Lean4-Formalisierungsprojekts, dass seine Arbeit einen kleinen, aber nicht belanglosen Bug enthält
  • Formalisiert werden sollte die Argumentation auf Seite 6 des arXiv-Papers 2310.05328
  • Der problematische Ausdruck hat die folgende Form
    • 1/2 log((n - 1)/(n - k - 1))
  • Für n = 3, k = 2 divergiert dieser Ausdruck

Umfang des Fehlers und Art der Korrektur

  • Dieses Problem tritt nur bei kleinen n-Werten auf
    • Für n >= 8 funktioniert die betreffende Argumentation weiterhin
    • Kleine n lassen sich direkt mit einer gröberen Methode behandeln, allerdings mit schlechteren Konstanten
  • Tao geht davon aus, dass sich die Argumentation durch Anpassung einiger numerischer Konstanten auf der betreffenden Seite korrigieren lässt
  • In die neue Version der Arbeit will er eine Fußnote aufnehmen, dass die frühere Argumentation leicht ungenau war und dies beim Versuch entdeckt wurde, sie in Lean zu formalisieren

Die konkrete Stelle, an der Lean stockte

  • An der Stelle, an der die Formalisierung scheiterte, verlangte Lean den Beweis von 0 < n - 3
    • Die einzige verfügbare Annahme war n > 2
    • Die Taktik linarith konnte aus der Negation von 0 < n - 3 keinen Widerspruch ableiten

Verwandte Beiträge

1 Kommentare

 
GN⁺ 2023-10-28
Hacker-News-Kommentare

  • Er hat Anfang dieses Monats begonnen, Lean4 mithilfe von GPT-4 zu lernen: https://mathstodon.xyz/@tao/111208692505811257
    Viele seiner Mastodon-Beiträge in diesem Monat drehten sich um seinen Lernfortschritt, und es ist ein interessantes Beispiel dafür, wie sehr Large Language Models sogar die Arbeit von Spitzenleuten beschleunigen können

    • Auch wenn man nicht programmieren kann, können Menschen mit guter Kommunikationsfähigkeit mit Large Language Models schnell funktionierende Automatisierungen bauen
      Interessanterweise könnten solche Tools die Ungleichheit sogar vergrößern, wenn nur Hochqualifizierte sie effektiv nutzen
    • GPT-4 ist erstaunlich. Heutzutage nutze ich Google kaum noch, wenn ich mit einer Programmierfrage anfange
    • Ich stimme bis zu einem gewissen Grad zu, aber Terry ist eine so außergewöhnliche Person, dass ich es schwierig finde, diesen Fall zu verallgemeinern. Natürlich ist er auch ein großzügiger und bescheidener Mensch
    • Für die Elite wird es leicht zu einem 100x-Tool. Die besten Ingenieure sind jetzt Menschen mit 10000x Produktivität

  • Wenn man einen einfachen Einstieg in Lean4 sucht, ist das Natural Number Game gut: https://adam.math.hhu.de/#/g/hhu-adam/NNG4
    Wenn man ohne Spiel nur lesen möchte, dann hier: https://lean-lang.org/theorem_proving_in_lean4/introduction.html

    • Ich bin Anfänger und frage mich: Wie unterscheidet sich Lean4 von TLA+ oder Alloy? Ich frage mich auch, ob das überhaupt sinnvolle Vergleichsobjekte sind
      Anfangs hatte ich Alloy als Allow geschrieben

  • Vor einigen Jahren suchte ich nach Möglichkeiten, Fehler in den Programmen zu reduzieren, die ich schreibe, und stieß auf Lamports TLA+. Ich lernte, formale Spezifikationen zu schreiben, indem ich das Verhalten von Programmen als Zustandsmaschinen betrachtete
    TLA+ hat mir geholfen, Abstraktionen klar zu verstehen, und später entdeckte ich auch die Reihe Software Foundations, in der man mit dem Coq-Proof-Assistant formal korrekte Software erstellt. Die Übungen waren wie kleine Spiele aufgebaut, daher hat es ziemlich Spaß gemacht, sie zu lösen: https://softwarefoundations.cis.upenn.edu/

    • Code-Korrektheit ist zu einer verlorenen Kunst geworden. Die Anforderung, abstrakt zu denken, schreckt viele Entwickler ab
      Formale Spezifikationen als High-Level-Abstraktion konzentrieren sich auf eine eigene Sprache zur Beschreibung von Code, während Code Contracts als Low-Level-Abstraktion eher darauf hinauslaufen, Verifikationslogik durch ein besseres Modell zu ersetzen. In C# gab es einmal Code Contracts[1], ein einfacher, aber mächtiger Ansatz, bei dem Verträge zur Compile-Zeit mit dem Z3-SMT-Solver[2] geprüft wurden. Einige Jahre später wurde es jedoch eingestellt[3], und mit der Entfernung aus der .NET Runtime war es praktisch vorbei. Das Nächstliegende in C# ist derzeit vermutlich Dafny[4], und die C#-Entwicklung überlegt weiterhin, wie man so etwas direkt in die Sprache aufnehmen könnte[5]
      [1] https://www.microsoft.com/en-us/research/project/code-contracts/
      [2] https://github.com/Z3Prover/z3
      [3] https://github.com/microsoft/CodeContracts
      [4] https://github.com/dafny-lang/dafny
      [5] https://github.com/dotnet/csharplang/issues/105
    • Mich würde interessieren, ob du dir auch Idris2 angesehen hast. Immer wenn ich solche Theorem Prover sehe, habe ich das Gefühl, dass es eine Impedanzfehlanpassung zur allgemeinen Programmierung gibt
      Idris2 scheint eine Allzwecksprache anzustreben und zugleich ein weiterentwickeltes Typsystem für Theorem Proving zu bieten: https://github.com/idris-lang/Idris2
    • Ich hatte mit Software Foundations dieselbe positive Erfahrung
      Es gibt auch ein gewissermaßen davon abgeleitetes Buch, das statt Coq Agda verwendet: https://plfa.github.io/
      Ich habe es noch nicht gelesen, aber es steht auf meiner Liste, und ich denke, Agda oder Idris dürften sich eher wie Programmiersprachen anfühlen als Coq

  • Abhängige Typen finde ich wirklich vielversprechend. Allerdings dürfte es vorerst schwierig sein, sie zu bekommen
    Dependent Haskell ist in Arbeit, aber es heißt, dass es schwierig ist, so etwas nachträglich in eine bestehende Sprache einzubauen. Auch der Idris-Entwickler sagte, er hoffe, dass Idris als Modell für andere Sprachen dient; eine Mainstream-Adoption scheint aber schwierig. Coq, Agda und F* sind ebenfalls nicht als Allzwecksprachen entworfen. Die Compiler-Implementierung ist komplex, und die Syntax kann ausführlich werden, aber was ich möchte, ist Einfachheit. Ich will alles, was ich über Eingaben und Ausgaben weiß, kodieren können. In heutigen Mainstream-Sprachen weiß man über Argumente oder Ausgaben oft mehr, als das Typsystem ausdrücken lässt

    • Ich teile die Begeisterung für abhängige Typen völlig, aber anders als bei den Typsystemen, die wir gewohnt sind, sind Theoreme über abhängige Typen viel schwieriger zu beweisen, sodass sie für den Einsatz im gesamten Programm nicht besonders bequem wirken
      Schön wäre ein gradueller Ansatz wie bei TypeScript, bei dem man an beliebigen Stellen Informationen über Werteinschränkungen auf Typebene hinzufügen kann, ohne überall alles beweisen zu müssen
    • Einfach erklärt bedeutet abhängige Typisierung, dass der Typ einer Variablen vom Wert einer anderen Variablen abhängen kann
      Wenn man zum Beispiel eine Liste von Zahlen und zugleich ihre Länge kennt, kann man mit abhängigen Typen einen Listentyp erstellen, der die Länge explizit enthält, und zur Compile-Zeit garantieren, dass Operationen diese Länge einhalten. Wenn eine Funktion so spezifiziert ist, dass sie nur Listen der Länge 3 annimmt, und man ihr eine Liste der Länge 4 übergibt, kompiliert das nicht, sodass der Fehler vor der Ausführung abgefangen wird. Es fühlt sich an wie eine zusätzliche Sicherheitsschicht, die Typen ausdrucksstärker macht und sogar komplexe Beziehungen zwischen Variablen kodiert

  • Wenn einer der brillantesten Köpfe unserer Generation seine Arbeitsbreite durch die Kombination aus Large Language Models und automatischem Beweisen erweitern kann, sieht die Zukunft dieser Technologiekombination sehr vielversprechend aus.
    Am Anfang steht das Beheben von Bugs, dann hilft sie bei der Verifikation, und am Ende dürfte sie neue Entdeckungen vorantreiben und Grenzen verschieben. Wir brauchen einen Begriff für das Phänomen, dass eine Dynamik wie das Mooresche Gesetz Bereiche „infiziert“, die ursprünglich keine solche kumulative Eigenschaft hatten. Als zusätzlicher Kontext: Terence Tao nutzt Copilot, um Lean zu lernen: https://mathstodon.xyz/@tao/111271244206606941
    Ohne Copilot hätte er es wohl auch gekonnt, aber vielleicht hätte ihn die Reibung beim Annehmen eines neuen Werkzeugs gar nicht erst anfangen lassen. Large Language Models haben in solchen Situationen als „Fahrrad für den Geist“ großes Potenzial.

    • Lean 4 ist eine Programmiersprache und ein Theorem Prover und hat meines Wissens nichts mit Large Language Models zu tun.
    • Large Language Models sind Compiler für natürliche Sprachen wie Englisch.

  • Vor ein paar Jahren habe ich auch einmal in einem Beitrag auf Terence Taos Mathe-Blog einen Bug gefunden. Ich habe ihn darauf hingewiesen, er hat ihn behoben und sich bedankt.
    Auf die Titelseite von Hacker News hat es das natürlich nicht geschafft.

  • Ich war besorgt, weil ich dachte, Lean4 sei noch ein weiteres Large Language Model, tatsächlich ist es aber ein ziemlich robustes und zuverlässiges Werkzeug.

    • Wenn es Terence Tao dabei hilft, Bugs in Arbeiten zu finden, ist es nach meinen Maßstäben robust und zuverlässig genug.
    • Die Lean-4-Community ist ziemlich optimistisch, was die Kombination von Large Language Models und Theorem Provern für Beweisassistenz und Formalisierung angeht.
    • Wenn die Nachricht gelautet hätte: „Terry Tao nutzt ChatGPT mit großem Nutzen zum Beweisen neuer Theoreme“, wäre das für mich persönlich wohl eine größere Neuigkeit gewesen.
    • Er berichtet, dass Copilot bei Formalisierungsarbeit nützlich ist: https://mathstodon.xyz/@tao/111271244206606941

  • Ich frage mich, ob man formale Beweisprüfer wie den Lean-Beweisprüfer mit Sprachmodellen kombinieren kann, die synthetische Vermutungs-Beweis-Paare in einer formalen Sprache wie Lean erzeugen.
    Mit dem Lean-Beweisprüfer ließen sich die von einem Sprachmodell geschriebenen synthetischen Beweise automatisch auf Korrektheit prüfen, und diese Information könnte als Reward-Signal für Reinforcement Learning dienen, das auf das ursprüngliche Sprachmodell angewendet wird, damit es bessere Beweise schreibt. Alternativ könnte man die korrekten synthetischen Beweise aus früheren Runden als Trainingsdaten verwenden, um ein neues Modell zu trainieren. Man könnte das Ganze auch adversarialer gestalten: Aufteilung in ein Modell zur Erzeugung von Vermutungen und ein Modell für Beweise/Gegenbeweise, plus ein weiteres Modell, das vorhersagt, ob ein synthetischer Beweis vom Lean-Beweisprüfer verifiziert wird. Je niedriger die vorhergesagte Wahrscheinlichkeit für die richtige Antwort ist, desto größer wäre die Belohnung für das beweiserzeugende Modell, wenn es tatsächlich einen korrekten Beweis liefert. Fügt man schließlich ein Modell hinzu, das die Belohnung vorhersagt, die das beweiserzeugende Modell für eine bestimmte synthetische Vermutung erhalten würde, wird das Modell zur Erzeugung von Vermutungen dafür belohnt, Vermutungen mit hoher erwarteter Belohnung zu erstellen, die für das beweiserzeugende Modell weder zu schwer noch zu leicht sind. Das Gesamtsystem könnte immer schwierigere synthetische Beweise hervorbringen, was zu besserem Selbsttraining des beweiserzeugenden Modells führen kann. Im Prinzip ließe sich das bis zu übermenschlichen Fähigkeiten bei der Beweiserzeugung skalieren, ähnlich wie GANs oder Self-Play bei AlphaGo Zero. Der schwierige Teil ist das anfängliche Bootstrapping: Für das erste Training des generativen Modells braucht man von Menschen bereitgestellte Lean-Beweisdaten. Sobald die synthetischen Beweise aber gut genug sind, könnte das System sein Selbsttraining automatisch fortsetzen

  • Frühere Hintergründe dazu, wie Tao auf diesem Weg Tools auf Basis großer Sprachmodelle, darunter GPT-4, eingesetzt hat, finden sich hier: https://mathstodon.xyz/@tao/111233986893287137

  • Seinen Fortschritt kann man auch auf GitHub verfolgen: https://github.com/teorth/symmetric_project/