En informática teórica , un algoritmo de certificación es un algoritmo que genera, junto con una solución al problema que resuelve, una prueba de que la solución es correcta. Se dice que un algoritmo de certificación es eficiente si el tiempo de ejecución combinado del algoritmo y un verificador de pruebas es más lento como máximo en un factor constante que el algoritmo no certificador más conocido para el mismo problema. [1]
La prueba producida por un algoritmo de certificación debería ser en cierto sentido más simple que el algoritmo en sí, ya que de lo contrario cualquier algoritmo podría considerarse certificante (con su salida verificada ejecutando el mismo algoritmo nuevamente). A veces esto se formaliza exigiendo que una verificación de la prueba tome menos tiempo que el algoritmo original, mientras que para otros problemas (en particular aquellos para los que la solución se puede encontrar en tiempo lineal ) la simplicidad de la prueba de salida se considera de una manera menos formal. sentido. [1] Por ejemplo, la validez de la prueba de salida puede ser más evidente para los usuarios humanos que la exactitud del algoritmo, o un verificador de la prueba puede ser más susceptible de verificación formal . [1] [2]
Las implementaciones de algoritmos de certificación que también incluyen un verificador de la prueba generada por el algoritmo pueden considerarse más confiables que los algoritmos que no certifican. Porque, siempre que se ejecuta el algoritmo, sucede una de tres cosas: produce una salida correcta (el caso deseado), detecta un error en el algoritmo o su implicación (no deseado, pero generalmente es preferible a continuar sin detectar el error), o tanto el algoritmo como el corrector están defectuosos de una manera que enmascara el error y evita que sea detectado (no deseado, pero poco probable ya que depende de la existencia de dos errores independientes). [1]
Ejemplos de
Muchos ejemplos de problemas con algoritmos comprobables provienen de la teoría de grafos . Por ejemplo, un algoritmo clásico para probar si un gráfico es bipartito simplemente generaría un valor booleano: verdadero si el gráfico es bipartito, falso en caso contrario. Por el contrario, un algoritmo de certificación puede generar un color 2 del gráfico en el caso de que sea bipartito, o un ciclo de longitud impar si no lo es. Cualquier gráfico es bipartito si y solo si puede ser de 2 colores, y no bipartito si y solo si contiene un ciclo impar. Tanto comprobar si una coloración 2 es válida como comprobar si una determinada secuencia de vértices de longitud impar es un ciclo se puede realizar de forma más sencilla que probar la bipartición. [1]
De manera análoga, es posible probar si un gráfico dirigido dado es acíclico mediante un algoritmo de certificación que genera un orden topológico o un ciclo dirigido. Es posible probar si un grafo no dirigido es un grafo cordal mediante un algoritmo de certificación que genera un orden de eliminación (un orden de todos los vértices de modo que, para cada vértice, los vecinos que están más tarde en el orden forman una camarilla ) o un ciclo sin acordes. Y es posible probar si un gráfico es plano mediante un algoritmo de certificación que genera una incrustación plana o un subgrafo de Kuratowski . [1]
El algoritmo de Euclides extendido para el máximo común divisor de dos enteros x y y está certificando: emite tres enteros g (el divisor), una , y b , de manera que ax + por = g . Esta ecuación solo puede ser cierta para los múltiplos del máximo común divisor, por lo que la prueba de que g es el máximo común divisor se puede realizar comprobando que g divide tanto a x como a y y que esta ecuación es correcta. [1]
Ver también
- Verificación de cordura , una prueba simple de la exactitud de una salida o resultado intermedio que no se requiere para ser una prueba completa de corrección.
Referencias
- ↑ a b c d e f g McConnell, RM; Mehlhorn, K .; Näher, S .; Schweitzer, P. (mayo de 2011), "Certificar algoritmos", Computer Science Review , 5 (2): 119–161, doi : 10.1016 / j.cosrev.2010.09.009.
- ^ Alkassar, Eyad; Böhme, Sascha; Mehlhorn, Kurt ; Rizkallah, Christine (junio de 2013), "A Framework for the Verification of Certifying Computations", Journal of Automated Reasoning , 52 (3): 241–273, arXiv : 1301.7462 , doi : 10.1007 / s10817-013-9289-2.