Redes profundas podem ser treinadas para provar teoremas?

Suponha que tenhamos um grande número de provas no cálculo de predicado de primeira ordem. Suponhamos que também tenhamos axiomas, corolários e teoremas nessa área da matemática dessa forma.

Considere cada proposição que foi provada e o corpo da teoria existente em torno dessa proposição específica como um exemplo em um conjunto de treinamento e uma boa prova conhecida da proposição como os rótulos associados. Agora, considere uma rede artificial profunda projetada especificamente para treinar neste conjunto de exemplos e os hiperparâmetros configurados corretamente para isso.

É possível treinar uma rede artificial profunda de tal maneira que a apresentação de uma nova proposição e a teoria existente em torno dela, apresentada em cálculo de predicados de primeira ordem na entrada, produzam uma prova na saída?

(Obviamente, essas provas devem ser verificadas manualmente.)

Se a proporção de boas provas resultantes for suficientemente alta, será possível criar um algoritmo genético que proponha proposições à rede profunda treinada, criando assim provas?

Isso é possível?

Seria possível usar esse tipo de projeto de rede profunda para resolver a conjectura de Collatz ou Riemann ou, pelo menos, reorganizar padrões de uma maneira que os matemáticos sejam mais capazes de chegar a uma prova legítima?

Os sistemas de produção existentes, desenvolvidos nas últimas décadas, têm as regras de inferência codificadas neles. Eles são baseados na visão de Leibniz de que toda a lógica clássica pode ser codificada em linguagem simbólica e processada mecanicamente. A lógica de predicados de primeira ordem foi desenvolvida e uma nomeclatura foi formalizada.

Embora a visão da prova automática do teorema tenha sido consideravelmente contestada pelos dois teoremas da incompletude de Gödel, o trabalho de completude de Turing e o desenvolvimento de uma arquitetura para realizá-lo praticamente por von Neumann reviveram o trabalho para automatizar o processo mecânico de inferência.

O laboratório de IA do MIT, durante o tempo de Minsky, estava vivo com esses esforços, mas o que eles chamaram de explosão combinatória mostrou que havia disponibilidade insuficiente de recursos de computação para procurar o espaço necessário para provar automaticamente teoremas arbitrários de complexidade não trivial. Grandes computadores paralelos chamados máquinas de conexão e vários esquemas, usando meta regras e abordagens heurísticas, foram empregados para superar o problema de explosão combinatória.

Redes artificiais foram introduzidas e a idéia de que poderiam rivalizar com as máquinas de produção foi rejeitada pela comunidade LISP quando proposta pela primeira vez. No entanto, no contexto de considerável sucesso no aumento dos recursos de computação e nas recentes conquistas do aprendizado de máquina, muitos começaram a fazer perguntas que foram arquivadas no século XX.

Já sabemos que as redes artificiais podem aprender funções lógicas e algébricas arbitrárias, muitas das quais são aprendidas pelo PAC. ¹ Dado o ambiente de aprendizado adequado, aprender inferência lógica é claramente algo que o córtex cerebral pode fazer no seu ponto atual da evolução. Se as redes neurais atingirão esse nível de cognição é uma questão em aberto.

Essa pesquisa convencional de IA e aprendizado de máquina não está focada na aquisição de redes artificiais de regras de inferência lógica, principalmente porque programá-las em um sistema como o DRools e outros sistemas de produção comumente usados ​​parece que a abordagem mais racional não significa que sempre será. A questão é se existe um retorno suficiente sobre o investimento para fazer o que pode ser interessante, mas certamente caro, quando outras soluções já existem.

Essa pergunta é semelhante a outra pergunta do Artificial Intelligence Stack Exchange sobre o quão boa é a IA em matemática. Uma das respostas dadas lá é aplicável aqui.

É importante não descartar nenhuma abordagem nesse período, já que o interesse recente em IA não apenas reacendeu os gastos do governo, mas também os gastos comerciais. Esse gasto aumenta o pessoal, o poder da computação e o incentivo para superar os obstáculos que antes se pensava serem intransponíveis.

Notas de rodapé

[1] O PAC Learning é uma estrutura para determinar a computabilidade prática dos algoritmos de aprendizado, dadas as características da classe de hipóteses que podem ser aprendidas usando o modelo fornecido e a precisão e confiança esperadas do processo de aprendizado.

Sua ideia pode ser viável em geral, mas uma rede neural é provavelmente a ferramenta de alto nível errada a ser usada para explorar esse problema.

