Lean4 ayudó a encontrar un pequeño bug en un artículo reciente de Terence Tao

• Terence Tao descubrió un error pequeño pero no trivial en un artículo mientras trabajaba en un proyecto de formalización en Lean4
• El error apareció en un argumento de la página 6 del artículo de arXiv 2310.05328: 1/2 log((n - 1)/(n - k - 1)) diverge cuando n = 3, k = 2
• El problema se limita a valores pequeños de n: para n >= 8 el argumento existente funciona, y los valores pequeños de n pueden tratarse directamente con un método más burdo
• Lean pedía demostrar 0 < n - 3, pero la única hipótesis era n > 2, por lo que la táctica linarith no lograba obtener la contradicción necesaria
• Tao corrigió el argumento ajustando algunas constantes numéricas, y planea incluir en la nueva versión una nota al pie indicando que la imprecisión del argumento anterior se descubrió durante el intento de formalizarlo en Lean

---

La formalización en Lean4 reveló un error

• Terence Tao descubrió un bug pequeño pero no trivial en su artículo durante su proyecto de formalización en Lean4
• El objetivo de la formalización era un argumento de la página 6 del artículo de arXiv 2310.05328
• La expresión problemática tenía la siguiente forma:
  • 1/2 log((n - 1)/(n - k - 1))
• Esta expresión diverge cuando n = 3, k = 2

Alcance del error y forma de corregirlo

• El problema solo ocurre para valores pequeños de n
  • Para n >= 8, ese argumento sigue funcionando
  • Los valores pequeños de n pueden tratarse directamente con un método más burdo, aunque las constantes empeoran
• Tao considera que puede corregir el argumento cambiando algunas constantes numéricas de esa página
• En la nueva versión del artículo planea agregar una nota al pie indicando que el argumento anterior era ligeramente impreciso y que se descubrió al intentar formalizarlo con Lean

Punto concreto donde Lean se trabó

• En el punto donde falló la formalización, Lean exigía demostrar 0 < n - 3
  • La única hipótesis disponible era n > 2
  • La táctica linarith no pudo derivar una contradicción a partir de la negación de 0 < n - 3

[GN⁺]

Comentarios de Hacker News

• Empezó a aprender Lean4 con ayuda de GPT-4 a principios de este mes: https://mathstodon.xyz/@tao/111208692505811257
  Muchas de sus publicaciones en Mastodon de este mes trataban sobre su progreso de aprendizaje, y es un caso interesante de cuánto pueden acelerar el trabajo incluso de personas de altísimo rendimiento los modelos de lenguaje grandes

  • Incluso alguien que no sabe programar, si se comunica bien, puede crear rápidamente automatizaciones funcionales con modelos de lenguaje grandes
    Curiosamente, si solo la gente muy capacitada puede aprovechar bien estas herramientas, también podrían ampliar aún más la desigualdad
  • GPT-4 es sorprendente. Últimamente casi ya no uso Google cuando empiezo con preguntas relacionadas con programación
  • Estoy de acuerdo hasta cierto punto, pero Terry es una persona demasiado excepcional, así que me parece difícil generalizar este caso. Claro, también es una persona generosa y humilde
  • Para la élite, fácilmente se vuelve una herramienta de 100x. Ahora los ingenieros de más alto nivel son personas con 10000x de productividad

• Si quieres acercarte fácilmente a Lean4, Natural Number Game es una buena opción: https://adam.math.hhu.de/#/g/hhu-adam/NNG4
  Si prefieres solo leer y no jugar, aquí está: https://lean-lang.org/theorem_proving_in_lean4/introduction.html

  • Soy principiante y tengo curiosidad: ¿en qué se diferencia Lean4 de TLA+ o Alloy? También me pregunto si realmente son cosas comparables
    Al principio había escrito Alloy como Allow

• Hace algunos años, mientras buscaba maneras de reducir errores en los programas que escribo, conocí TLA+ de Lamport y aprendí a redactar especificaciones formales pensando el comportamiento del programa como una máquina de estados
  TLA+ me ayudó a entender con claridad la abstracción, y después también descubrí la serie Software Foundations, que usa el asistente de pruebas Coq para construir software formalmente correcto. Los ejercicios están planteados como pequeños juegos, así que fue bastante divertido resolverlos: https://softwarefoundations.cis.upenn.edu/

  • La corrección del código se ha vuelto una habilidad perdida. La exigencia de pensar de manera abstracta intimida a muchos desarrolladores
    Las especificaciones formales, que son una abstracción de alto nivel, se enfocan en un lenguaje dedicado a describir el código, mientras que los contratos de código, una abstracción de bajo nivel, se parecen más a reemplazar la lógica de validación por un mejor modelo. En C# alguna vez existió Code Contracts[1], un enfoque simple pero potente que verificaba contratos en tiempo de compilación con el solver SMT Z3[2], pero fue abandonado años después[3] y prácticamente terminó al ser removido del .NET Runtime. Lo más cercano hoy en C# probablemente sea Dafny[4], y en el desarrollo de C# todavía siguen pensando cómo incorporar algo así directamente en el lenguaje[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
  • Me pregunto si también revisaste Idris2. Cada vez que veo este tipo de demostradores de teoremas, siento que hay un desajuste con la programación general
    Idris2 parece ofrecer un sistema de tipos más avanzado para demostración de teoremas, mientras apunta a ser un lenguaje de propósito general: https://github.com/idris-lang/Idris2
  • Yo también tuve una experiencia positiva similar con Software Foundations
    También existe un libro derivado en cierta medida que usa Agda en lugar de Coq: https://plfa.github.io/
    Todavía no he podido leerlo, pero lo tengo en mi lista, y creo que Agda o Idris probablemente se sienten más como lenguajes de programación que Coq

