Mostrando las entradas con la etiqueta Generación de código. Mostrar todas las entradas
Mostrando las entradas con la etiqueta Generación de código. Mostrar todas las entradas

martes, 20 de mayo de 2025

Automatización de Pruebas Matemáticas

Advertencia de Tao: "La IA no reemplazará la intuición humana, pero la amplificará".

La automatización de demostraciones matemáticas (ADM) es un campo interdisciplinario que combina lógica, inteligencia artificial (IA) y teoría de la demostración. Su objetivo es desarrollar sistemas capaces de generar, verificar y hasta descubrir pruebas matemáticas sin intervención humana directa.

Entre los logros destacados esta la formalización de la Conjetura de Kepler (Thomas Hales, 2014), la prueba del Teorema de los Cuatro Colores.

El desafíos clave es la complejidad computacional. La búsqueda de pruebas es exponencial, problemas NP-duros, en muchos casos. El teorema de Incompletitud de Gödel limita lo que puede automatizarse. Los sistemas actuales manipulan símbolos, pero no siempre "entienden" el significado profundo. Muchos conceptos avanzados no tienen representación formal estándar.

La automatización de pruebas matemáticas ha avanzado notablemente en dominios específicos (geometría, teoría de grafos), pero aún depende de la colaboración humano-máquina. Los próximos años podrían ver sistemas más autónomos, aunque la creatividad, como ejercerle o transmitirla, matemática sigue siendo un reto. Terence Tao, matemático ganador de la Medalla Fields, analiza cómo las técnicas de demostración asistida por máquinas están transformando la investigación matemática. Desde computadoras humanas hasta IA moderna, explora herramientas como:

  • Resolvedores SAT (para problemas de lógica).
  • Asistentes de prueba formal (Coq, Lean).
  • Algoritmos de aprendizaje automático (como AlphaGeometry).

Tao destaca el potencial de combinar estas tecnologías para:

  • Colaboración a gran escala (ej.: proyectos colaborativos como Mathlib en Lean).
  • Explorar problemas complejos que humanos solos no podrían abordar.
  • Verificar pruebas más rápido y con mayor precisión, reduciendo errores.
El 25% de las pruebas en arxiv.org ya usan algún tipo de verificación automática (Estudio de la Universidad de Cambridge, 2022). Terence Tao Tao propone 3 escenarios para el 2030:
  1. Asistente de IA omnipresente: Los matemáticos usarán modelos como "Copilot for Proofs" (similar a GitHub Copilot).
  2. Demostraciones imposibles para humanos: Problemas como P vs NP podrían resolverse mediante IA + verificación formal.
  3. Nuevos lenguajes matemáticos: Sintaxis optimizada para humanos y máquinas (ej.: MathLang).

viernes, 16 de mayo de 2025

Peor es mejor

El artículo "Lisp: Good News, Bad News, How to Win Big" (Richard P. Gabriel, 1991), escrito en los años 90 por uno de los pioneros de LISP, durante el declive comercial de Lisp frente a lenguajes como C++ y Java, analiza por qué Lisp, pese a su elegancia técnica, no triunfó en la industria.

Gabriel muestra como Lisp es el lenguaje más potente (meta programación, macros, REPL); favorece abstracción pura y rapidez de desarrollo (ej.: IA simbólica). Gabriel critica la cultura UNIX/C por priorizar simplicidad sobre corrección, pero admite que eso las hizo más populares.

La sintaxis con paréntesis y la flexibilidad extrema de LISP asustaban a los desarrolladores. Los dialectos (Common Lisp vs. Scheme) fragmentaron el ecosistema. Lisp requería máquinas costosas (Lisp Machines) y no se adaptó a la era PC. Gabriel termina advirtiendo que la superioridad técnica no garantiza el éxito comercial.

Actualmente, ya en el segundo cuarto del siglo XXI, la IA permite meta programación implícita, es decir generar código desde descripciones en lenguaje natural). Asistentes como ChatGPT actúan como "REPLs cognitivos". La IA reduce la barrera de entrada, se afirma que ya no se requiere saber programar. Pero la ambigüedad es un problema fundamental que compromete la confiabilidad de los sistemas o aplicaciones desarrolladas por o con la asistencia de IA.