A força de uma rede neural é encontrar representações internas que permitam uma solução altamente não linear ao mapear entradas para saídas. Quando treinamos uma rede neural, esses mapeamentos são aprendidos estatisticamente através da repetição de exemplos. Isso tende a produzir modelos que interpolam bem quando recebem dados semelhantes ao conjunto de treinamento, mas que extrapolam mal.

Os modelos de redes neurais também não têm contexto, de modo que, se você usou um modelo generativo (por exemplo, um RNN treinado em sequências que criam provas válidas ou interessantes), ele pode facilmente produzir lixo estatisticamente agradável, mas sem sentido.

O que você precisará é de algum princípio organizador que permita explorar e confirmar provas de maneira combinatória. De fato, algo como a sua ideia já foi feito mais de uma vez, mas não consigo encontrar uma referência atualmente.

Nada disso impede você de usar uma rede neural dentro de uma IA que procura por provas. Pode haver lugares dentro de uma IA de matemática em que você precise de uma boa heurística para orientar pesquisas, por exemplo - por exemplo, no contexto, X é a sub prova Y e provavelmente interessante ou relevante. Avaliar um escore de probabilidade é algo que uma rede neural pode fazer como parte de um esquema mais amplo de IA. É semelhante à maneira como as redes neurais são combinadas com o aprendizado por reforço.

Pode ser possível construir sua idéia integralmente a partir de redes neurais em princípio. Afinal, existem boas razões para suspeitar que o raciocínio humano funciona de maneira semelhante usando neurônios biológicos (não provado que os artificiais possam corresponder a isso de qualquer maneira). No entanto, a arquitetura desse sistema está além de qualquer configuração moderna de design ou treinamento da NN. Definitivamente, não se trata apenas de adicionar camadas suficientes e alimentar os dados.

O que nós sabemos

De acordo com uma página do Banco Mundial , "Hoje, existem cerca de 200 milhões de estudantes do ensino superior no mundo, contra 89 milhões em 1998". Pelo menos 1 em 100, como requisito de matemática, teve que desenvolver uma prova para um teorema e viver pelo menos 40 anos depois.

Embora existam pelo menos 20 milhões de redes neurais que possam provar um teorema, elas ficam aquém dos exemplos que responderiam afirmativamente a essa pergunta. Essas redes neurais são biológicas, não artificiais, e na maioria das vezes têm teoremas comprovados anteriormente, não a conjectura de Collatz ou a conjectura de Riemann.

O que alguns acreditam

Aqueles que acreditam que o aprendizado profundo de Q e os dispositivos baseados em atenção serão acompanhados por outros projetos de sistemas de aprendizagem até que as faculdades do cérebro humano sejam simuladas e talvez superadas, provavelmente incluiriam a prova do teorema como uma dessas capacidades humanas. Provavelmente, eles declarariam lógica e inferência de predicados como apenas outra função cognitiva complexa que será alcançada em sistemas artificiais.

Aqueles que acreditam que algumas capacidades estão imbuídas em seres humanos e são capacidades reservadas, podem declarar lógica e inferência predicadas como reservadas apenas aos seres humanos.

Estado atual do progresso

Não há artigos acadêmicos indicando a capacidade de provar até as provas mais simples usando lógica e inferência predicadas. É possível que um governo ou empresa privada tenha alcançado algum nível de sucesso ao fazê-lo, mas isso não foi divulgado.

A ideia de que redes artificiais, se desenvolvidas de maneira apreciável, poderiam superar sistemas de produção, sistemas de IA baseados em produções ou regras, em suas áreas de maior eficácia, foi proposta no início do desenvolvimento da IA. Foi disputado naquela época e disputado agora, no entanto, os argumentos não são matemáticos, portanto não há forte indicação de que seja impossível.

Certamente outros aspectos cognitivos do pensamento humano são objetivos importantes da pesquisa em IA. Diálogo, educação automatizada, planejamento, análise estratégica e pilotagem de veículos são todos aspectos do pensamento superior que exigem mais do que DQN e abordagens de rede baseadas em atenção agora podem oferecer, mas o esforço de pesquisa nessas áreas é apreciável e bem financiado.

Abordagem Potencial

A pesquisa em relação às habilidades cognitivas lógicas deve iniciar provas já conhecidas, muito mais simples do que as conjecturas mencionadas na pergunta. Por exemplo, foi provado que a soma de dois números inteiros não negativos deve ser outro número inteiro não negativo. No cálculo de predicado, isso pode ser representado como uma sequência de caracteres.

