Prueba asistida por computadora

Prueba matemática generada al menos parcialmente por computadora

Una prueba asistida por computadora es una prueba matemática que ha sido generada al menos parcialmente por computadora .

La mayoría de las demostraciones asistidas por computadora hasta la fecha han sido implementaciones de grandes demostraciones por agotamiento de un teorema matemático . La idea es utilizar un programa de computadora para realizar cálculos extensos y proporcionar una prueba de que el resultado de estos cálculos implica el teorema dado. En 1976, el teorema de los cuatro colores fue el primer teorema importante verificado mediante un programa de computadora .

También se han realizado intentos en el área de la investigación de la inteligencia artificial para crear nuevas pruebas más pequeñas, explícitas y nuevas de teoremas matemáticos desde abajo hacia arriba utilizando técnicas de razonamiento automatizadas como la búsqueda heurística . Estos demostradores de teoremas automatizados han demostrado una serie de resultados nuevos y han encontrado nuevas pruebas para teoremas conocidos. ^{[ cita necesaria ]} Además, los asistentes de prueba interactivos permiten a los matemáticos desarrollar pruebas legibles por humanos que, no obstante, se verifican formalmente para determinar su corrección. Dado que estas pruebas son generalmente comprobables por humanos (aunque con dificultad, como ocurre con la prueba de la conjetura de Robbins ), no comparten las implicaciones controvertidas de las pruebas por agotamiento asistidas por computadora.

Métodos

Un método para utilizar computadoras en demostraciones matemáticas es mediante los llamados números validados o números rigurosos. Esto significa calcular numéricamente pero con rigor matemático. Se utiliza la aritmética de valores establecidos y el principio de inclusión ^{[ aclarar ]} para garantizar que la salida de valores establecidos de un programa numérico incluya la solución del problema matemático original. Esto se hace controlando, encerrando y propagando errores de redondeo y truncamiento utilizando, por ejemplo, aritmética de intervalos . Más precisamente, se reduce el cálculo a una secuencia de operaciones elementales, digamos . En una computadora, el resultado de cada operación elemental se redondea con la precisión de la computadora. Sin embargo, se puede construir un intervalo proporcionado por límites superior e inferior sobre el resultado de una operación elemental. Luego se procede reemplazando números con intervalos y realizando operaciones elementales entre dichos intervalos de números representables. ^{[ cita necesaria ]} ${\displaystyle (+,-,\times ,/)}$

Objeciones filosóficas

Las demostraciones asistidas por computadora son objeto de cierta controversia en el mundo matemático, siendo Thomas Tymoczko el primero en articular objeciones. Quienes se adhieren a los argumentos de Tymoczko creen que las demostraciones extensas asistidas por computadora no son, en cierto sentido, demostraciones matemáticas "reales" porque implican tantos pasos lógicos que no son prácticamente verificables por seres humanos, y que en realidad se está pidiendo a los matemáticos que reemplazar la deducción lógica a partir de axiomas supuestos con confianza en un proceso computacional empírico, que se ve potencialmente afectado por errores en el programa de computadora, así como defectos en el entorno de ejecución y el hardware. ^[1]

Otros matemáticos creen que las demostraciones extensas asistidas por computadora deberían considerarse cálculos , más que pruebas : el algoritmo de prueba en sí debería demostrarse válido, de modo que su uso pueda considerarse como una mera "verificación". Los argumentos de que las pruebas asistidas por computadora están sujetas a errores en sus programas fuente, compiladores y hardware pueden resolverse proporcionando una prueba formal de corrección del programa de computadora (un enfoque que se aplicó con éxito al teorema de los cuatro colores en 2005) como además de replicar el resultado utilizando diferentes lenguajes de programación, diferentes compiladores y diferentes hardware informático.

