Prueba asistida por ordenador

De Wikipedia, la enciclopedia libre
Ir a la navegación Ir a la búsqueda
"Averiguar si cualquier mapa se puede pintar con cuatro colores, de forma que cualquier par de regiones contiguas estén pintadas de diferentes colores". En 1976, K. Appel y V. Haken, con la ayuda de cálculos de ordenador diseñados al efecto, demostraron que es posible colorear cualquier mapa con cuatro colores

Una prueba asistida por ordenador es una demostración matemática que ha sido generada al menos parcialmente utilizando una computadora.

La mayoría de las pruebas asistidas por ordenador hasta la fecha han sido desarrollos de pruebas por exhaustación de un elevado número de casos asociados a un teorema matemático. La idea es usar un programa de computadora para realizar cálculos largos 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 que se verificó con un programa informático.

También se han realizado intentos en el área de investigación de la inteligencia artificial para crear pruebas más pequeñas, explícitas y nuevas de teoremas matemáticos de abajo hacia arriba usando técnicas de razonamiento automático, como la búsqueda heurística. Tales demostraciones automáticas de teoremas han demostrado numerosos nuevos resultados y han encontrado nuevas pruebas para teoremas conocidos. Además, la demostración interactiva de teoremas permite a los matemáticos desarrollar pruebas legibles para los seres humanos que, no obstante, se verifican formalmente para verificar su exactitud. Dado que estas pruebas son generalmente revisables por los matemáticos (aunque no sin dificultades, como con la prueba de la conjetura de Robbins) no comparten las implicaciones controvertidas de las pruebas asistidas por ordenador mediante agotamiento.

Métodos[editar]

Un método para usar computadoras en pruebas matemáticas es por medio de los sistemas denominados validación numérica o rigor numérico. Esto significa calcular numéricamente, pero con rigor matemático. Se usa de principios aritméticos y la inclusión con valores establecidos para garantizar que la salida de valor fijo de un programa numérico encierre la solución del problema matemático original. Esto se hace controlando, adjuntando y propagando los errores de redondeo y truncamiento usando, por ejemplo, intervalos aritméticos. Más precisamente, si se reduce el cálculo a una secuencia de operaciones elementales, como (+, -, *, /). En una computadora, el resultado de cada operación elemental se completa con su precisión de cálculo. Sin embargo, puede construirse un intervalo proporcionado por límites superiores e inferiores sobre el resultado de una operación elemental. A continuación se procede reemplazando números por intervalos y realizando operaciones elementales entre dichos intervalos de números representables.

Objeciones filosóficas[editar]

Las pruebas asistidas por ordenador son objeto de cierta controversia en el mundo de las matemáticas, siendo Thomas Tymoczko uno de los primeros en formular objeciones. Aquellos que se adhieren a los argumentos de Tymoczko creen que las largas pruebas asistidas por ordenador no son, en cierto sentido, demostraciones reales porque implican tantos pasos lógicos que no son prácticamente verificables por los seres humanos, y que se está pidiendo a los matemáticos que reemplacen de forma efectiva la deducción lógica de axiomas asumidos por la confianza en un proceso computacional empírico, que se ve potencialmente afectado por errores en el programa de la computadora, así como también por defectos en el entorno de tiempo de ejecución y del propio dispositivo.[1]

Otros matemáticos creen que las largas pruebas asistidas por computadora deben considerarse como cálculos, en lugar de pruebas: el algoritmo de prueba en sí mismo debe probarse como válido, de modo que su uso puede considerarse como una mera verificación. Los argumentos de que las pruebas asistidas por ordenador están sujetas a errores en sus programas fuente, compiladores y dispositivos electrónicos pueden resolverse proporcionando una prueba formal de corrección del programa informático (un enfoque que se aplicó con éxito al teorema de los cuatro colores en 2005), así como replicar el resultado usando diferentes lenguajes de programación, diferentes compiladores y diferentes tipos de computadora.

Otra forma posible de verificar las pruebas asistidas por ordenador es generar sus pasos de razonamiento en una forma legible por una máquina, y luego usar una demostración automática de teoremas para comprobar su corrección. Este enfoque de usar un programa de computadora para probar que otro programa es correcto no atrae a los escépticos de las pruebas con ordenador, que lo ven como una capa de complejidad añadida sin abordar la necesidad percibida de la comprensión humana.

Otro argumento en contra de las pruebas asistidas por ordenador es que carecen de belleza matemática, que no proporcionan ideas ni conceptos nuevos y útiles. De hecho, este es un argumento que podría avanzarse contra cualquier prueba prolongada por agotamiento.

