Hilo de Ben Goertzel (@bengoertzel)

Acerca del uso de LLM para ayudar a demostrar problemas matemáticos difíciles (existencia+unicidad de Navier-Stokes, P/reddit.com/r/singularity/…to https://t.co/tOvR1LbfZ6 sobre el uso de IA por parte de algunas personas de DeepMind para ayudar a demostrar el teorema de existencia y unicidad de Navier-Stokes, me motiva a señalar que hace un par de meses intenté demostrar este teorema con la ayuda de detalles de un par de LLM, https://t.co/uPCZ9GRnz5 La idea de la demostración fue mía: básicamente, usar la aplicación de la ecuación HJB (que he usado mucho en trabajos recientes de IA) a la ecuación de Navier-Stokes, para así aplicar los resultados de existencia/uniformidad de HJB a NS. Sin embargo, los detalles son bastante complejos y no tenía tiempo para analizarlos personalmente, por lo que los LLM me resultaron muy útiles. Dicho esto, son asuntos delicados y no puedo asegurar al 100% que no haya ninguna brecha... Lo dejé de lado porque trabajar en la IA general me pareció más prioritario. Pensé en intentar convertirlo en una solución Lean integral, pero aún no tenía tiempo para hacerlo... Casi al mismo tiempo, también aproveché algo de ayuda de LLM para completar los detalles de una idea que tenía sobre cómo demostrar P/=NP usando una variación de la debilidad cuántica (una herramienta conceptual/matemática que desarrollé como parte de mi trabajo en AGI, generalizando la noción de debilidad de Michael Timothy Bennett como una alternativa a la navaja de Occam tradicional). https://t.co/vKP3grPtbV Nuevamente, trabajar hacia una AGI requiere mucho tiempo y no he tenido tiempo para hacer una formalización completa (aunque obviamente los LLM también ayudan con eso...) y como con cualquier prueba monstruosa como esta, podría haber una brecha que no estoy viendo... No he estado haciendo ruido sobre estos esfuerzos porque quería esperar para formalizar y verificar completamente las cosas, pero ahora que hay ruido de otros sobre esfuerzos similares, pienso, bueno, lo que sea... Parte de mi objetivo al abordar estos complejos problemas matemáticos [mi doctorado fue en matemáticas, aunque rápidamente me decanté por la IA] ha sido pensar en cómo usar eficazmente nuestro sistema proto-AGI Hyperon como "controlador" para los LLM en este tipo de trabajo. Es decir, en este tipo de trabajo, una mente creativa con visión de futuro debe aportar ideas para la prueba, un LLM debe trabajar en los detalles y, posteriormente, Lean u otro marco de trabajo de ITP debe realizar una verificación formal completa. El papel que espero que Hyperon pueda desempeñar aquí es el de "mente creativa con visión de futuro"... Pero en estos intentos de prueba que acabo de publicar, he sido yo, no Hyperon, quien ha intentado desempeñar este papel ;)