Otra forma posible de verificar pruebas asistidas por computadora es generar sus pasos de razonamiento en un formato legible por máquina y luego utilizar un programa de verificación de pruebas para demostrar su exactitud. Dado que validar una prueba dada es mucho más fácil que encontrar una prueba, el programa de verificación es más simple que el programa asistente original y, en consecuencia, es más fácil ganar confianza en su exactitud. Sin embargo, este enfoque de utilizar un programa informático para demostrar que el resultado de otro programa es correcto no atrae a los escépticos de la prueba informática, quienes lo ven como una adición de otra capa de complejidad sin abordar la necesidad percibida de comprensión humana.

Otro argumento en contra de las pruebas asistidas por computadora es que carecen de elegancia matemática : que no proporcionan conocimientos ni conceptos nuevos y útiles. De hecho, éste es un argumento que podría esgrimirse contra cualquier prueba extensa por agotamiento.

Una cuestión filosófica adicional que plantean las pruebas asistidas por ordenador es si convierten las matemáticas en una ciencia casi empírica , donde el método científico se vuelve más importante que la aplicación de la razón pura en el campo de los conceptos matemáticos abstractos. Esto se relaciona directamente con el argumento dentro de las matemáticas sobre si las matemáticas se basan en ideas o "simplemente" un ejercicio de manipulación de símbolos formales. También plantea la cuestión de si, según la visión platónica , todos los objetos matemáticos posibles en algún sentido "ya existen", si las matemáticas asistidas por computadora son una ciencia observacional como la astronomía, en lugar de una ciencia experimental como la física o la química. Esta controversia dentro de las matemáticas ocurre al mismo tiempo que en la comunidad física se plantean preguntas sobre si la física teórica del siglo XXI se está volviendo demasiado matemática y está dejando atrás sus raíces experimentales.

El campo emergente de las matemáticas experimentales está enfrentando este debate de frente centrándose en los experimentos numéricos como su principal herramienta para la exploración matemática.

Aplicaciones

Teoremas demostrados con la ayuda de programas de computadora.

La inclusión en esta lista no implica que exista una prueba formal verificada por computadora, sino más bien que un programa de computadora ha estado involucrado de alguna manera. Consulte los artículos principales para obtener más detalles.

• Teorema de los cuatro colores , 1976 ^[2]
• Conjetura de universalidad de Mitchell Feigenbaum en dinámica no lineal. Probado por OE Lanford utilizando rigurosa aritmética informática, 1982
• Connect Four , 1988 – un juego resuelto
• Inexistencia de un plano proyectivo finito de orden 10, 1989
• Conjetura de la doble burbuja , 1995 ^[3]
• Conjetura de Robbins , 1996
• Conjetura de Kepler , 1998: el problema del embalaje óptimo de esferas en una caja
• Atractor de Lorenz , 2002 - 14º de los problemas de Smale demostrados por Warwick Tucker utilizando aritmética de intervalos
• Caso de 17 puntos del problema del Final Feliz , 2006
• Kouril ^{[4] [5] [6]} (entre 2006 y 2016) calculó varios números de van der Waerden utilizando un solucionador SAT basado en FPGA .
• Dureza NP de triangulación de peso mínimo , 2008
• Ahmed ^{[7] [8] [9] [10] [11]} (entre 2009 y 2014) calculó varios números de van der Waerden utilizando solucionadores SAT independientes y distribuidos basados ​​en algoritmos DPLL . Ahmed utilizó por primera vez solucionadores SAT distribuidos en grupos para demostrar w(2; 3, 17) = 279 y w(2; 3, 18) = 312 en 2010. ^[8]
• Las soluciones óptimas para el Cubo de Rubik se pueden obtener con un máximo de 20 movimientos de cara, 2010 ^[12]
• El número mínimo de pistas para un Sudoku con solución es 17, 2012
• En 2014 se resolvió un caso especial del problema de discrepancia de Erdős utilizando un solucionador SAT . Terence Tao resolvió más tarde la conjetura completa sin ayuda de una computadora. ^[13]
• Problema de triples booleanos pitagóricos resuelto utilizando 200 terabytes de datos en mayo de 2016. ^[14]
• Aplicaciones a la teoría de Kolmogorov-Arnold-Moser ^{[15] [16]}
• Propiedad de Kazhdan (T) para el grupo de automorfismo de un grupo libre de rango al menos cinco
• Schur número cinco , la prueba de que S(5) = 161 fue anunciada en 2017 por Marijn Heule y ocupaba 2 petabytes de espacio ^{[17] [18]}
• La conjetura de Keller en la dimensión 7 es el único caso restante en 2020 con una prueba de 200 gigabytes ^{[19] [20]}
• El número cromático de empaquetamiento de la cuadrícula cuadrada infinita es 15, por Subercaseaux y Heule en 2023 ^{[21] [22]} (Ver también: Problema de Hadwiger-Nelson para el número cromático del plano)

