martes, 11 de diciembre de 2007

VISION ARTIFICIAL

vision artificial
INTRODUCCION

En el año 1955 Herbert Simon, el físico Allen Newell, uno de los padres de la IA actual, y J.C. Shaw, programador de la RAND Corp. y compañero de Newell, desarrollan el primer lenguaje de programación orientado a la resolución de problemas de la IA, el IPL-11. Un año más tarde estos tres científicos desarrollan el primer programa de IA al que llamaron "Logic Theorist", el cual era capaz de demostrar teoremas matemáticos. Este programa demostró 38 de los 52 teoremas del segundo capítulo de "Principia Mathematica" de Russel y Whitehead, uno de ellos incluso de manera más elegante a la propuesta por los autores.
Los centros de investigación fundamentales para la IA durante sus primeros años, de 1956 a 1963, fueron la Universidad Carnegie Mellon, el Massachusetts Institute of Technologie (o MIT), la Universidad de Stanford e IBM, siendo los temas de investigación fundamentales el desarrollo de heurísticas y el aprendizaje de máquina.
En 1957 Newell y Simon continúan su trabajo con el desarrollo del GPS o General Problems Solver. GPS era un sistema orientado a la resolución de problemas; a diferencia del "Logic Theorist", el cual se orientó a la demostración de teoremas matemáticos, GPS no estaba programado para resolver problemas de un determinado tipo, razón a la cual debe su nombre.
En la década del 60 se comienza en el MIT el estudio de la visión artificial, lo cual implica no solo captar imágenes a través de una cámara, sino también la comprensión, por parte del ordenador, de lo que estas imágenes representan. Un resultado importante en este trabajo lo constituye el "mundo de micro-bloques", en el cual un robot era capaz de percibir un conjunto de bloques sobre una mesa, moverlos y apilarlos; el éxito se debió a los investigadores Larry Roberts, Gerald Sussman, Adolfo Guzman, Max Clowes, David Huffman, David Waltz, Patrick Winston, y Berthold Horn.

VISIÓN ARTIFICIAL

La Visión artificial, también conocida como Visión por Computador (del inglés Computer Vision) o Visión técnica, es un subcampo de la inteligencia artificial. El propósito de la visión artificial es programar un computador para que "entienda" una escena o las características de una imagen.

Esquema de relaciones entre visión por computadora y otras áreas afines.
Los objetivos típicos de la visión artificial incluyen:
La detección, segmentación, localización y reconocimiento de ciertos objetos en imágenes (por ejemplo, caras humanas).
La evaluación de los resultados (ej.: segmentación, registro).
Registro de diferentes imágenes de una misma escena u objeto, i.e., hacer concordar un mismo objeto en diversas imágenes.
Seguimiento de un objeto en una secuencia de imágenes.
Mapeo de una escena para generar un modelo tridimensional de la escena; tal modelo podría ser usado por un robot para navegar por la escena.
Estimación de las posturas tridimensionales de humanos.
Búsqueda de imágenes digitales por su contenido.
Estos objetivos se consiguen por medio de reconocimiento de patrones, aprendizaje estadístico, geometría de proyección, procesado de imágenes, teoría de gráficos y otros campos. La visión artificial cognitiva está muy relacionada con la psicología cognitiva y la computación biológica.

Visión Artificial aplicada al Sistema Visual Humano