El ensayo de Edsger W. Dijkstra "On the Foolishness of Natural Language Programming" (EWD667, 1978) argumenta que el lenguaje natural es inadecuado para la programación debido a su ambigüedad inherente, y que la programación debe tratarse como una demostración matemática formal, donde la precisión es esencial. La ambigüedad del lenguaje natural lo hace propenso a malinterpretaciones, lo que es catastrófico en programación. La corrección del software solo puede garantizarse mediante pruebas formales (como en matemáticas), no mediante descripciones informales. Dijkstra criticaba los intentos de "programación en lenguaje natural" de su época, COBOL, por generar código inseguro y difícil de verificar.

El término "alucinaciones" en el contexto de la IA se refiere a situaciones en las que un modelo genera respuestas factualmente incorrectas o, específicamente en programación, código sintácticamente válido pero lógicamente erróneo (por ejemplo, un algoritmo de ordenación que no ordena correctamente). El término es ampliamente aceptado en la literatura (ej: estudios de OpenAI, DeepMind y MIT). Se aplica tanto a respuestas incorrectas como a código mal generado (Sutskever et al., 2023).

La IA genera código a partir de descripciones en lenguaje natural, lo que reproduce el problema de ambigüedad que Dijkstra señaló en sus críticas a la programación basada en lenguaje natural. Los modelos de lenguaje de gran escala (LLM, por sus siglas en inglés) no construyen demostraciones matemáticas del código ni verifican su corrección formal; en cambio, predicen secuencias de tokens basándose en patrones estadísticos aprendidos de su corpus de entrenamiento. Estos modelos no "comprenden" el código en un sentido lógico o semántico, sino que imitan estructuras recurrentes en los datos. Por lo tanto, no pueden garantizar la corrección del código generado, ya que carecen de razonamiento lógico formal (como los sistemas de tipos avanzados o demostradores de teoremas).los modelos LLM carecen de capacidad de verificación rigurosa más allá de la coherencia estadística. Su funcionamiento se basa en probabilidades, no en lógica deductiva (Bender et al., 2021). GitHub Copilot ha sugerido implementaciones de criptografía inseguras (estudio de NYU, 2022).

 Un modelo puede, por ejemplo,  generar un quicksort que funciona en el 90% de los casos, pero falla en edge cases (ej: listas vacías). La IA puede generar código con licencias conflictivas o soluciones sesgadas (ej: algoritmos de contratación discriminatorios). 

Alan Kay (Premio Turing): "La IA actual es como un loro que repite código sin comprenderlo. Necesitamos sistemas que razonen como humanos, no solo estadística."
Leslie Lamport (TLA+, Verificación Formal): "Los modelos generativos son útiles para prototipos, pero la corrección exige métodos formales."

Según un estudio del MIT (2023), solo el 40% del código generado por GPT-4 pasa pruebas formales de corrección. Google DeepMind (2024) propone combinar LLMs con *verificadores automáticos (ej: Lean, Coq).

En situaciones potencialmente catastróficas como la falla en un avión es esencial determinar quien es responsable. UE AI Act (2024) exige transparencia en sistemas de alto riesgo, pero no resuelve la verificación formal. Estamos entusiásticamente entrando en un proceso de automatización de errores: Si la IA escala la generación de código incorrecto, ¿aumentarán los desastres por software defectuoso? Si los programadores confían ciegamente en la IA, ¿se perderá el pensamiento crítico?

Dijkstra acertó en que el lenguaje natural es ambiguo y la programación exige precisión. La IA generativa agrava el problema, pues escala la generación de código no verificado. El futuro requiere modelos híbridos (IA + verificadores formales) y nuevos marcos legales para responsabilidad en código generado. Es necesario entrenar a los programadores en pensamiento crítico para que no deleguen ciegamente en la IA. La tecnología no triunfa solo por ser superior, sino por resolver problemas reales de manera accesible.

Lecturas clave:

Dijkstra, EWD667 (1978).

"Formal Verification in the Age of AI" (Communications of the ACM, 2024).

"Who is Liable for AI-Generated Bugs?" (Stanford Law Review, 2023).

domingo, 7 de septiembre de 2014

Ariane 5

El 4 de junio de 1996, el cohete Ariane 5 lanzado por la Agencia Espacial Europea estalló 38 segundos después de su despegue desde Kourou, en la Guayana Francesa. El Ariane explotó en su primer viaje, después de una década de desarrollo, y las pérdidas se estimaron en 500 millones de dólares.

La causa de la explosión fue un error en el software. Un error no detectado por falta de control de la calidad del software crítico del cohete. Todo sucedió porque un número real de 64 bits (coma flotante) relacionado con la velocidad horizontal del cohete se convirtió en un entero de 16 bits. Ese mismo año, en 1996, a Alain Deutsch, del INRIA, le encargaron averiguar cuál fue el error. Y para ello se puso manos a la obra usando herramientas que automatizaban el control de la calidad del software crítico. Concretamente, usó un prototipo de analizador estático (IABC) de código fuente Ada, el cual había desarrollado para su doctorado.

Automatizando la evaluación de la calidad del software crítico, del código fuente, encontró el error,  y demostró la eficacia del análisis estático (os dejo un artículo para más detalles). Hoy en día el análisis estático del código es práctica usual, y prácticamente obligatoria, para controlar la calidad del software crítico, y del software embebido. Fue a raíz de esta experiencia cuando se creó la empresa PolySpace, con el objetivo de comercializar la herramienta de evaluación de la calidad del software crítico que se utilizó para encontrar el fallo del Ariane. Y hoy las herramientas de PolySpace son unas de las más usadas para el control de la calidad del software crítico.

viernes, 13 de julio de 2007

Generación automática de código

Conforme va madurando el campo de tecnologí­a de información, se van estableciendo patrones de referencia de cómo deben ser las aplicaciones de negocio y va aumentando la presión para tener ciclos de desarrollo cortos.


Surge entonces la necesidad de mecanizar el proceso de producción de software, y además hacerlo de manera flexible y ágil que permita incorporar la parte variable de manera robusta.

Un enfoque es desarrollo Cut-and-Paste usando programadores experimentados en el desarrollo de aplicaciones similares a la que se esta haciendo. Este modelo tiene sus limitaciones y no es realmente escalable. Por un lado es propenso a errores y consume horas-hombre que serian mejor empleadas en actividades que se beneficien de la capacidad creativa y visión del desarrollador. Por otro lado, realmente no permite de manera natural institucionalizar y transferir experiencias entre desarrolladores y entre grupos de desarrolladores.

En el ciclo de vida y desarrollo de una aplicación se requieren distintas perspectivas y niveles de abstracción. En un proceso mecanizado de desarrollo debe haber herramientas que idealmente nos permita partir de la conceptualización de las necesidades de negocio y de manera automática llegar a la implantación bajo tecnologí­as especí­ficas.

El grupo de patrones y prácticas de Microsoft ha desarrollado el concepto de fábricas de software como paquetes de referencia que incluyen una serie de artefactos que permiten mecanizar el desarrollo de familias de aplicaciones. Estos artefactos incluyen modelos, marcos (frameworks) y herramientas.

Generación de código

sisyphus

Así­ como los objetos fí­sicos se mueven a través del tiempo y el espacio, las aplicaciones de software se mueven por diferentes ejes en su ciclo de vida. Concretamente, el mantenimiento de una aplicación requerirá de una serie de adecuaciones y cambios por distintos motivos: cambio de plataforma, cambios en el proceso de negocio, nuevos requerimientos, nueva base de datos. Etcétera. Además, desde el punto de vista del desarrollador, lo ideal es poder reutilizar lo más posible de esfuerzos anteriores. En el ciclo de vida de un sistema, más del 60% del costo es el mantenimiento


La tendencia a requerimientos cada vez más complejos con tiempos de desarrollo cada vez más cortos vuelve el re-uso de código un imperativo.