Observatorio de información y Publicaciones

Resumen: Los modelos de lenguaje grande (LLM) se utilizan cada vez más para la tutoría automatizada, pero su confiabilidad en dominios simbólicos estructurados aún no está clara. Estudiamos la retroalimentación a nivel de paso para pruebas de lógica proposicional, que requieren un razonamiento simbólico preciso alineado con el estado de prueba actual del alumno.

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.