Cuando la retina está dañada o no funciona bien, los fotorreceptores dejan de funcionar, pero eso no quiere decir que toda la estructura del Sistema Visual Humano no pueda seguir funcionando. Por ello hay una parte de científicos que están desarrollando microchips de silicio que puedan dotar de visión artificial a aquellas personas a las que no les funcionan los fotorreceptores.
Como ya sabemos, la información captada por los fotorreceptores se transmite a las células ganglionales, donde se interpreta y se manda al cerebro a través del nervio óptico. Existen enfermedades que afectan a estas células como la tetignosis pigmentaria o la DMAE, que dejan inoperativos los fotorreceptores pero no dañan las células ganglionales o el nervio óptico, con lo cual el problema no es que la información no puede llegar al cerebro, sino que no se puede captar. En estos casos se pueden desarrollar unos conos y bastones artificiales.
Los requisitos de los microchips para que cumpla la función de los fotorreceptores son:
Que sean lo suficientemente pequeños como para implantarlos en el ojo.
Que tengan una fuente de abastecimiento de energía continua.
Que no causen rechazo, es decir,que sean biocompatibles con los tejidos del ojo.
Uno de los micros que se ha desarrollado con éxito por el momento es un dispositivo de 2mm de diámetro y fino como un pelo humano. Contiene 3500 células solares microscópicas que imitan a los bastones y los conos y convierten la luz en pulsos eléctricos. Se abastece de energía solar, con lo que se evitan cables y baterías.
Microscopía digital
Producción de la imagen digital en microscopía óptica
La digitalización de una imagen electrónica o de video capturada por un microscopio óptico permite obtener un incremento espectacular en las posibilidades de ampliar características, extraer información o modificar la imagen. En comparación con el mecanismo tradicional de capturación de imágenes, la fotomicrografía en película, la digitalización de la imagen y el proceso de postadquisición/recuperación permiten una modificación reversible de la imagen como matriz ordenada de enteros fundamentalmente libre de ruido más que una mera serie de variaciones análogas en color e intensidad. Esta sección trata sobre diversos temas de actualidad acerca de la adquisición y procesamiento de imágenes para microscopía óptica.
Propiedades básicas de las imágenes digitales
Las imágenes de señal continua se reproducen mediante dispositivos electrónicos analógicos que registran los datos de la imagen con precisión utilizando varios métodos, como una secuencia de fluctuaciones de la señal eléctrica o cambios en la naturaleza química de la emulsión de una película, que varían continuamente en los diferentes aspectos de la imagen. Para procesar o visualizar en el ordenador una señal continua o una imagen analógica, se debe convertir primero a un formato comprensible para el ordenador o formato digital. Este proceso se aplica a todas las imágenes, independientemente de su origen, complejidad y de si son en blanco y negro (escala de grises) o a todo color. Una imagen digital se compone de una matriz rectangular (o cuadrada) de píxeles que representan una serie de valores de intensidad ordenados en un sistema de coordenadas (x,y).

Detectores de imagen electrónicos

La gama de métodos de detección de luz y la amplia variedad de dispositivos de imagen que están disponibles actualmente para el microscopista hacen que su selección sea difícil y a menudo confusa. Con este documento se pretende ofrecer ayuda para la comprensión de conceptos básicos sobre la detección de luz y proporcionar una guía para la selección del detector electrónico adecuado (CCD o sistema de videocámara) con aplicaciones específicas de microscopía óptica.
Fundamentos de la producción de imágenes en vídeo
Las imágenes ópticas producidas en el microscopio pueden ser capturadas utilizando bien técnicas de película tradicionales, digitalmente con detectores electrónicos como un chargecoupled device (CCD), o con una cámara de tipo tubo. Las cámaras son a menudo el recurso más apropiado cuando se deben grabar sucesos dinámicos en tiempo real.
Introducción a los sensores de imagen CMOS
Los sensores de imagen CMOS se han diseñado con la capacidad de integrar un número de funciones de procesamiento y control directamente en el circuito integrado del sensor, lo que se extiende más allá de la tarea fundamental de recopilación de fotones. Estos nuevos aspectos incluyen generalmente lógica temporal, control de exposición, conversión de analógico a digital, obturación, balance de blancos, ajuste del aumento y algoritmos de procesamiento inicial de la imagen. Se están introduciendo sensores de imagen CMOS económicos en el campo de la microscopía óptica en instrumentos para fines educativos que combinan una calidad óptica aceptable con paquetes de software de control e imagen fáciles de usar.
Conceptos básicos sobre procesamiento digital de la imagen
El procesamiento digital de la imagen permite una modificación reversible de la imagen prácticamente libre de ruido en forma de una matriz de enteros en vez de las clásicas manipulaciones en el cuarto oscuro o filtración de voltajes dependientes del tiempo necesarios para las imágenes analógicas y señales de video. Incluso aunque muchos algoritmos de procesamiento de imágenes son extremadamente potentes, el usuario medio a menudo aplica operaciones a imágenes digitales sin tener en cuenta los principios subyacentes tras dichas manipulaciones. Las imágenes que resultan de una manipulación descuidada están a menudo distorsionadas con respecto a aquellas que podrían producirse si la potencia y versatilidad del software de procesamiento digital fuesen utilizados correctamente.
Estrategias recomendadas para el procesamiento de imágenes digitales
Dependiendo de las condiciones de iluminación, la integridad de la muestra y los métodos de preparación, las imágenes capturadas con el microscopio óptico pueden requerir una cantidad considerable de rehabilitación/reinserción/renovación para conseguirun equilibrio entre precisión científica y composición estética. Las imágenes digitales que se obtienen mediante un CCD (charge-coupled device) o un CMOS (complementary metal oxide semiconductor) a menudo sufren señales-a-ruido pobres, iluminación irregular, impurezas de enfoque, deslumbramiento, cambios en los colores y otros problemas que distorsionan la calidad global de la imagen.

Deconvolución en microscopía óptica