$\forall a∈C, b∈C: s=a+b \implies s∈C$

Ele diz que aeb são membros do conjunto de números de contagem, que os s, definidos como a soma dos dois, também devem ser membros do conjunto de números de contagem. Sua prova também pode ser representada como uma sequência de cadeias de caracteres do cálculo de predicados de primeira ordem.

Nenhum projeto de pesquisa pequeno

Esse exemplo pode parecer simples para alguém que fez anos de cursos de matemática e construiu provas. Não é simples para uma criança, e é muito difícil fazer com que uma rede artificial converja para uma função que aplique todas as regras de inferência lógica e incorpore meta-regras para chegar a uma prova de um sistema formal como a aritmética inteira.

Turing redes completas, como RNNs, certamente terá vantagens sobre MLPs (perceptrons multicamadas). As redes baseadas em atenção podem ser uma opção de pesquisa razoável. Existem outros indicados nas referências abaixo.

Uma plataforma de computação paralela seria necessária para a pesquisa, já que o vetor de entrada pode ser centenas de Kbytes. É difícil estimar o tamanho dos exemplos e quantos seriam necessários sem levar um ano ou dois para o processo de pesquisa.

A definição dos números de contagem, o sinal de mais e o sinal de igual devem primeiro ser definidos, e essas definições e vários axiomas, postulados, lemas e corolários devem fazer parte do exemplo de entrada na forma formal, como a proposta a ser comprovado acima, juntamente com essa proposta.

E esse é o trabalho de preparar apenas um exemplo. Você precisaria de milhares para treinar conhecimento intuitivo sobre as regras de inferência em uma rede profunda. (Escolhi a palavra INTUITIVA deliberadamente por razões teóricas que levariam pelo menos cem páginas para explicar bem.)

Este não é um projeto pequeno, pois o conjunto de dados de exemplo deve ter pelo menos alguns milhares de casos, e cada caso, embora possa compartilhar alguma teoria, deve ser configurado para que a proposta seja perfeitamente formada e o corpo de teoria necessário também seja apresentado. de forma perfeita na entrada para cada iteração de treinamento.

Meu palpite é que seria necessário uma equipe de pesquisadores brilhantes com o entendimento apropriado de redes profundas, convergência e cálculo de predicados por cerca de dez anos para treinar uma rede para fornecer provas viáveis ​​em resposta a simples propostas matemáticas.

Mas não seria uma pequena conquista

Isso pode parecer um esforço absurdo para alguns, mas seria a primeira vez que alguém ensinaria um computador a ser lógico. A natureza precisou apenas da idade da terra para ensinar inferência lógica a um organismo, Sócrates.

As pessoas assumem que, como um computador é composto de circuitos digitais que executam a lógica por design, os computadores são lógicos. Qualquer pessoa que esteja envolvida no desenvolvimento de software há décadas com a tendência de pensar mais profundamente do que hackers por diversão ou dinheiro sabe de maneira diferente. Mesmo após uma programação cuidadosa, os computadores não simulam inferência lógica e não podem corrigir seu próprio comportamento programado para qualquer bug arbitrário. De fato, a maior parte do desenvolvimento de software atualmente é de correção de bugs.

Simular o pensamento lógico seria um passo importante para simular a cognição e o conjunto mais amplo de capacidades humanas.

Referências

Aprendendo a redigir redes neurais para responder perguntas Jacob Andreas, Marcus Rohrbach, Trevor Darrell e Dan Klein UC, Berkeley 2016 https://arxiv.org/pdf/1601.01705.pdf

Aprendendo várias camadas de representação Geoffrey E. Hinton Departamento de Ciência da Computação, Universidade de Toronto 2007 http://www.csri.utoronto.ca/~hinton/absps/ticsdraft.pdf

Máquina de Turing Neural (apresentação de slides) Autor: Alex Graves, Greg Wayne, Ivo Danihelka Apresentado por: Tinghui Wang (Steve) https://eecs.wsu.edu/~cook/aiseminar/papers/steve.pdf

Máquinas de Turing Neural (papel) Alex Graves, Greg Wayne, Ivo Danihelka https://pdfs.semanticscholar.org/c112/6fbffd6b8547a44c58b192b36b08b18299de.pdf 2014

Aprendizado por Reforço, Neural Turing Machines Wojciech Zaremba, papel da conferência Ilya Sutskever ICLR https://arxiv.org/pdf/1505.00521.pdf?utm_content=buffer2aaa3&utm_medium=social&utm_source=twitter.com&utm_campaign=buffer 2016

Máquina de Turing Neural Dinâmica com Esquemas de Endereçamento Contínuo e Discreto Caglar Gulcehre1, Sarath Chandar1, Kyunghyun Cho2, Yoshua Bengio1 https://arxiv.org/pdf/1607.00036.pdf 2017

Uma rede de inferência nebulosa autoconstrutiva on-line e suas aplicações Transações IEEE de Chia-Feng Juang e Chin-Teng Lin IEEE em sistemas nebulosos, v6, n1 1998 https://ir.nctu.edu.tw/bitstream/11536/ 32809/1 / 000072774800002.pdf

Redes Neurais de Sequência de Gated Gated Yujia Li e Richard Zemel ICLR conference paper 2016 https://arxiv.org/pdf/1511.05493.pdf

Construindo Máquinas que Aprendem e Pensam como Pessoas Brenden M. Lake, Tomer D. Ullman, Joshua B. Tenenbaum e Samuel J. Gershman Ciências do Comportamento e do Cérebro 2016 https://arxiv.org/pdf/1604.00289.pdf

Redes neurais profundas pré-treinadas e dependentes de contexto para reconhecimento de fala de grande vocabulário George E. Dahl, Dong Yu, Li Deng e Alex Acero Transações do IEEE sobre processamento de áudio, linguagem e linguagem 2012 https://s3.amazonaws.com/ academia.edu.documents / 34691735 / dbn4lvcsr-transaslp.pdf? AWSAccessKeyId = AKIAIWOWYYGZ2Y53UL3A & Expira = 1534211789 & Signature = 33QcFP0JGFeA% 2FTsqjQZpXYrIGm%% 3D & response-content 3D

Incorporando entidades e relações para aprendizagem e inferência em bases de conhecimento Bishan Yang1, Wen-tau Yih2, Xiaodong He2, Jianfeng Gao2 e Li Deng2, documento da conferência ICLR 2015 https://arxiv.org/pdf/1412.6575.pdf

Um algoritmo de aprendizagem rápida para redes de crença profunda Geoffrey E. Hinton, Simon Osindero, Yee-Whye Teh (comunicado por Yann Le Cun) Computação Neural 18 2006 http://axon.cs.byu.edu/Dan/778/papers/Deep % 20Networks / hinton1 * .pdf

FINN: Uma estrutura para inferência rápida e escalonável de redes neurais binárias Yaman Umuroglu, et al 2016 2016 https://arxiv.org/pdf/1612.07119.pdf

Do aprendizado de máquina ao raciocínio de máquina Léon Bottou 8/8/2011 https://arxiv.org/pdf/1102.1808.pdf

Aprendizado profundo Yann LeCun1,2, Yoshua Bengio3 e Geoffrey Hinton4,5 Nature vol 521 2015 https://www.evl.uic.edu/creativecoding/courses/cs523/slides/week3/DeepLearning_LeCun.pdf

É possível, mas provavelmente não é uma boa ideia.

A prova lógica é uma das áreas mais antigas da IA, e existem técnicas criadas para fins específicos que não precisam ser treinadas e que são mais confiáveis ​​do que uma abordagem de rede neural seria, uma vez que elas não se baseiam no raciocínio estatístico , e use o amigo do matemático: raciocínio dedutivo.

O campo principal é chamado "Prova automatizada de teoremas " e é suficientemente antigo para ser calcificado um pouco como uma área de pesquisa. Não há muitas inovações, mas algumas pessoas ainda trabalham nisso.

A idéia básica é que a prova de teoremas é apenas uma pesquisa guiada clássica ou heurística: você parte de um estado que consiste em um conjunto de premissas aceitas. Em seguida, você aplica qualquer regra lógica de inferência válida para gerar novas premissas que também devem ser verdadeiras, expandindo o conjunto de conhecimentos que você possui. Eventualmente, você pode provar a premissa desejada, por meio de pesquisas enumerativas, como a primeira pesquisa de largura ou aprofundamento iterativo , ou através de algo como A * com uma heurística específica do domínio. Muitos solucionadores também usam apenas uma regra lógica ( unificação ) porque é completa e reduz o fator de ramificação da pesquisa.