Programação em lógica indutiva

Programação em lógica indutiva (ILP) é um subcampo de aprendizado de máquina que utiliza lógica de programação como uma representação uniforme, por exemplo, conhecimento prévio e hipóteses. Dada uma codificação de conhecimento prévio e um conjunto de exemplos representado como uma lógica de banco de dados de fatos, um sistema ILP irá derivar um programa de lógica hipotetizado que envolve todos os aspectos positivos e nenhum dos exemplos negativos.

• Esquema: os exemplos positivos + exemplos negativos + conhecimento prévio ⇒ hipótese.

Programação em lógica indutiva é particularmente útil em bioinformática e processamento de linguagem natural. Gordon Plotkin e Ehud Shapiro definiram a fundamentação teórica inicial para aprendizagem de máquina indutiva em uma lógica de definição. Shapiro construiu a sua primeira implementação (Sistema de Modelo de Inferência), em 1981: um programa Prolog que indutivamente inferia programas lógicos de exemplos positivos e negativos. O termo Programação em lógica indutiva foi introduzido pela primeira vez em um artigo publicado por Stephen Muggleton , em 1991. Muggleton também fundou a conferência internacional sobre Programação em lógica indutiva, introduziu as idéias teóricas de Invenção de Predicado, Resolução inversa, e Implicação Inversa. Muggleton implementado Implicação Inversa primeiro no sistema PROGOL. O termo "indutivo" aqui refere-se ao filosófico (por exemplo, sugerindo uma teoria para explicar fatos observados), ao invés do matemático (por exemplo, a prova de propriedade para todos os membros de um conjunto ordenado) de indução.

Definição Formal

O conhecimento de prévio é dado como uma lógica da teoria B, comumente na forma de cláusulas de Horn usado em lógica de programação. Os exemplos positivos e o negativos são fornecidos como um conjunto ${\displaystyle }$ e ${\displaystyle }$ de não negados e negados literais, respectivamente. Uma hipótese correta h é uma proposição lógica satisfazer os seguintes requisitos.

${\displaystyle }$