La deconvolución es una técnica de procesamiento de imagen computacionalmente intensiva/reforzadora que se está utilizando cada vez más para mejorar el contraste y la resolución de las imágenes digitales capturadas con el microscopio. Su fundamento se basa en un juego de métodos diseñados para eliminar las imprecisiones presentes en las imágenes producidas por la abertura limitada del objetivo. Prácticamente, cualquier imagen obtenida con un microscopio digital fluorescente se puede deconvolver y se están desarrollando varias aplicaciones nuevas que utilizan técnicas de deconvolución para imágenes transmitidas de luz compuestas mediante varias estrategias de procesamiento de contraste. Uno de los campos qué más puede beneficiarse de la deconvolución es el de montajes en tres dimensiones a partir de secciones ópticas.

DEMOSTRACIÓN DE TEOREMAS


A finales del siglo XIX, los logistas formalizaron una noción ideal de prueba. A lo que les llevó no fue otra cosa que un ávido interés de la verdad. Estas abstracciones matemáticas fueron realizadas a mano. Tardaríamos un siglo en darnos cuenta de que estas pruebas y los programas eran lo mismo. La lógica moderna empezó con Gottlob Frege a finales de 1870. Medio siglo más tarde dos aspectos del trabajo de Frege alcanzaron su punto culminante: La deducción natural de Grentzen, que capturó una noción de prueba y el Lambda Cálculo de Alonzo Church, que capturó la noción de programa. Ambos se publicaron a principios de 1930.

Hasta finales de 1960 no se descubrió la correspondencia tan precisa que había entre las pruebas de Grentzen y los programas de Church. Introdujo la deducción natural en 1934. Muchas de las ideas son descendientes directas del trabajo de Frege. Alonzo Church introdujo el Lambda Cálculo en 1932. Fue entendido como un nuevo camino de formulación lógica. Hacia 1936, Church se dio cuenta de que los términos lambda podrían ser usados para expresar toda función que podría ser computada por una máquina. Al mismo tiempo, Turing escribió el famoso artículo de la máquina que lleva su nombre. Se reconoció rápidamente que ambas formulaciones eran equivalentes y Turing fue a estudiar a Princeton con Church entre 1936 y 1938.

Church redujo todas las nociones del cálculo de sustitución. Normalmente, un matemático debe definir una función mediante una ecuación. Por ejemplo, si una función f es definida por la ecuación f(x)=t, donde t es algún término que contiene a x, entonces la aplicación f(u) devuelve el valor t[u/x], donde t[u/x] es el término que resulta de sustituir u oir cada aparición de x en t.

Por ejemplo, si f(x)=x*x, entonces f(3)=3*3=9. Church propuso una forma especial (más compacta) de escribir estas funciones. En vez de decir “la función f donde f(x)=t”, él simplemente escribió \x.t. Para el ejemplo anterior: \x.x*x.
Un término de la forma \x.t se llama “lambda expresión”.

Church introdujo una versión tipada del lambda cálculo en 1940. Como ya hemos dicho había una correspondencia entre los trabajos de Church y Grentzen que fue descubierta logistas como Haskell Curry y W.A. Howard. Un artículo de Howard en el que se refleja dicha correspondencia fue escrito en 1969 pero no se publicó hasta 1980 debido a la influencia que podía ejercer. Church y Curry vivieron para ver el impacto tan importante que tuvieron sus teorías en los lenguajes de programación. Gentzen no fue tan afortunado ya que murió en 1945.

El Lambda Cálculo de Church tuvo un profundo impacto en el campo de los lenguajes de programación. El concepto de que funciones pueden tomar funciones como argumentos y devolver funciones, fue particularmente importante.
Lisp usó la palabra clave lambda para definir funciones pero su definición de una función difiere sutilmente de la que da el lambda cálculo.

Algunos de los lenguajes que se inspiraron en el lambda cálculo son: Iswin,
Scheme (un dialecto de Lisp), Miranda, Haskell...
Iswin y Scheme son no tipados (sin tipos) pero los otros tienen sistemas de tipos basados en los sistemas de Hindley-Milner y Girar-Reynolds. Standard ML se caracteriza por su exploración en el tipado de módulos, Haskell por el tipado de clases y O’Calm por el tipado de objetos orientados.


El impacto de la lógica.

La programación funcional con tipos tienen también una especial importancia en Java. Guy Steele unos de los 3 diseñadores principales de Java, empezó con Scheme.
John Roser otro programador de Scheme introdujo términos lambda en Java en forma de clases internas y son usadas para implementar llamadas en el GUI. Una nueva generación de lenguajes distribuidos está ahora en desarrollo, por ejemplo: Cálculo pi de Milner, Ámbito de Cardelli y Gordon, el cálculo de Fournier, Gonthier y otros...
Todos estos lenguajes siguen la tradición del lambda cálculo tipado.


