De vueltas con la formación científica en Ciencias de la Computación e Inteligencia Artificial

esquema de cómo aplicar model checking en un sistema industrial

La redacción de la entrada donde hablaba de la frustración con que se afronta en España el futuro de las Ciencias de la Computación e Inteligencia Artificial (CCIA) -como entidad independiente de las tecnologías que la usan- me sugirió la idea de dar nota de otros ejemplos llamativos. Básicamente, y sin pretender ser exhaustivos, me he interesado por anuncios que presenten el problema de manera diferente. También quiero dejar claro que afortunadamente existen excepciones en España que son prometedoras.

Por tanto, como la entrada a la que hago mención cubre el campo de las ofertas de trabajo, ahora comento dos que cubren otros aspectos:

  1. I+D en la empresa. Una de las start-up más interesantes que sigo es la que los autores de Pellet han creado en torno a su demostrador. Es emblemática por varios motivos. En primer lugar, adoptan la filosofía del software libre como motor de innovación y plantean el modelo de negocio en torno a sus productos. En segundo lugar, su producto estrella es un demostrador automático, palabra prohibida en la teoría o en la práctica en los curriculums de matemáticos e informáticos. Y en tercer lugar, por su activa apuesta por la formación de sus trabajadores, colaboradores y/o becarios. Es esto último lo más llamativo: Los colaboradores-estudiantes van camino de conseguir tesis doctorales en universidades de prestigio. Otra cosa impensable en nuestro desolador panorama científico. Y no sólo porque la empresa, en general, sólo desea programadores. También por el ambiente clientelista de las carreras técnicas para con las empresas contratadoras. Por supuesto, el caso del que hablo no es único; es sólo un ejemplo reciente. Este caso también es especialmente llamativo porque una de las rutinarias quejas en este país es la deficiente transferencia de la investigación de las universidades a las empresas. Cuando leo o escucho una de esas quejas, me sorprende que casi nadie (de ambos bandos) reivindique la condición necesaria para que esto ocurra: Las empresas deben incentivar, contratar y tener doctores, para así entender la importancia, evaluar y aplicar los resultados. Pero eso tiene un coste que muchas empresas en España no pueden o no desean sufragar. Porque es una actitud equivocada pensar que la Universidad debe proveer la tecnología, la herramienta acabada, convirtiéndose en una subcontrata. La Universidad puede aportar en mucho mayor grado conocimiento, que debe ser aplicado. Pero eso, como digo, es caro. Que apliquen otros.
  2. Investigación de calidad. Recientemente la Association for Computing Machinery (ACM) -cuyo lema es Advancing Computing as a Science & Professionha otorgado su prestigioso premio ACM Turing award a tres investigadores que he seguido con devoción estos últimos años. Se trata de Edmund M. Clarke, E. Allen Emerson, y Joseph Sifakis, los fundadores de la teoría de model-checking como la gran herramienta para la verificación formal. Cuando leí el artículo tuve la misma sensación que cuando me atreví a decir que ningún egresado de los nuevos planes de estudio españoles resolverá el problema P?NP. Pero, en este caso, con mayor dolor. Me explico. En mi opinión, ese problema sólo se podrá atacar desde la teoría de conjuntos y la teoría de modelos, es decir, realmente es un problema lógico-matemático-computacional. Sin embargo, el model checking no es una herramienta puramente teórica, es usable y está implementada en muchos sistemas. Pero el desconocimiento y las deficiencias en lógica computacional impedirán su uso generalizado en países como España, por las razones que ya comenté. Y en mi campo de interés, agentes inteligentes y Web Semántica, se puede convertir en una herramienta crítica para hacer de la teoría de agentes una verdadera ingeniería, al presentar un soporte formal para la verificación del producto software en este campo. La idea de usar semánticas de tipo Kripke en el campo de sistemas multiagente ya la adelantaron Joseph Y. Halpern, Moshe Y. Vardi en su trabajo clásico Model Checking vs. Theorem Proving: A Manifesto, donde argumentan que el razonamiento basado en modelos es mucho más eficiente que la demostración automática para la verificación (aunque teniendo en cuenta que está basado en modelos). Concluyendo, vista la situación de la ciencia en España, me atrevo a pronosticar que será muy difícil que un nuevo licenciado diseñe el lenguaje de programación orientado a agentes racionales que toda la comunidad científica de este campo persigue, desde la propuesta fundacional de Y. Shoham.

Me temo que prontamente presentaré nuevos ejemplos, de perfil completamente distinto, donde se volverá a mostrar en toda su crudeza la previsible pérdida de competitividad de la ciencia española frente a la de otros países, debido a la progresiva mercantilización de la educación superior.

Anuncios