Ver también

• Verificación formal
• Teórico de la lógica
• prueba matemática
• Metamatemáticas
• Comprobación de modelos
• Diecisiete o busto
• Computación simbólica
• Numéricos validados

Referencias

1. Tymoczko, Thomas (1979), "El problema de los cuatro colores y su significado matemático", The Journal of Philosophy , 76 (2): 57–83, doi :10.2307/2025976, JSTOR  2025976.
2. Gonthier, Georges (2008), "Prueba formal: el teorema de los cuatro colores" (PDF) , Avisos de la Sociedad Matemática Estadounidense , 55 (11): 1382–1393, MR  2463991, archivado (PDF) desde el original en 2011 -08-05
3. Hass, J.; Hutchings, M.; Schlafly, R. (1995). "La conjetura de la doble burbuja". Anuncios electrónicos de investigación de la Sociedad Estadounidense de Matemáticas . 1 (3): 98-102. CiteSeerX 10.1.1.527.8616 . doi :10.1090/S1079-6762-95-03001-0. 
4. Kouril, Michal (2006). Un marco de retroceso para clústeres de Beowulf con una extensión a la computación de múltiples clústeres y la implementación de problemas de referencia Sat (tesis doctoral). Universidad de Cincinnati.
5. Kouril, Michal (2012). "Calcular el número de van der Waerden W (3,4) = 293". Enteros . 12 : A46. SEÑOR  3083419.
6. Kouril, Michal (2015). "Aprovechando los clústeres FPGA para cálculos SAT". Computación paralela: en el camino hacia la exaescala : 525–532.
7. Ahmed, Tanbir (2009). "Algunos números nuevos de van der Waerden y algunos números tipo van der Waerden". Enteros . 9 : A6. doi :10.1515/integ.2009.007. SEÑOR  2506138. S2CID  122129059.
8. Ahmed, Tanbir (2010). "Dos nuevos números de van der Waerden w(2;3,17) y w(2;3,18)". Enteros . 10 (4): 369–377. doi :10.1515/integ.2010.032. SEÑOR  2684128. S2CID  124272560.
9. Ahmed, Tanbir (2012). "Sobre el cálculo de los números exactos de van der Waerden". Enteros . 12 (3): 417–425. doi :10.1515/integ.2011.112. SEÑOR  2955523. S2CID  11811448.
10. Ahmed, Tanbir (2013). "Algunos números más de Van der Waerden". Diario de secuencias enteras . 16 (4): 13.4.4. SEÑOR  3056628.
11. Ahmed, Tanbir; Kullmann, Oliver; Snevily, Hunter (2014). "Sobre los números de van der Waerden w (2; 3, t)". Matemática Aplicada Discreta . 174 (2014): 27–51. arXiv : 1102.5433 . doi : 10.1016/j.dam.2014.05.007 . SEÑOR  3215454.
12. "El número de Dios es 20". cubo20.org . Julio de 2010 . Consultado el 18 de octubre de 2023 .
13. Cesare, Chris (1 de octubre de 2015). "El genio de las matemáticas resuelve el acertijo de un maestro". Naturaleza . 526 (7571): 19–20. Código Bib :2015Natur.526...19C. doi : 10.1038/naturaleza.2015.18441 . PMID  26432222.
14. Cordero, Evelyn (26 de mayo de 2016). "La prueba matemática de doscientos terabytes es la más grande jamás realizada". Naturaleza . 534 (7605): 17–18. Código Bib :2016Natur.534...17L. doi : 10.1038/naturaleza.2016.19990 . PMID  27251254.
15. Celletti, A.; Chierchia, L. (1987). "Estimaciones rigurosas para una teoría KAM asistida por computadora". Revista de Física Matemática . 28 (9): 2078–86. Código bibliográfico : 1987JMP....28.2078C. doi : 10.1063/1.527418.
16. Figueras, JL; Haro, A.; Luque, A. (2017). "Rigurosa aplicación asistida por computadora de la teoría KAM: un enfoque moderno". Fundamentos de la Matemática Computacional . 17 (5): 1123–93. arXiv : 1601.00084 . doi :10.1007/s10208-016-9339-3. hdl :2445/192693. S2CID  28258285.
17. Heule, Marijn JH (2017). "Schur número cinco". arXiv : 1711.08076 [cs.LO].
18. "Schur número cinco". www.cs.utexas.edu . Consultado el 6 de octubre de 2021 .
19. Brakensiek, Josué; Heule, Marijn; Mackey, Juan; Narváez, David (2020). "La resolución de la conjetura de Keller". En Peltier, Nicolás; Sofronie-Stokkermans, Viorica (eds.). Razonamiento automatizado . Apuntes de conferencias sobre informática. vol. 12166. Saltador. págs. 48–65. doi :10.1007/978-3-030-51074-9_4. ISBN 978-3-030-51074-9. PMC  7324133 .
20. Hartnett, Kevin (19 de agosto de 2020). "La búsqueda por computadora resuelve un problema matemático de hace 90 años". Revista Quanta . Consultado el 8 de octubre de 2021 .
21. Subercaseaux, Bernardo; Heule, Marijn JH (23 de enero de 2023). "El número cromático de embalaje de la cuadrícula infinita es 15". arXiv : 2301.09757 [cs.DM].
22. Hartnett, Kevin (20 de abril de 2023). "El número 15 describe el límite secreto de una cuadrícula infinita". Revista Quanta . Consultado el 20 de abril de 2023 .