Demostradores de teoremas

Hewlett-Packard aplicó el demostrador de teorema HOL para verificar que ciertos protocolos no sufrían interbloqueo. Con esto se descubrieron errores. El departamento de defensa y Tecnología Australiano está aplicando el demostrador de teorema Isabelle para verficar las condiciones de seguridad de ciertos misiles.

HOL e Isabelle están implementados en Standard ML, fue desarrollado por Gordon, Melham y otros con versiones publicadas en 1988,1990 y 1998; Isabelle fue desarrollado por Paulson, Nipkow y otros con versiones publicadas en 1988, 1994, 1998 y 1999.

ML/LCF explotó dos características principales centrales de los lenguajes funcionales:
- Funciones de orden superior.
- Tipos.

Una prueba táctica es una función a la que se le pasa una fórmula meta (final) para ser demostrada y que devuelve una lista de sub-metas emparejadas con una justificación.
Una justificación es una función que va de las pruebas a la prueba final.
Una táctica es una función que transforma tácticas pequeñas en tácticas grandes.

ML/LCF fue desarrollado por Mildner, Gordon y Wadsworth y la descripción completa fue publicada en 1979. HOL e Isabelle son sólo dos de los muchos demostradores de teoremas que aprovecharon las ideas de LCF, al igual que el estándar ML es sólo uno de los muchos lenguajes que aprovecharon las ideas desarrolladas en ML. Entre otros, COQ está implementado en CAML, Veritas en Miranda, Yarrow en Haskell y ALF,ELF y LEGO en Estándar ML también.



Confianza y Seguridad.

Cuando ejecutamos código máquina ¿hay algún modo de complementar la confianza de la persona que nos haya mandado ese código con un test que me garantice la seguridad?

La hay:
Lenguaje de tipos ensamblados, es uno de los modos.
El sistema de tipos desarrollado para el lambda cálculo es lo bastante flexible como para ser aplicado a otros lenguajes de programación de otros estilos y puede extenderse, incluso, al lenguaje máquina. En Java, los códigos bytes son declarados como tipos y diseñados en TAL (Grez Morriset 1998) que son chequeados por el verificador antes de ejecutar el código. Igualmente, en TAL, el código máquina es declarado con tipos que son chequeados por el chequeador de tipos antes de ejecutar el código.

Demostrador de teoremas Isabelle

El lenguaje en el cual se realizan las pruebas es HOL (acrónimo de Higher-Order Logic), que es un lenguaje fuertemente tipificado con estructuras de datos, funciones recursivas (incluyendo valores funcionales) y expresiones lógicas con cuantificadores.
Entre las características más destacables de Isabelle se pueden mencionar:

v Sistema de deducción natural
v Inferencia de tipos para verificar que los términos manejados estén bien construidos
v Módulos llamados teorías
v Conjuntos y tipos de datos recursivos
v Inducción estructural
v Facilidades para realizar demostraciones interactivas
v Simplificación por reescritura de términos.
Ejemplo extraído de un archivo de teoría

subsection{*Definición inductiva de los números pares*}

consts Par :: "nat set" Par de tipo conjunto de naturales
inductive Par Definición inductiva de par
intros
ZeroI: "0 : Par" Cero es par
Add2I: "n : Par ==> Suc(Suc n) : Par" n+2 es par si n lo es

text{* Uso de reglas de introducción: *}
lemma "Suc(Suc(Suc(Suc 0))) \ Par" 4 es par
apply(rule Add2I) Pasos de la prueba
apply(rule Add2I)
apply(rule ZeroI)
done

text{* Prueba inductiva sencilla: *}
lemma "n:Par ==> n+n : Par" 2n es par si n lo es
Pasos de la prueba
apply(erule Par.induct) Inducción basada en la def. de Par
apply(simp) simplificación
apply(rule Par.ZeroI)
apply(simp)
apply(rule Par.Add2I)
apply(rule Par.Add2I)
apply(assumption)
done





CONCLUSIÓN


La Visión artificial es una tecnología cada día más empleada en distintos ámbitos, en especial en la industria y difundida con frecuencia en medios técnicos. Sin embargo se emplean habitualmente muchos conceptos poco claros, cuando no directamente equivocados por todas las partes implicadas, proveedores, usuarios y técnicos en general. Por ello en este artículo se repasa algunos de los conceptos mas importantes, dando directivas sencillas y claras, aplicables muchas de ellas a otros problemas de sensórica y automatización.




No hay comentarios: