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).

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.

Depreciación de funciones en Visual Studio C/C++

Uno de los problemas que se presenta al actualizar una aplicación en Visual Studio C/C++ es la depreciación de funciones. La motivación de muchos de estos cambios es hacer el código más seguro.



Existen varias maneras de eliminar las advertencias para las funciones obsoletas o depreciadas. Las más sencilla es definir _CRT_SECURE_NO_WARNINGS o usar el pragma warning. Lo más recomendable es usar la versión segura equivalente.

Referencias:

strcpy_s, wcscpy_s, _mbscpy_s

Security Enhancements in the CRT

Clear code that works

A partir de una visión clara e intima del proceso de desarrollo de software, Kent Beck a creado un enfoque metodológico que  a primera vista pareciera contra intuitivo pero que ha resultado exitoso y ampliamente aceptado en la comunidad de programadores.

En Test Driven Development: By Example (Addison-Wesley Signature Series), el libro seminal de TDD, Beck aplica el refrán de divide y vencerás al precepto de calidad en la producción de código:  Clear code that works.
Beck propone contracorriente que es posible separar las consideraciones de calidad de código, desde la perspectiva de ingeniería de software, de la verificación de la funcionalidad, y que el primer paso en cada iteración del proceso de desarrollo es definir y aplicar las pruebas de funcionalidad.
Beck utiliza un proceso de refactorización para pasar de código funcional a código limpio, utilizando la eliminación de redundancia o duplicidad  como guía metodológica.
Haciendo una analogía con un semáforo,  Beck describe un proceso iterativo de 3 pasos:

1. Rojo. Empezar con una prueba que debe fallar, tal ves ni compilar siquiera.
2. Verde. Hacer que el código pase la prueba de la manera más expedita y simple, sin consideración alguna a normas y patrones de calidad de código.
3. Refactorizar. Eliminar redundancia en código, pruebas, y datos.

De tan sencillo enfoque Beck elabora la metodología de desarrollo dirigido por pruebas.

El gobierno uruguayo utilizar software libre en la administración pública

El gobierno uruguayo eligió utilizar software libre en la administración pública para disponer de un "comunicación segura" tras los recientes casos de espionaje por parte de los Estados Unidos, según anunció el canciller de ese país, Luis Almagro.

A medidados de julio, los presidentes de los países del Mercosur explicitaron en Montevideo la importancia de apoyar el desarrollo de software libre "a fin de lograr una verdadera apropiación, promoción del libre conocimiento y transferencia tecnológica, reduciendo la dependencia de soluciones provistas por trasnacionales del sector".

Nubes

El continuo abaratamiento de la infraestructura computacional y la omnisciencia de conexiones de banda ancha están generando un cambio de paradigmas en el industria de tecnología de información y se ven nubes acumulándose en el cielo informático.

Referencias

• Nutch
• http://en.wikipedia.org/wiki/Hadoop
• HBase
• http://www.danga.com/mogilefs/
• http://aws.amazon.com/ec2/

El bueno, malo, y bonito

javascript esta en un estado límbico. Por un lado permite trucos de manejo de pantallas tipo Ajax y por otro es un riesgo de seguridad. ¿Qué influencia será más fuerte?

Firefox flaws raise Mozilla security doubts

Levantamiento de requerimientos

El siguiente escenario es tí­pico: Un consultor trabaja con los usuarios para describir los procesos de negocio que serán soportados por el software. El equipo de desarrollo recibe la descripción del consultor pero no están familiarizados con los términos de negocio y consideran la descripción demasiado informal. Los desarrolladores escriben su propia descripción desde un punto de vista técnico. El usuario no entiende esta descripción pero la acepta para que el proyecto avance. El resultado puede ser un sistema que desde el punto de vista del usuario es difícil de usar y que no cumple con sus expectativas.

Parte de este problema es metodológico, y en parte es intrínseco a las caracterí­sticas de los usuarios. Algunas de las problemáticas que se presentan:

• Los usuarios no saben que es lo que quieren
• Los usuarios no aceptan como un compromiso los requerimientos escritos
• Los usuarios insistirán en nuevos requerimientos después de fijar costos y agendas.
• Los usuarios no están disponibles y la comunicación con ellos es lenta
• Los usuarios no participan en revisiones de avance.
• Los usuarios no entienden el proceso de desarrollo y no les interesa.

Existen herramientas y metodologías para el levantamiento de requerimientos. Casos de uso y UML son medios para formalizar este proceso. Que diagramas UML es apropiado usar dependerá del sistema a desarrollar.

Una guía simple en términos de la complejidad del sistema:

• Aplicación mono usuario
  • Diagrama de casos de uso.
  • Diagrama de clases.
  • Diagrama de interacción.
• Aplicación mono usuario, con manejo de eventos:
  • Añadir: Diagrama de estados.
• Aplicación cliente servidor:
  • Añadir: Diagrama de despliegue y diagrama de componentes, dependiendo de la complejidad.
• Aplicación compleja distribuida:
  • Todos.

Para una aplicación sencilla debemos realizar entre tres y seis tipos de diagramas, y para una aplicación compleja unos nueve tipos. El diagrama de casos de uso puede modelar el contexto de un sistema o los requisitos del mismo. Se puede extender la colección de elementos base de UML utilizando estereotipos.

Referencias:

• Database answers es un repositorio con más de 450 esquemas de datos para diferentes aplicaciones. Algunos usados como referencia en la documentación de Microsoft SQL Server 2005
• En el caso de .Net, Design patterns, AJAX Design Patterns, and .NET training , tiene ejemplos en C# y VB
• https://www6.software.ibm.com/developerworks/education/r-rsmvisual/
• http://www.programacion.net/tutorial/uml/
• http://www.clikear.com/manuales/uml/
• http://odl-skopje.etf.ukim.edu.mk/uml-help/