Yo, como muchas personas, soy un usuario entusiasta de software matemático como Mathematica y Maple. Sin embargo, me siento cada vez más frustrado por los muchos casos en que dicho software simplemente le da la respuesta incorrecta sin previo aviso. Esto puede ocurrir al realizar todo tipo de operaciones, desde sumas simples hasta la optimización, entre muchos otros ejemplos.
Me he estado preguntando qué se podría hacer con este grave problema. Lo que se necesita es alguna forma de permitir que el usuario verifique la exactitud de una respuesta que se le da para que tenga cierta confianza en lo que se le dice. Si tuviera que obtener una solución de un colega de matemáticas, él / ella podría simplemente sentarse y mostrarle su trabajo. Sin embargo, esto no es factible para una computadora en la mayoría de los casos. ¿Podría la computadora darle un testigo simple y fácilmente comprobable de la exactitud de su respuesta? Es posible que la verificación tenga que hacerse por computadora, pero es de esperar que verificar el algoritmo de verificación sea mucho más fácil que verificar el algoritmo para producir el testigo en primer lugar. ¿Cuándo sería factible y cómo podría formalizarse exactamente?
En resumen, mi pregunta es la siguiente.
¿Podría ser posible, al menos en teoría, que el software matemático proporcione una prueba comprobable breve junto con la respuesta que ha solicitado?
Un caso trivial en el que podemos hacer esto de inmediato es la factorización de enteros, por supuesto, o muchos de los problemas clásicos de NP completo (por ejemplo, circuito hamiltoniano, etc.).
fuente
Respuestas:
El concepto de "testigos" o "pruebas verificables" no es totalmente nuevo: como se menciona en los comentarios, busque el concepto de "certificado". Se me ocurrieron tres ejemplos, hay más (en los comentarios y en otros lugares):
Kurt Mehlhorn describió en 1999 un problema similar en los algoritmos de geometría computacional (por ejemplo, errores menores en las coordenadas pueden producir grandes errores en los resultados de algún algoritmo), resuelto de manera similar en la biblioteca Leda , al insistir en que cada algoritmo produce un "certificado" de su respuesta además de la respuesta misma.
Demaine, López-Ortiz y Munro en 2000 utilizaron los conceptos de certificados (los llaman "pruebas") para mostrar límites inferiores adaptativos en el cálculo de la unión y la intersección (y la diferencia, pero esta es trivial) de conjuntos ordenados. No excluya su trabajo porque no utilizaron certificados para protegerse contra errores informáticos: demostraron que aunque el certificado puede ser lineal en el tamaño de la instancia en el peor de los casos, a menudo es más corto y, por lo tanto, puede "comprobarse" "en tiempo sublineal (dado acceso aleatorio a la entrada como una matriz ordenada o un B-Tree), y en particular en un tiempo inferior al requerido para calcular dicho certificado.
He estado usando el concepto de certificados en varios otros problemas desde que vi a Ian Munro presentando su implementación en Alenex 2001 , y en particular para las permutaciones (disculpas por el enchufe descarado, viene otro), donde el certificado es más corto en el mejor de los casos que en el peor de los casos, lo que produce una estructura de datos comprimidos para permutaciones. Una vez más, verificar el certificado (es decir, el orden) lleva más tiempo lineal, menos que calcularlo (es decir, ordenarlo).
El concepto no siempre es útil para la verificación de errores: existen problemas en los que la verificación del certificado lleva tanto tiempo como la producción (o simplemente la producción del resultado). Se me ocurren dos ejemplos, uno trivial y otro complicado, Blum y Kannan (mencionados en los comentarios) dan otros.
La biblioteca Leda es el esfuerzo más general (que yo sepa) para hacer que los algoritmos deterministas de producción de certificados sean la norma en la práctica. El trabajo de Blum y Kannan es el mejor esfuerzo que vi para que sea la norma en teoría, pero sí muestran los límites de este enfoque.
Espero eso ayude...
fuente