Máquina Gödel - Gödel machine

Uma máquina de Gödel é um programa de computador hipotético de autoaperfeiçoamento que resolve problemas de maneira otimizada. Ele usa um protocolo de autoaperfeiçoamento recursivo no qual reescreve seu próprio código quando pode provar que o novo código fornece uma estratégia melhor. A máquina foi inventada por Jürgen Schmidhuber (proposta pela primeira vez em 2003), mas tem o nome de Kurt Gödel, que inspirou as teorias matemáticas.

A máquina de Gödel é frequentemente discutida quando se trata de questões de meta-aprendizagem , também conhecidas como "aprender a aprender". Os aplicativos incluem a automação de decisões de design humano e transferência de conhecimento entre várias tarefas relacionadas, e podem levar ao design de arquiteturas de aprendizagem mais robustas e gerais. Embora teoricamente possível, nenhuma implementação completa foi criada.

A máquina de Gödel é muitas vezes comparado com Marcus Hutter 's AIXItl , outra especificação formal de uma inteligência geral artificial . Schmidhuber aponta que a máquina de Gödel pode começar implementando AIXItl como seu subprograma inicial e se auto-modificar depois de encontrar provas de que outro algoritmo para seu código de pesquisa será melhor.

Limitações

Os problemas tradicionais resolvidos por um computador requerem apenas uma entrada e fornecem alguma saída. Computadores desse tipo tiveram seu algoritmo inicial conectado. Isso não leva em consideração o ambiente natural dinâmico e, portanto, era um objetivo a ser superado pela máquina de Gödel.

A máquina de Gödel tem limitações próprias, entretanto. De acordo com o Primeiro Teorema da Incompletude de Gödel , qualquer sistema formal que englobe a aritmética é falho ou permite declarações que não podem ser provadas no sistema. Conseqüentemente, mesmo uma máquina de Gödel com recursos computacionais ilimitados deve ignorar aqueles auto-aperfeiçoamentos cuja eficácia ela não pode provar.

Variáveis ​​de interesse

Existem três variáveis ​​que são particularmente úteis no tempo de execução da máquina de Gödel.

• Em algum momento , a variável terá o equivalente binário de . Isso é incrementado continuamente ao longo do tempo de execução da máquina.${\ displaystyle t}$${\ displaystyle {\ text {time}}}$${\ displaystyle t}$

• Qualquer entrada destinada à máquina de Gödel do ambiente natural é armazenada em variável . É provável que mantenha valores diferentes para valores diferentes de variável .${\ displaystyle x}$${\ displaystyle x}$${\ displaystyle {\ text {time}}}$

• As saídas da máquina de Gödel são armazenadas em variável , onde seria a string de bits de saída em algum momento .${\ displaystyle y}$${\ displaystyle y (t)}$${\ displaystyle t}$

Em qualquer momento , onde , o objetivo é maximizar o sucesso futuro ou utilidade. Uma função de utilidade típica segue o padrão : ${\ displaystyle t}$${\ displaystyle (1 \ leq t \ leq T)}$${\ displaystyle u (s, \ mathrm {Env}): S \ times E \ rightarrow \ mathbb {R}}$

${\ displaystyle u (s, \ mathrm {Env}) = E _ {\ mu} {\ Bigg [} \ sum _ {\ tau = {\ text {time}}} ^ {T} r (\ tau) \ mid s, \ mathrm {Env} {\ Bigg]}}$

onde é uma entrada de recompensa com valor real (codificado dentro ) no tempo , denota o operador de expectativa condicional com relação a alguma distribuição possivelmente desconhecida de um conjunto de distribuições possíveis ( reflete tudo o que é conhecido sobre as reações possivelmente probabilísticas do ambiente), e o acima mencionado é uma função de estado que identifica exclusivamente o ciclo atual. Observe que levamos em consideração a possibilidade de estender a expectativa de vida por meio de ações apropriadas. ${\ displaystyle r (t)}$${\ displaystyle s (t)}$${\ displaystyle t}$${\ displaystyle E _ {\ mu} [\ cdot \ mid \ cdot]}$${\ displaystyle \ mu}$${\ displaystyle M}$${\ displaystyle M}$${\ displaystyle {\ text {time}} = \ operatorname {time} (s)}$${\ displaystyle s}$

Instruções usadas por técnicas de prova

A natureza das seis instruções de modificação de prova abaixo torna impossível inserir um teorema incorreto na prova, banalizando assim a verificação da prova.

get-axioma ( n )