Otras lecturas

• Lenat, DB (1976). AM: Un enfoque de inteligencia artificial para el descubrimiento en matemáticas como búsqueda heurística (PDF) (Doctor). Laboratorio de IA, Universidad de Stanford. STAN-CS-76-570, Informe del proyecto de programación heurística HPP-76-8.
• Meyer, KR; Schmidt, DS, eds. (2012). Pruebas asistidas por ordenador en análisis. Volúmenes IMA en matemáticas y sus aplicaciones. vol. 28. Saltador. ISBN 978-1-4613-9092-3.
• Nakao, M.; Ciruela, M.; Watanabe, Y. (2019). Métodos de verificación numérica y pruebas asistidas por computadora para ecuaciones diferenciales parciales. Serie Springer en Matemática Computacional. Saltador. ISBN 9789811376696.

enlaces externos

• Lanford, Óscar E. (1982). "Una prueba asistida por computadora de las conjeturas de Feigenbaum" (PDF) . Toro. América. Matemáticas. Soc . 6 (3): 427–434. CiteSeerX  10.1.1.434.8389 . doi :10.1090/S0273-0979-1982-15008-X.
• Furse, Edmundo (1990). ¿Por qué AM se quedó sin fuerza? (Reporte técnico). Departamento de Estudios de Computación, Universidad de Glamorgan. CS-90-4. Archivado desde el original el 17 de julio de 2012 . Consultado el 6 de septiembre de 2016 .{{cite tech report}}: Mantenimiento CS1: bot: estado de la URL original desconocido ( enlace )
• Begley, S. (16 de abril de 2018). "Las pruebas numéricas realizadas por computadora pueden ser erróneas". Pittsburgh Post-Gazette . Archivado desde el original el 16 de abril de 2018.
• "Un número especial sobre pruebas formales". Avisos de la Sociedad Matemática Estadounidense . Diciembre de 2008.