modified on 21 jul 2017 at 00:39 ••• 8.311 views

Razonamiento Asistido por Computador

De Master

(Diferencias entre revisiones)
(Página Web)
(Contenido)
Línea 1: Línea 1:
= Contenido =
= Contenido =
-
En la actualidad, los sistemas de hardware y de software tienen con frecuencia un grado de complejidad elevado, y la tendencia es que cada vez sean más complejos. Algunos de estos sistemas son denominados "de seguridad crítica", ya que su corrección (es decir, que funcionen como se espera que funcionen) es fundamental (por ejemplo, porque de ellos dependan vidas humanas o grandes cantidades de dinero). La aproximación clásica a la verificación de la corrección consiste en comprobar el sistema sobre un conjunto grande de datos de entrada. Si bien este método puede ser satisfactorio en algunos casos, no lo es en el caso de los sistemas de seguridad crítica, ya que el descubrimiento de un fallo está supeditado a que el dato de entrada que lo desvela se encuentre en el conjunto de las pruebas. Una alternativa consiste en modelar formalmente los sistemas como objetos matemáticos, y formular su corrección mediante teoremas, susceptibles de ser demostrados formalmente. De esta manera aumentamos drásticamente nuestra confianza en su buen funcionamiento. La complejidad de los sistemas puede hacer que esas demostraciones sean laboriosas y complejas, por lo que resulta imprescindible disponer de la ayuda de un sistema que sirva para comprobar las demostraciones. ACL2 es uno de los sistemas de razonamiento automático se ha aplicado en la industria, sobre todo para la verificación de hardware.
+
<!--En la actualidad, los sistemas de hardware y de software tienen con frecuencia un grado de complejidad elevado, y la tendencia es que cada vez sean más complejos. Algunos de estos sistemas son denominados "de seguridad crítica", ya que su corrección (es decir, que funcionen como se espera que funcionen) es fundamental (por ejemplo, porque de ellos dependan vidas humanas o grandes cantidades de dinero). La aproximación clásica a la verificación de la corrección consiste en comprobar el sistema sobre un conjunto grande de datos de entrada. Si bien este método puede ser satisfactorio en algunos casos, no lo es en el caso de los sistemas de seguridad crítica, ya que el descubrimiento de un fallo está supeditado a que el dato de entrada que lo desvela se encuentre en el conjunto de las pruebas. Una alternativa consiste en modelar formalmente los sistemas como objetos matemáticos, y formular su corrección mediante teoremas, susceptibles de ser demostrados formalmente. De esta manera aumentamos drásticamente nuestra confianza en su buen funcionamiento. La complejidad de los sistemas puede hacer que esas demostraciones sean laboriosas y complejas, por lo que resulta imprescindible disponer de la ayuda de un sistema que sirva para comprobar las demostraciones. ACL2 es uno de los sistemas de razonamiento automático se ha aplicado en la industria, sobre todo para la verificación de hardware.
Los objetivos de esta materia son los siguientes:
Los objetivos de esta materia son los siguientes:
Línea 8: Línea 8:
* Conocer la lógica de ACL2, su axiomas , sus reglas de inferencia (con especial énfasis en el principio de inducción) y la noción de demostración en la misma.
* Conocer la lógica de ACL2, su axiomas , sus reglas de inferencia (con especial énfasis en el principio de inducción) y la noción de demostración en la misma.
* Entender el funcionamiento del demostrador automático de ACL2, como asistente en la realización de pruebas formales de la corrección de los sistemas modelados.
* Entender el funcionamiento del demostrador automático de ACL2, como asistente en la realización de pruebas formales de la corrección de los sistemas modelados.
-
* Alcanzar destreza práctica en el manejo del demostrador para la demostración de resultados sencillos.
+
* Alcanzar destreza práctica en el manejo del demostrador para la demostración de resultados sencillos.-->
 +
 
 +
Esta asignatura pretende ser una continuación de la asignatura del primer cuatrimestre "Aprendizaje Automático", abordando con
 +
mayor profundidad algunas de las cuestiones ya vistas e introduciendo nuevos temas, aportando un enfoque práctico, pero sin
 +
olvidar el necesario fundamento teórico de las distintas técnicas introducidas.
 +
 
 +
* Introducción al lenguaje python
 +
* Algoritmos básicos de aprendizaje automático
 +
* El sistema scikit-learn
 +
* Aprendizaje de árboles, reglas de clasificación y reglas de asociación
 +
* Modelos de regresión
 +
* Modelos probabilísticos
 +
* Modelos líneales y redes neuronales
 +
* Aprendizaje de modelos no paramétricos
 +
* Evaluación de modelos
 +
* Ensemble learning
 +
---------------------------------------------------------
 +
 
 +
 
 +
 
== [http://www.us.es/estudios/master/master_M095/asignatura_50950011 Programa de la asignatura] ==
== [http://www.us.es/estudios/master/master_M095/asignatura_50950011 Programa de la asignatura] ==
== [http://www.cs.us.es/cursos/ram/ Página Web] ==
== [http://www.cs.us.es/cursos/ram/ Página Web] ==

Revisión de 00:38 21 jul 2017

Contenido

Esta asignatura pretende ser una continuación de la asignatura del primer cuatrimestre "Aprendizaje Automático", abordando con mayor profundidad algunas de las cuestiones ya vistas e introduciendo nuevos temas, aportando un enfoque práctico, pero sin olvidar el necesario fundamento teórico de las distintas técnicas introducidas.

  • Introducción al lenguaje python
  • Algoritmos básicos de aprendizaje automático
  • El sistema scikit-learn
  • Aprendizaje de árboles, reglas de clasificación y reglas de asociación
  • Modelos de regresión
  • Modelos probabilísticos
  • Modelos líneales y redes neuronales
  • Aprendizaje de modelos no paramétricos
  • Evaluación de modelos
  • Ensemble learning



Programa de la asignatura

Página Web