Acrescenta o n -ésimo axioma como um teorema à seqüência de teoremas atual. Abaixo está o esquema inicial do axioma:

• Os axiomas de hardware especificam formalmente como os componentes da máquina podem mudar de um ciclo para o outro.
• Os Axiomas de Recompensa definem o custo computacional da instrução de hardware e o custo físico das ações de produção. Axiomas relacionados também definem a vida útil da máquina de Gödel como quantidades escalares que representam todas as recompensas / custos.
• Os axiomas de ambiente restringem a maneira como novas entradas x são produzidas a partir do ambiente, com base nas sequências anteriores de entradas y .
• Axiomas de incerteza / manipulação de cordas Os axiomas são axiomas padrão para aritmética, cálculo, teoria da probabilidade e manipulação de cordas que permitem a construção de provas relacionadas a valores de variáveis ​​futuras dentro da máquina de Gödel.
• Os Axiomas do Estado Inicial contêm informações sobre como reconstruir partes ou todo o estado inicial.
• Os Axiomas de Utilidade descrevem o objetivo geral na forma da função de utilidade u .

aplicar regra ( k , m , n )

Obtém o índice k de uma regra de inferência (como Modus tollens , Modus ponens ) e tenta aplicá-lo aos dois teoremas previamente provados m e n . O teorema resultante é então adicionado à prova.

deletar-teorema ( m )

Exclui o teorema armazenado no índice m na prova atual. Isso ajuda a mitigar as restrições de armazenamento causadas por teoremas redundantes e desnecessários. Teoremas excluídos não podem mais ser referenciados pela função de regra de aplicação acima .

set-switchprog ( m , n )

Substitui switchprog S ^p _{m: n} , desde que seja uma substring não vazia de S ^p .

Verifica()

Verifica se o objetivo da busca de prova foi alcançado. Um teorema alvo afirma que dada a função de utilidade axiomatizada atual u (Item 1f), a utilidade de uma mudança de p para o switchprog atual seria maior do que a utilidade de continuar a execução de p (o que continuaria procurando por switchprog alternativas). Isso é demonstrado na seguinte descrição da função check () decodificada para a Máquina Gödel:

${\ displaystyle D_ {KA} = {\ frac {d _ {\ text {poro}}} {3}} u = {\ frac {d _ {\ text {pore}}} {3}} {\ sqrt {\ frac {8 \ kappa NT} {\ pi M_ {A}}}}}$

estado2 teorema ( m , n )

Toma em dois argumentos, m e n , e as tentativas para converter o conteúdo de S _{m: n} em um teorema.

Aplicativos de exemplo

Otimização NP-difícil por tempo limitado

A entrada inicial para a máquina de Gödel é a representação de um grafo conectado com um grande número de nós ligados por arestas de vários comprimentos. Dentro de um determinado tempo, T deve encontrar um caminho cíclico conectando todos os nós. A única recompensa de valor de verdade vai ocorrer em tempo T . É igual a 1 dividido pelo comprimento do melhor caminho encontrado até agora (0 se nenhum foi encontrado). Não há outras entradas. O subproduto da maximização da recompensa esperada é encontrar o caminho mais curto encontrável dentro do tempo limitado, dado o viés inicial.

Prova rápida de teorema

Prove ou refute o mais rápido possível que todos os inteiros pares> 2 são a soma de dois primos ( conjectura de Goldbach ). A recompensa é 1 / t , onde t é o tempo necessário para produzir e verificar a primeira dessas provas.

Maximizando a recompensa esperada com recursos limitados

Um robô cognitivo que precisa de pelo menos 1 litro de gasolina por hora interage com um ambiente parcialmente desconhecido, tentando encontrar depósitos de gasolina escondidos e limitados para reabastecer ocasionalmente seu tanque. Ele é recompensado em proporção ao seu tempo de vida e morre após no máximo 100 anos ou assim que seu tanque estiver vazio ou cair de um penhasco, e assim por diante. As reações ambientais probabilísticas são inicialmente desconhecidas, mas presume-se que sejam amostradas do Speed ​​Prior axiomatizado, de acordo com o qual reações ambientais difíceis de computar são improváveis. Isso permite uma estratégia computável para fazer previsões quase ótimas. Um subproduto da maximização da recompensa esperada é maximizar a vida útil esperada.

Veja também

• Teoremas da incompletude de Gödel

Referências

links externos

• Página inicial das máquinas Goedel
• Máquinas Goedel: solucionadores de problemas universais e auto-referenciais, fazendo melhorias comprovadamente ideais