"Necessidade" não impõe uma restrição sobre h, mas proíbe qualquer geração de uma hipótese, enquanto os fatos positivos são explicáveis sem ela. "Suficiência" requer qualquer hipótese gerada h para explicar todos os exemplos positivos ${\displaystyle }$. "A fraca consistência" proíbe a geração de qualquer hipótese h que contradiz o conhecimento prévio B. "Consistência forte" também proíbe a geração de qualquer hipótese h que é inconsistente com os exemplos negativos ${\displaystyle }$, dado o conhecimento prévio B; isso implica "Fraca consistência"; se exemplos negativos não são dados, ambas as exigências coincidem. Džeroski exige apenas "Suficiência" (chamado de "Integridade" e "Forte consistência".

Exemplo

Relações familiares assu na secção "Exemplo"

O seguinte exemplo bem conhecido sobre a aprendizagem definições das relações familiares usa abreviaturas

${\displaystyle }$, ${\displaystyle }$, ${\displaystyle }$, ${\displaystyle }$, ${\displaystyle }$, ${\displaystyle }$, ${\displaystyle }$, ${\displaystyle }$e ${\displaystyle }$.

Ele começa a partir do conhecimento prévio (imagem)

${\displaystyle }$,

os exemplos positivos

${\displaystyle }$,

e a proposição trivial ${\displaystyle }$ para indicar a ausência de exemplos negativos.

A abordagem de "generalização relativa menos geral (rlgg)" de Plotkin para Programação em Lógica Indutiva deve ser utilizada para obter uma sugestão sobre como definir formalmente a relação filha {\textit {dau}}.

Esta abordagem utiliza os seguintes passos.

• Relativizar cada exemplo de literal positivo com o conhecimento prévio completo:

  ${\begin{aligned}{\textit {dau}}(m,h)\leftarrow {\textit {par}}(h,m)\land {\textit {par}}(h,t)\land {\textit {par}}(g,m)\land {\textit {par}}(t,e)\land {\textit {par}}(n,e)\land {\textit {fem}}(h)\land {\textit {fem}}(m)\land {\textit {fem}}(n)\land {\textit {fem}}(e)\\{\textit {dau}}(e,t)\leftarrow {\textit {par}}(h,m)\land {\textit {par}}(h,t)\land {\textit {par}}(g,m)\land {\textit {par}}(t,e)\land {\textit {par}}(n,e)\land {\textit {fem}}(h)\land {\textit {fem}}(m)\land {\textit {fem}}(n)\land {\textit {fem}}(e)\end{aligned}}$,

• Converter para forma normal conjuntiva:

  ${\begin{aligned}{\textit {dau}}(m,h)\lor \lnot {\textit {par}}(h,m)\lor \lnot {\textit {par}}(h,t)\lor \lnot {\textit {par}}(g,m)\lor \lnot {\textit {par}}(t,e)\lor \lnot {\textit {par}}(n,e)\lor \lnot {\textit {fem}}(h)\lor \lnot {\textit {fem}}(m)\lor \lnot {\textit {fem}}(n)\lor \lnot {\textit {fem}}(e)\\{\textit {dau}}(e,t)\lor \lnot {\textit {par}}(h,m)\lor \lnot {\textit {par}}(h,t)\lor \lnot {\textit {par}}(g,m)\lor \lnot {\textit {par}}(t,e)\lor \lnot {\textit {par}}(n,e)\lor \lnot {\textit {fem}}(h)\lor \lnot {\textit {fem}}(m)\lor \lnot {\textit {fem}}(n)\lor \lnot {\textit {fem}}(e)\end{aligned}}$,

• Anti-unificar cada par compatível   de literais:
  • ${\textit {dau}}(x_{me},x_{ht})$ de ${\textit {dau}}(m,h)$ e ${\textit {dau}}(e,t)$,
  • $\lnot {\textit {par}}(x_{ht},x_{me})$ de $\lnot {\textit {par}}(h,m)$ e $\lnot {\textit {par}}(t,e)$,
  • $\lnot {\textit {fem}}(x_{me})$ de $\lnot {\textit {fem}}(m)$ e $\lnot {\textit {fem}}(e)$,
  • $\lnot {\textit {par}}(g,m)$ de $\lnot {\textit {par}}(g,m)$ e $\lnot {\textit {par}}(g,m)$, similar para qualquer outro literal de conhecimento prévio:
  • $\lnot {\textit {par}}(x_{gt},x_{me})$ de $\lnot {\textit {par}}(g,m)$ e $\lnot {\textit {par}}(t,e)$, e muitos mais literais negados
• Excluir todos os literais negados contendo variáveis que não ocorrem em um literal positivo:
  • Após excluir todos os literais negados contendo outras variáveis além de $x_{me},x_{ht}$, somente ${\textit {dau}}(x_{me},x_{ht})\lor \lnot {\textit {par}}(x_{ht},x_{me})\lor \lnot {\textit {fem}}(x_{me})$ resta, juntamente com todos os literais que vieram do conhecimento prévio
• Converter cláusulas de volta para a forma de Horn:
  • ${\textit {dau}}(x_{me},x_{ht})\leftarrow {\textit {par}}(x_{ht},x_{me})\land {\textit {fem}}(x_{me})\land ({\text{all background knowledge facts}})$

A cláusula de Horn resultante é a hipótese h obtida pela abordagem rlgg. Ignorando os fatos do conhecimento prévio, a cláusula informalmente lê "x_{{me}} é chamado de uma filha de x_{{ht}} se x_{{ht}} é o pai de x_{{me}} e x_{{me}} é feminina", que é uma definição comumente aceita.

Sobre os requisitos acima, "Necessidade" estava satisfeita porque o predicado ${\displaystyle }$ não aparece no conhecimento prévio, o que, portanto, não implica qualquer propriedade que contém esse predicado, tal como os exemplos positivos são. "Suficiência" é satisfeita pela hipótese h calculada, pois, juntamente com ${\displaystyle }$ a partir do conhecimento prévio, implica o primeiro exemplo positivo ${\displaystyle }$, e da mesma forma h e ${\displaystyle }$ a partir do conhecimento prévio implica o segundo exemplo positivo ${\displaystyle }$. "A fraca consistência" é satisfeita por h, pois h detém na estrutura de Herbrand (finita) descrita pelo conhecimento prévio; semelhante para o "Consistência forte".

A definição comum da relação avó, ${\displaystyle }$, não pode ser aprendida através da abordagem acima, uma vez que a variável y ocorre somente na cláusula corpo; os literais correspondentes teriam sido eliminados na 4ª etapa da abordagem. Para superar essa falha, que passo tem que ser modificada de tal forma que possa ser parametrizada com diferentes heurística de pós-seleção de literais. Historicamente, a implementação GOLEM é baseada na abordagem rlgg.

Systema de Programação em Lógica Indutiva

Systema de Programação em Lógica Indutiva é um programa que toma como entrada teorias lógicas ${\displaystyle }$ e saída uma hipótese correta H em relação a essas teorias. Um algoritmo de um sistema de ILP é composto de duas partes: a hipótese de pesquisa e hipótese de seleção. Primeiro uma hipótese é pesquisada com um método de Programação em Lógica Indutiva, em seguida, um subconjunto das hipóteses encontradas (na maioria dos sistemas, uma hipótese) é escolhido por um algoritmo de seleção. Um algoritmo de seleção de pontua cada um das hipóteses e devolve aquelas com a maior pontuação. Um exemplo de função de pontuação inclue compactação mínima de comprimento onde de uma hipótese com uma menor complexidade de Kolmogorov tem a pontuação mais alta e é devolvida. Um sistema de ILP é completa se e somente se para qualquer entrada de teorias lógicas ${\displaystyle }$ qualquer hipótese correta H em relação a estas teorias pode ser encontrad com seu método de pesquisa de hipótese.

Pesquisa de Hipótese

Modernos sistemas de ILP como Progol, Saraiva, e Imparo encontram uma hipótese H , utilizando o princípio da implicação inversa para as teorias B, E, H: ${\displaystyle }$. Primeiro eles constroem uma teoria intermediária F chamada de uma teoria ponte que satisfaça as condições ${\displaystyle }$ e ${\displaystyle }$. Em seguida, como ${\displaystyle }$, eles generalizam a negação da teoria ponte F com a anti-implicação. No entanto, a operação de anti-implicação, sendo altamente não-determinística, é computacionalmente mais cara. Portanto, uma pesquisa de hipótese alternativa pode ser conduzida usando a operação da inversa de classificação (anti-subsunção), que é menos não-determinística que anti-implicação.

Perguntas sobre completude de uma pesquisa de hipótese específica de um sistema ILP de surgiram. Por exemplo, Progol o método de pesquisa de hipótese com base na regra de inferência da implicação inversa não é completa pelo  exemplo de Yamamoto . por outro lado, Imparo é completa, tanto para o método de anti-implicação  quanto para o método de classificação inversa extendida .

Implementações

• 1BC e 1BC2: de primeira ordem naive Bayesian classificadores: (http://www.cs.bris.ac.uk/Research/MachineLearning/1BC/)
• ACE (UM Combinado do Motor) (http://dtai.cs.kuleuven.be/ACE/)
• Aleph (http://web.comlab.ox.ac.uk/oucl/research/areas/machlearn/Aleph/)
• Átomo (http://www.ahlgren.info/research/atom/)
• Claudien (http://dtai.cs.kuleuven.be/claudien/)
• DL-Aluno (http://dl-learner.org)
• (Dmáxhttp://dtai.cs.kuleuven.be/dmax/)
• FOLHA (ftp://ftp.cs.su.oz.au/pub/foil6.sh)
• Golem (ILP) (http://www.doc.ic.ac.uk/~shm/Software/golem)
• Imparo
• Inthelex (INcremental Teoria de Aprendiz, a partir de Exemplos)http://lacam.di.uniba.it:8000/systems/inthelex/)
• Limão:http://cs.anu.edu.au/people/Eric.McCreath/lime.html)
• Metagol (http://github.com/metagol/metagol)
• Mio (http://libra.msra.cn/Publication/3392493/mio-user-s-manual)
• MIS (Modelo de Inferência do Sistema) por Ehud Shapiro
• PROGOL (http://www.doc.ic.ac.uk/~shm/Software/progol5.0)
• RSD (http://labe.felk.cvut.cz/~zelezny/rsd/)
• Tércio (http://www.cs.bris.ac.uk/publications/Papers/1000545.pdf)
• Warmr (agora incluído no ACE)
• ProGolem (http://ilp.doc.ic.ac.uk/ProGolem/)

Veja também

• Raciocínio de senso comum
• Conceito de análise formal
• Método Indutivo
• Raciocínio indutivo
• Programação Indutiva
• Probabilidade Indutiva
• Estatísticas relacionais de aprendizagem
• Versão espaço de aprendizagem