Una cuestión filosófica adicional planteada por las pruebas asistidas por ordenador es si convierten las matemáticas en una ciencia cuasi-empírica, en la que el método científico se vuelve más importante que la aplicación de la razón pura en el área 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 son un ejercicio de manipulación de símbolos formales. También plantea la cuestión de si, de acuerdo con el punto de vista platónico, todos los objetos matemáticos posibles en algún sentido "ya existen"; si las matemáticas asistidas por ordenador son una ciencia observacional como la astronomía, en lugar de una experimental como la física o la química. Curiosamente, esta controversia dentro de las matemáticas está ocurriendo al mismo tiempo que las preguntas que se hacen en la comunidad de la física sobre si la física teórica del siglo veintiuno se está volviendo demasiado matemática y está dejando atrás sus raíces experimentales.

El campo emergente de las matemáticas experimentales dilucida este debate de frente, al enfocarse en los experimentos numéricos como su herramienta principal para la exploración matemática.

Teoremas en venta[editar]

En 2010, los académicos de la Universidad de Edimburgo ofrecieron a las personas la posibilidad de "comprar su propio teorema" creado a través de una prueba asistida por ordenador. Este nuevo teorema llevaría el nombre del comprador.[2][3]

Ejemplos[editar]

Teoría de números[editar]

Debido a que la teoría de números opera en gran medida con números enteros, el uso de cálculos basados ​​en la evidencia en este campo resulta ser muy fructífera.

  • Se afirma que el número de Mersenne es un número primo. Este hecho puede verificarse teóricamente mediante razonamientos humanos, pero de forma práctica solo con el uso de tecnología informática.
  • Leonhard Euler formuló la conjetura de que la ecuación no tiene solución en números enteros positivos. Sin embargo, posteriormente se demostró que hay al menos una solución:
, , , , .

Esta solución se encontró usando un procedimiento de búsqueda de fuerza bruta por ordenador.[4]

Teoría de grafos[editar]

Uno de los éxitos más famosos en la aplicación de pruebas informáticas en teoría de grafos es la solución del teorema de los cuatro colores. Este famoso problema se planteó en 1852, y se formula de la siguiente manera: "Averiguar si cualquier mapa se puede pintar con cuatro colores, de forma que cualquier par de regiones contiguas estén pintadas de diferentes colores". En 1976, K. Appel y V. Haken, con la ayuda de cálculos diseñados al efecto, demostraron que es posible colorear cualquier mapa con cuatro colores.

Hidrodinámica[editar]

El Instituto Kéldysh de Matemática Aplicada convirtió la hidrodinámica en un objeto sistemático de investigación con el uso de cálculos asistidos por ordenador bajo la dirección de Konstantín Ivánovich Babenko. Un ejemplo es el siguiente teorema:.[5]

  • Teorema: Cuando y el problema espectral de Orr-Sommerfeld tiene un valor propio que se encuentra en el semiplano . En consecuencia, en la formulación lineal de estos parámetros, el flujo de Poiseuille es inestable.

Lista de teoremas probados con la ayuda de programas de ordenador[editar]

La inclusión en esta lista no implica que exista una prueba formal documentada por computadora, sino que un programa de ordenador ha estado involucrado de alguna manera en su demostración. Véanse los artículos principales para más detalles.

Véase también[editar]

Referencias[editar]

  1. Tymoczko, Thomas (1979), «The Four-Color Problem and its Mathematical Significance», The Journal of Philosophy 76 (2): 57-83, doi:10.2307/2025976 .
  2. «Herald Gazette article on buying your own theorem». Herald Gazette Scotland. noviembre de 2010. Archivado desde el original el 21 de noviembre de 2010. 
  3. «School of Informatics, Univ.of Edinburgh website». School of Informatics, Univ.of Edinburgh. abril de 2015. 
  4. Babenko K.I. (1986). Fundamentos del análisis numérico. Moscú: Ciencia. 
  5. Babenko K.I., Vasiliev M.M. (1983). Cálculos auxiliares en el problema de la estabilidad del flujo de Poiseuille 273 (6) (DAN URSS edición). pp. 1289-1294. 
  6. Cesare, Chris (1 de octubre de 2015). «Maths whizz solves a master’s riddle». Nature. pp. 19-20. doi:10.1038/nature.2015.18441. 
  7. Lamb, Evelyn (26 de mayo de 2016). «Two-hundred-terabyte maths proof is largest ever». Nature 534: 17-18. PMID 27251254. doi:10.1038/nature.2016.19990. 

Lecturas adicionales[editar]

  • Lenat, D.B., (1976), AM: Un enfoque de inteligencia artificial para el descubrimiento en matemáticas como búsqueda heurística, Ph.D. Tesis, STAN-CS-76-570, y Heuristic Programming Project Report HPP-76-8, Stanford University, AI Lab., Stanford, CA.

Enlaces externos[editar]