• Los tipos dependientes realmente me entusiasman. Pero parece que por ahora será difícil que lleguen
  Dependent Haskell está en marcha, pero dicen que es difícil encajarlo después en un lenguaje existente, y el creador de Idris también dijo que esperaba que Idris sirviera como modelo para otros lenguajes, no que tuviera adopción masiva. Coq, Agda y F* tampoco fueron diseñados como lenguajes de propósito general. Implementar el compilador es complejo y la sintaxis puede volverse verbosa, pero lo que yo quiero es simplicidad. Quiero codificar todo lo que sé sobre las entradas y salidas. En los lenguajes convencionales de hoy, muchas veces uno sabe más sobre los argumentos o los resultados de lo que el sistema de tipos permite expresar

  • Comparto por completo el entusiasmo por los tipos dependientes, pero a diferencia de los sistemas de tipos a los que estamos acostumbrados, los teoremas sobre tipos dependientes son mucho más difíciles de demostrar, así que no parece cómodo usarlos en programas completos
    Me gustaría algo gradual, como TypeScript, donde no haga falta demostrarlo todo en todas partes, sino que se pueda añadir información de restricciones de valores a nivel de tipos en ubicaciones arbitrarias
  • Una forma sencilla de explicar los tipos dependientes es que el tipo de una variable puede depender del valor de otra variable
    Por ejemplo, si conoces una lista de números y también su longitud, con tipos dependientes puedes crear un tipo de lista que incluya explícitamente esa longitud, y garantizar en tiempo de compilación que las operaciones respeten esa longitud. Si defines una función que solo acepta una lista de longitud 3 y le pasas una de longitud 4, no compilará, así que puedes detectar el error antes de ejecutar. Es como una capa adicional de comprobaciones de seguridad que hace a los tipos más expresivos y permite codificar incluso relaciones complejas entre variables

• Si una de las mentes más brillantes de nuestra generación puede ampliar su capacidad de trabajo con la combinación de modelos de lenguaje grandes y demostración automática, el futuro de esa combinación tecnológica se ve muy prometedor
  Empieza corrigiendo bugs, luego ayuda con la verificación y, al final, probablemente impulse nuevos descubrimientos y expanda los límites. Hace falta un término para el fenómeno en que dinámicas tipo ley de Moore “infectan” campos que originalmente no tenían esa clase de naturaleza acumulativa. Como contexto adicional, Terence Tao está usando Copilot para aprender Lean: https://mathstodon.xyz/@tao/111271244206606941
  Seguramente habría podido hacerlo sin Copilot, pero tal vez no habría empezado por la fricción de adoptar una herramienta nueva. Los modelos de lenguaje grandes tienen un gran potencial en este tipo de situaciones de “bicicleta para la mente”

  • Lean 4 es un lenguaje de programación y un demostrador de teoremas, y hasta donde sé no tiene relación con los modelos de lenguaje grandes
  • Los modelos de lenguaje grandes son compiladores para lenguaje natural como el inglés

• Hace unos años también encontré un bug en una entrada del blog de matemáticas de Terence Tao. Se lo comenté, lo corrigió y hasta me dio las gracias
  Claro, eso no me llevó a la portada de Hacker News

  • Para quienes tengan interés, escribí con más detalle en mi post del blog: https://news.ycombinator.com/item?id=38040982

• Me preocupé al pensar que Lean4 era otro modelo de lenguaje grande, pero en realidad resultó ser una herramienta bastante sólida y confiable

  • Si ayuda a Terence Tao a encontrar bugs en artículos, para mí eso ya es prueba suficiente de que es sólida y confiable
  • La comunidad de Lean 4 es bastante optimista sobre combinar modelos de lenguaje grandes y demostradores de teoremas para asistencia en pruebas y formalización
  • Si la noticia hubiera sido “Terry Tao usa ChatGPT de forma muy útil para nuevas demostraciones de teoremas”, personalmente me habría parecido una noticia aún mayor que esta
  • Él considera que Copilot es útil para el trabajo de formalización: https://mathstodon.xyz/@tao/111271244206606941

