Observatorio de información y Publicaciones

Resumen:Presentamos FormalProofBench, un punto de referencia privado diseñado para evaluar si los modelos de IA pueden producir pruebas matemáticas formalmente verificadas a nivel de posgrado. Cada tarea combina un problema de lenguaje natural con una declaración formal de Lean~4, y un modelo debe generar una prueba de Lean aceptada por el verificador de Lean 4.

Resumen: Arte. 50 II de la Ley de Inteligencia Artificial de la UE exige una doble transparencia para el contenido generado por IA: los resultados deben etiquetarse en forma comprensible para humanos y legible por máquina para su verificación automatizada. Este requisito, que entrará en vigor en agosto de 2026, choca con las limitaciones fundamentales de los actuales sistemas de IA generativa.

Resumen: Los enfoques existentes para el monitoreo predictivo de procesos son subsimbólicos, lo que significa que aprenden correlaciones entre características descriptivas y una característica objetivo basándose completamente en datos, por ejemplo, prediciendo las necesidades quirúrgicas de un paciente basándose en eventos históricos y datos biométricos.