Búsqueda · 28 momentos en 13 episodios
Ignacio CrespoBorja TosarJosé EdelsteinIsabel CorderoFrancis VillatoroHéctor Socaserrores en antecedentes astra openaidemostraciones matemáticas nielsenconocimiento matemático previo de máquinasNielsenFrancis VillatoroAstraOpenAILeanmedallas FieldsAristóteles
Conocimiento Matemático previo de máquinas
Ep565: Introgresión; Eclipse; Inestabilidad Kelvin-Helmholtz; Piezoquiralidad
6 de agosto de 20263 momentos
Con
0:000:301:001:302:002:303:003:34
Francis Villatoro explica que en las demostraciones matemáticas realizadas por máquinas como Astra de OpenAI, es crucial revisar los antecedentes incluidos, ya que pueden contener errores a pesar de basarse en conocimiento matemático previo.
…líneas y te lo tienes que leer con extremo cuidado porque cualquier pequeña desviación de lo que es el rigor matemático invalida automáticamente la prueba. No, pero es que Lean lo ha verificado, no, perdona, Lean lo ha verificado si en un código en Lean. Es muy importante, digamos, darle los antecedentes de la demostración. En una demostración matemática entre humanos, yo asumo que el que lee la demostración ya conoce los antecedentes. Yo me ahorro todo eso, porque ya los conoce. Pero en una demostración hecha por la máquina desde cero, se incluyen esos antecedentes y en esos antecedentes, ese conocimiento matemático conocido, puede haber errores. Y este matemático, Nielsen, ha descubierto. en una de las demostraciones, la de la conjuntura de Cornes que hay dos errores. Corners requiere dos condiciones, la propiedad T, que el grupo sea ICC, y resulta que en el código Lean, donde se definen esas propiedades, se cometen errores. Llámale…
Significado #1 · Palabras #1
Francis Villatoro explica que en las demostraciones matemáticas realizadas por máquinas como Astra de OpenAI, es crucial revisar los antecedentes incluidos, ya que pueden contener errores a pesar de basarse en conocimiento matemático previo.
Habla: Francis VillatoroSignificado #1 · Palabras #1errores en antecedentes astra openaidemostraciones matemáticas nielsenconocimiento matemático previo de máquinas…líneas y te lo tienes que leer con extremo cuidado porque cualquier pequeña desviación de lo que es el rigor matemático invalida automáticamente la prueba. No, pero es que Lean lo ha verificado, no, perdona, Lean lo ha verificado si en un código en Lean. Es muy importante, digamos, darle los antecedentes de la demostración. En una demostración matemática entre humanos, yo asumo que el que lee la demostración ya conoce los antecedentes. Yo me ahorro todo eso, porque ya los conoce. Pero en una demostración hecha por la máquina desde cero, se incluyen esos antecedentes y en esos antecedentes, ese conocimiento matemático conocido, puede haber errores. Y este matemático, Nielsen, ha descubierto. en una de las demostraciones, la de la conjuntura de Cornes que hay dos errores. Corners requiere dos condiciones, la propiedad T, que el grupo sea ICC, y resulta que en el código Lean, donde se definen esas propiedades, se cometen errores. Llámale…
Francis Villatoro explica la evolución en la generación de demostraciones matemáticas por parte de la inteligencia artificial Astra de OpenAI, contrastando el proceso anterior con el actual.
Habla: Francis VillatoroPalabras #16conversor aristóteles a lenguaje leanverificación en lenguaje lean…a popularizar, ya está empezando a haber gente que está diciendo: No, no, no, no, yo no quiero que Charles G.P.T. me explique la demostración, porque yo no tengo ni zorrea, no lo voy a entender, quiero que me genere el código Lean automáticamente, porque las Demostraciones a principios de este año se generaban en lenguaje humano, hecho por la máquina, y entonces tú usabas Aristóteles, un conversor que te convertía esa demostración al lenguaje Lean, y después la verificabas en Lean. Se ha verificado en Lean y además entiendo el lenguaje humano con el que se ha descrito. Pero es que ahora no, ahora ha generado directamente Lean, el lenguaje máquina, entre comillas, incomprensible para los humanos. En muy pocos años, todas las carreras de matemáticas del Mundo, todos los licenciados en matemática del mundo van a tener que tener un curso de un año en Lean. Todos van a tener que ser expertos en Lean, porque van a aparecer miles, decenas de miles de demostraciones en Lean. Y la única manera de gestionar eso para…
Francis Villatoro explica cómo OpenAI contrató a matemáticos reconocidos para revisar y comprender las demostraciones generadas por la máquina antes de publicar un documento.
Habla: Francis VillatoroPalabras #5contratación de matemáticos por openairevisión de demostraciones máquina openaiartículo digerido treinta páginas…Ahora sabemos que una de ellas no lo es y hay dudas de alguna de las otras O sea, estas demostraciones hay que cogerlas con mucho cuidado Pero es que la ocasión anterior, con la famosa demostración de la hipótesis de la unidad, del disco unitario o algo así, OpenAI, antes de sacar la publicación del documento, contrató a una serie de matemáticos que eran todos muy famosos, medallas Phil, gente muy famosa, para que escribieran documentos. Los matemáticos entendieron ahí trabajando con la máquina y con la gente que había hecho, los informáticos que habían hecho esto y otros matemáticos trabajaron eso y ya venía digerido y se podía entender. Y tú leías el artículo de 30 páginas y te enterabas. Pero es que ahora OpenAI no lo ha hecho. Ha dicho: ¿Para qué?, ¿para qué? Si lo que yo quiero es ganar inversión en bolsa. Si a mí las matemáticas no me importan, soy OpenAI. ¿Qué me importa a mí que las matemáticas progresen? ¿Qué me importa a mí que las…