• Me pregunto si se podría combinar un verificador formal de pruebas como el verificador de pruebas Lean con un modelo de lenguaje que genere pares sintéticos de conjetura-demostración en un lenguaje formal como Lean.
  Un verificador de pruebas Lean podría validar automáticamente si una prueba sintética escrita por un modelo de lenguaje es correcta, y esa información podría usarse como señal de recompensa de aprendizaje por refuerzo aplicada al modelo de lenguaje original para hacer que escriba mejores pruebas. O también se podrían usar las pruebas sintéticas correctas de rondas anteriores como datos de entrenamiento para entrenar un nuevo modelo. Incluso podría hacerse de forma más adversarial. Se dividiría en un modelo generador de conjeturas y un modelo de prueba/refutación, y se añadiría un modelo que prediga si la prueba sintética será verificada por el verificador de pruebas Lean. Cuanto menor se prediga la probabilidad de acertar, mayor recompensa recibiría el modelo generador de pruebas cuando efectivamente produzca una prueba correcta. Finalmente, si se añade un modelo que prediga la recompensa que recibirá el modelo generador de pruebas para una conjetura sintética concreta, el modelo generador de conjeturas recibiría recompensa por crear conjeturas con alta recompensa esperada que no sean ni demasiado difíciles ni demasiado fáciles para el modelo generador de pruebas. Todo el sistema podría ir produciendo pruebas sintéticas cada vez más difíciles, y eso podría llevar a un mejor autoaprendizaje del modelo generador de pruebas. En principio, esto podría escalar incluso hasta una capacidad sobrehumana en generación de pruebas, y se parece a los GAN o al autojuego de AlphaGo Zero. La parte difícil es el bootstrapping inicial: para el entrenamiento inicial del modelo generador se necesitan datos de pruebas Lean proporcionados por humanos. Pero si las pruebas sintéticas llegan a ser lo bastante buenas, el sistema podría continuar automáticamente su autoaprendizaje

  • Este flujo de trabajo es un objetivo explícito de los desarrolladores de Lean 4. Incluso hay un canal en el chat oficial de Zulip que trata la interfaz entre ambos: https://leanprover.zulipchat.com/#streams/219941/Machine%20Learning%20for%20Theorem%20Proving
  • También parecería interesante entrenar este tipo de modelos con toda la literatura matemática. Daría ganas de usarlos para traducir y verificar las demostraciones de la literatura matemática en una forma verificable.
    Al final, se podría obtener un modelo que conozca todos los teoremas y todas las demostraciones correctas de la literatura matemática
  • Parece que ya hemos entrado en el mundo de la síntesis de pruebas basada en aprendizaje automático. No diría que ya exista el sistema completo descrito, pero sí hay muchos sistemas parecidos y componentes de ese tipo.
    Como etapas iniciales que parten de aprendizaje supervisado con pruebas existentes para encontrar nuevas pruebas, están TacticToe (https://arxiv.org/abs/1804.00596), Tactician (https://arxiv.org/pdf/2008.00120.pdf), CoqGym/ASTactic (https://arxiv.org/abs/1905.09381), Proverbot9001 (https://arxiv.org/abs/1907.07794), Diva (https://dl.acm.org/doi/10.1145/3510003.3510138#sec-terms) y otros. La mayoría incorpora algún tipo de modelo de lenguaje, pero si se buscan grandes modelos de lenguaje que hayan recibido atención recientemente, están GPT-f (https://arxiv.org/abs/2009.03393), Baldur (https://arxiv.org/abs/2303.04910), y COPRA (https://arxiv.org/abs/2310.04353). Aun así, por ahora estos modelos no parecen ser tan efectivos como las herramientas especializadas que no son grandes modelos de lenguaje. En la línea de aprender con aprendizaje por refuerzo más allá de las pruebas escritas por humanos están TacticZero (https://openreview.net/forum?id=edmYVRkYZv), un artículo de OpenAI (https://arxiv.org/pdf/2202.01344.pdf), rlCoP (https://arxiv.org/abs/1805.07563), trabajos de la familia HOList (https://arxiv.org/pdf/1905.10006.pdf), HyperTree Proof Search (https://arxiv.org/abs/2205.11491), además de trabajo en curso del equipo de la University of Massachusetts y mío
  • Ya hay personas haciendo esto. Un ejemplo del lado de Lean está aquí: https://morph.so/blog/the-personal-ai-proof-engineer/

• Aquí hay contexto previo sobre cómo Tao usó herramientas de grandes modelos de lenguaje, incluido GPT-4, en este proceso: https://mathstodon.xyz/@tao/111233986893287137

• Su progreso también se puede seguir en GitHub: https://github.com/teorth/symmetric_project/