Lógica, explicabilidade e entendimento futuro

Descoberta relacionada à lógica

A lógica é a base de muitas coisas. Mas quais são os fundamentos da própria lógica?

Na lógica simbólica, símbolos como peq são introduzidos para denotar afirmações (ou "proposições") do tipo "este é um ensaio interessante". Ainda existem certas regras de lógica, por exemplo, para qualquer p e q a expressão NOT (p AND q) é semelhante a (NOT p) OR (NOT q).

Mas de onde vêm essas "regras da lógica"? A lógica é um sistema formal. Como a geometria euclidiana, ela pode ser construída em axiomas. Mas o que são axiomas? Você pode começar com instruções como p AND q = q AND p, ou NOT NOT p = p. Mas quantos axiomas são necessários? Quão simples eles podem ser?

Esta questão tem sido dolorosa. Mas às 20:31 do domingo, 29 de janeiro de 2000, o único axioma apareceu na tela do meu computador. Eu já mostrei que nada poderia ser mais simples, mas logo estabeleci que esse pequeno axioma era suficiente para criar toda a lógica:


Como eu sabia que ela era verdadeira? Porque eu fiz o computador provar isso. E aqui está a prova que imprimi no livro “ Um Novo Tipo de Ciência ” (já disponível no repositório Wolfram Data ):


Usando a versão mais recente do Wolfram Language, qualquer pessoa pode gerar essa prova em não mais de um minuto. E todos os seus passos são fáceis de verificar . Mas por que o resultado será verdadeiro? Como explicar isso?

Cada vez mais perguntas semelhantes estão sendo feitas sobre todos os tipos de sistemas e aplicativos de computação relacionados ao aprendizado de máquina e à IA. Sim, vemos o que está acontecendo. Mas podemos entender isso?

Penso que esta questão é profundamente inerente - e criticamente importante para o futuro da ciência e da tecnologia e para o futuro de todo o desenvolvimento intelectual.

Mas antes de falarmos sobre isso, vamos discutir o axioma que eu descobri.

A história

A lógica como disciplina formal vem de Aristóteles, que viveu no século IV aC. Como parte do trabalho de sua vida em catalogar coisas (animais, razões etc.), Aristóteles compilou um catálogo de formas permissíveis de argumentos e criou modelos simbólicos para eles, os quais, em essência, forneceram o conteúdo principal da lógica por dois mil anos à frente.

No entanto, no século XV, a álgebra foi inventada e, com ela, uma imagem mais clara das coisas apareceu. Mas foi somente em 1847 que George Bull finalmente formulou a lógica da mesma maneira que a álgebra, com operações lógicas como AND e OR trabalhando de acordo com regras semelhantes às regras da álgebra.

Depois de alguns anos, as pessoas já estavam escrevendo sistemas axiomáticos para a lógica. Um exemplo típico foi:


Mas são AND, OR e NOT realmente necessários para a lógica? Após a primeira década do século XX, várias pessoas descobriram que a única operação que agora chamamos de NAND será suficiente e, por exemplo, p OR q pode ser calculado como (p NAND p) NAND (q NAND q). A "completude funcional" da NAND poderia permanecer para sempre estranha se não fosse o desenvolvimento da tecnologia de semicondutores - implementa todos os bilhões de operações lógicas em um microprocessador moderno usando uma combinação de transistores que executam apenas a função NAND ou a NOR associada.

Bem, como são os axiomas da lógica em termos de NAND? Aqui está a primeira versão conhecida deles, gravada por Henry Schaeffer em 1913 (aqui o ponto indica NAND):


Em 1910, Principia Mathematica, um trabalho de três volumes sobre a lógica e a filosofia da matemática de Alfred North Whitehead e Bertrand Russell, popularizou a idéia de que talvez toda a matemática possa ser deduzida da lógica. Diante disso, foi bastante interessante estudar a questão de quão simples os axiomas da lógica podem ser. O trabalho mais significativo nessa área foi realizado em Lviv e Varsóvia (então essas cidades faziam parte da Polônia), em particular Jan Lukasevich (como efeito colateral de seu trabalho em 1920, ele inventou um registro "polonês" que não requer colchetes). Em 1944, aos 66 anos, Lukasevich fugiu do avanço do exército soviético e em 1947 acabou na Irlanda.

Enquanto isso, o irlandês Carew Meredith, que estudou em Winchester e Cambridge, e se tornou professor de matemática em Cambridge, foi forçado a retornar à Irlanda em 1939 por causa de seu pacifismo. Em 1947, Meredith assistiu à palestra de Lukasevich em Dublin, que o inspirou a procurar axiomas simples, o que ele fez, na maioria das vezes, pelo resto de sua vida.

Em 1949, Meredith descobriu um sistema de dois axiomas:


Quase 20 anos depois, em 1967, ele conseguiu simplificar isso para:


É possível simplificar ainda mais isso? Meredith vem mexendo nisso há anos, descobrindo onde mais você pode remover o NAND extra. Mas depois de 1967, ele não avançou mais (e morreu em 1976), embora em 1969 tenha encontrado um sistema de três axiomas:


Quando comecei a estudar sistemas de axioma da lógica, não sabia nada sobre o trabalho de Meredith. Fiquei interessado neste tópico como parte de uma tentativa de entender qual comportamento pode resultar de regras simples. Nos anos 80, descobri inesperadamente que mesmo os autômatos celulares com as regras mais simples possíveis - como minha regra favorita 30 - podem levar a um comportamento incrivelmente complexo.

Depois de passar a década de 1990, na tentativa de entender a generalidade desse fenômeno, eu finalmente quis ver como ele pode ser aplicado à matemática. Na matemática, de fato, começamos a trabalhar com axiomas (por exemplo, em aritmética, em geometria, em lógica) e, então, com base nisso, tentamos provar todo um conjunto de teoremas complexos.

No entanto, quão simples podem ser os axiomas? Era isso que eu queria estabelecer em 1999. Como primeiro exemplo, decidi estudar lógica (ou, equivalentemente, álgebra booleana). Refutar todas as minhas expectativas, minha experiência com autômatos celulares, máquinas de Turing e outros sistemas - incluindo até equações diferenciais parciais - sugere que você pode simplesmente começar a listar os casos mais simples possíveis e, em algum momento, ver algo interessante

Mas é possível "abrir a lógica" dessa maneira? Só havia uma maneira de dizer isso. E no final de 1999, organizei tudo para começar a explorar o espaço de todos os sistemas possíveis de axioma, começando pelo mais simples.

Em certo sentido, qualquer sistema de axiomas define um conjunto de restrições, digamos, em p · q. Ela não diz o que p · q é, ela apenas fornece propriedades que p · q deve satisfazer (por exemplo, ela pode dizer que q · p = p · q). Então a questão é se é possível derivar dessas propriedades todos os teoremas da lógica que mantêm quando p · q é Nand [p, q]: nem mais nem menos.

Algo pode ser verificado diretamente. Podemos pegar o sistema de axiomas e ver quais formas p · q satisfazem os axiomas, se p e q são, digamos, verdadeiros e falsos. Se o sistema de axiomas é esse q · p = p · q, então sim, p · q pode ser Nand [p, q] - mas não necessariamente. Também pode ser And [p, q] ou Igual [p, q] ou muitas outras opções que não satisfazem os mesmos níveis que a função NAND na lógica. Mas quando chegamos ao sistema de axiomas {((p · p) · q) · (q · p) = q}, chegamos ao estado em que Nand [p, q] (e o equivalente a Nor [p , q]) permanecem os únicos modelos p · q em funcionamento - pelo menos se assumirmos que q ep têm apenas dois valores possíveis.

É então um sistema de axiomas para a lógica? Não. Porque implica, por exemplo, a existência de uma variante em que p e q têm três valores, mas isso não está na lógica. No entanto, o fato de esse sistema de axiomas de um axioma estar próximo do que precisamos indica que vale a pena procurar um único axioma a partir do qual a lógica é reproduzida. Foi exatamente isso que fiz em janeiro de 2000 (em nosso tempo, essa tarefa foi facilitada graças à função relativamente nova e muito conveniente da Wolfram Language, Groupings).

Foi bastante fácil verificar se os axiomas em que havia 3 ou menos NANDs (ou "operadores de pontos") não funcionavam. Às 5 da manhã de domingo, 29 de janeiro (sim, eu era uma coruja), descobri que axiomas contendo 4 NANDs também não funcionavam. Quando parei de trabalhar por volta das 6 da manhã, eu tinha 14 candidatos em minhas mãos com cinco NANDs. Mas continuando a trabalhar no domingo à noite e realizando testes adicionais, tive que desistir de todos.

Escusado será dizer que o próximo passo foi verificar os axiomas com 6 NAND. Havia 288.684 deles, mas meu código funcionou com eficiência e pouco tempo passou antes que o seguinte aparecesse na tela (sim, da versão 4 do Mathematica):


No começo eu não entendi o que fiz. Eu só sabia que tinha 25 axiomas não equivalentes com 6 NANDs que foram capazes de avançar além dos axiomas com 5 NANDs. Mas havia axiomas entre eles que geravam lógica? Eu tinha um método empírico capaz de descartar axiomas desnecessários. Mas a única maneira de saber com certeza a exatidão de um axioma em particular era provar que era capaz de reproduzir, por exemplo, os axiomas de Schaeffer para a lógica.

Demorou um pouco com os programas, mas depois de alguns dias, descobri que a maioria dos 25 axiomas recebidos não funcionava. Como resultado, dois sobreviveram:



E para minha grande alegria, pude provar o uso de um computador que ambos são axiomas para a lógica. A técnica utilizada garantiu a ausência de axiomas mais simples para a lógica. Portanto, eu sabia que havia atingido a meta: depois de um século (ou talvez alguns milênios) de pesquisas, podemos finalmente dizer que encontramos o axioma mais simples da lógica.

Logo depois, descobri sistemas de dois axiomas com 6 NANDs em geral, que, como provei, são capazes de reproduzir a lógica:



E se dermos como certa a comutatividade p · q = q · p, a lógica pode ser obtida a partir do axioma contendo apenas 4 NAND.

Por que isso é importante

Bem, digamos que é muito legal poder dizer que alguém "concluiu o trabalho iniciado por Aristóteles" (ou pelo menos Boole) e descobriu o sistema mais simples possível de axiomas para a lógica. É apenas um artifício, ou esse fato tem consequências importantes?

Antes da plataforma que desenvolvi em Um novo tipo de ciência, acho que seria difícil considerar esse fato como algo mais do que apenas uma curiosidade. Mas agora deve ficar claro que ele está conectado a todos os tipos de perguntas básicas, como se a matemática deve ser considerada uma descoberta ou uma invenção.

A matemática que as pessoas fazem é baseada em alguns sistemas de axiomas - cada um dos quais define uma área específica da matemática (lógica, teoria dos grupos, geometria, teoria dos conjuntos). Mas falando de maneira abstrata, há um número infinito de sistemas de axiomas - cada um dos quais define um campo da matemática que pode ser estudado, mesmo que as pessoas ainda não o tenham feito.

Antes do livro Um Novo Tipo de Ciência, aparentemente eu quis dizer que tudo o que existe "em algum lugar lá fora" no universo da computação deve ser "menos interessante" do que aquilo que as pessoas criaram e estudaram. Mas minhas descobertas a respeito de programas simples indicam que sistemas que simplesmente "em algum lugar lá fora" não têm possibilidades menos ricas do que aqueles cuidadosamente selecionados pelas pessoas.

E o sistema de axiomas da matemática? Para comparar o existente "em algum lugar lá fora" com o que as pessoas estudaram, você precisa saber se os sistemas de axiomas estão nas áreas existentes de matemática que estudamos. E, com base nos sistemas tradicionais criados pelas pessoas, podemos concluir que eles devem estar em algum lugar muito, muito distante - e, em geral, só podem ser encontrados se você já souber onde está.

Mas minha descoberta do sistema axioma respondeu à pergunta "Qual é a distância da lógica?" Para coisas como um autômato celular, é muito fácil numerar (como eu fiz nos anos 80) todos os autômatos celulares possíveis. É um pouco mais difícil fazer isso com os sistemas axioma - mas não muito. Em uma abordagem, meu axioma pode ser indicado como 411; 3; 7; 118 - ou, na Wolfram Language:


E, pelo menos no espaço de possíveis formas funcionais (sem levar em consideração a marcação de variáveis), há uma representação visual da localização desse axioma:


Dada a importância fundamental da lógica para um número tão grande de sistemas formais que as pessoas estudam, alguém poderia pensar que, em qualquer representação razoável, a lógica corresponde a um dos mais simples sistemas possíveis de axiomas. Mas, pelo menos em uma apresentação usando NAND, não é assim. Para ela, ainda existe um sistema muito simples de axiomas, mas provavelmente será um sistema de cem mil axiomas dentre todos os possíveis que podem ser encontrados se você começar a numerar o sistema de axiomas, começando pelo mais simples.

Diante disso, a próxima pergunta óbvia será: e todos os outros sistemas de axiomas? Como eles se comportam? É essa questão que o livro Um Novo Tipo de Ciência explora. E nele afirmo que coisas como sistemas observados na natureza são mais frequentemente descritas por essas “outras regras” que podemos encontrar numerando as possibilidades.

Quanto aos sistemas de axiomas, fiz uma imagem representando o que está acontecendo nas "áreas da matemática" correspondentes a vários sistemas de axiomas. A série mostra as consequências de um determinado sistema de axiomas, e as caixas indicam a verdade de um certo teorema em um determinado sistema de axiomas (sim, em algum momento o teorema de Gödel entra em vigor, após o qual fica incrivelmente difícil provar ou refutar um dado teorema em um determinado sistema de axiomas; na prática, com pelos meus métodos, isso acontece um pouco à direita do que é mostrado na figura).


Existe algo fundamentalmente especial nas áreas de matemática que são “pesquisadas por pessoas”? A julgar por essa e outras fotos, nada de óbvio vem à mente. Suspeito que exista apenas uma característica nessas áreas - o fato histórico de que foram estudadas. (Você pode fazer declarações como "elas descrevem o mundo real" ou "relacionadas a como o cérebro funciona", mas os resultados descritos no livro sugerem o contrário).

Bem, qual é o significado do meu sistema de axiomas para a lógica? Seu tamanho faz com que você sinta o conteúdo final da informação da lógica como um sistema axiomático. E isso nos faz acreditar - pelo menos por enquanto - que precisamos considerar a lógica mais como uma "construção inventada pelo homem" do que como uma "descoberta" que aconteceu por "razões naturais".

Se a história fosse diferente, e procuraríamos constantemente (como é feito no livro) muitos possíveis sistemas mais simples de axiomas, provavelmente provavelmente "abriríamos" o sistema de axiomas para a lógica, como aquele sistema cujas propriedades nos parecem interessantes. Mas, como estudamos um número tão pequeno de todos os sistemas possíveis de axiomas, acho que seria razoável considerar a lógica como uma "invenção" - uma construção especialmente criada.

Em certo sentido, na Idade Média, a lógica era assim - quando possíveis silogismos (tipos aceitáveis ​​de argumentos) eram representados na forma de mnemônicos latinos como bArbArA e cElErAnt. Portanto, agora é interessante encontrar uma representação mnemônica do que sabemos agora como o sistema mais simples de axiomas para a lógica.

Começando com ((p · q) · r) · (p · ((p · r) · p)) = r, cada p · q pode ser representado como um prefixo ou uma entrada polonesa (inversa à “entrada polonesa reversa” da calculadora HP ) na forma de Dpq - portanto, todo o axioma pode ser escrito como = DDDpqrDpDDprpr. Há também um mnemônico em inglês sobre esse assunto - FIGURA OUT Queue, onde os papéis p, q, r são desempenhados por u, r, e. Ou você pode observar as primeiras letras das palavras na frase a seguir (onde B é um operador ep, q, r são a, p, c): “Pouco a pouco, um programa calculou o melhor axioma binário da álgebra booleana, cobrindo todos os casos” [ o melhor axioma binário da álgebra booleana calculado por meio de um programa descreve gradualmente todos os casos].

Mecânica de Prova

Ok, então como você prova a correção do meu sistema de axiomas? A primeira coisa que vem à mente é mostrar que é possível deduzir um sistema conhecido de axiomas para a lógica - por exemplo, o sistema de axiomas Schaeffer:


Existem três axiomas aqui, e precisamos derivar cada um. Aqui está o que você pode fazer para produzir o primeiro, usando a versão mais recente do Wolfram Language:


Vale ressaltar que agora se tornou possível fazer isso. No "objeto de evidência" está escrito que 54 etapas foram usadas para a prova. Com base nesse objeto, podemos gerar um "caderno" que descreve cada uma das etapas:


Em geral, toda a sequência de lemas intermediários é comprovada aqui, o que nos permite deduzir o resultado final. Entre os lemas, existe toda uma rede de dependências mútuas:


Mas as redes envolvidas na derivação de todos os três axiomas no sistema de axiomas de Scheffer - para o último, 504 etapas incríveis são usadas:


Sim, é óbvio que essas redes são bastante confusas. Mas antes de discutir o que essa complexidade significa, vamos falar sobre o que acontece em cada etapa dessa evidência.

A ideia principal é simples. Imagine que temos um axioma que é simplesmente escrito como p · q = q · p (matematicamente, isso significa que o operador é comutativo). Mais precisamente, o axioma diz que, para qualquer expressão p e q, p · q é equivalente a q · p.

Bem, digamos que queremos deduzir desse axioma que (a) b (c) d = = (d) c) · (b · a). Isso pode ser feito usando o axioma para converter d · c para c · d, b · a para a · b e, finalmente, (c · d) · (a · b) para (a · b) · (c · d )

FindEquationalProof faz essencialmente a mesma coisa, embora não siga essas etapas exatamente na mesma ordem e mude o lado esquerdo da equação e o direito.


Depois de receber essa prova, você pode simplesmente rastrear cada etapa e verificar se eles fornecem o resultado indicado. Mas como encontrar evidências? Existem muitas sequências possíveis de permutações e transformações. Como encontrar uma sequência que traga com sucesso o resultado final?

Pode-se decidir: por que não tentar todas as seqüências possíveis e, se houver uma sequência de trabalho entre elas, ela deve ser encontrada?O problema é que você pode chegar rapidamente a um número astronômico de seqüências. A maior parte da arte de provar automaticamente os teoremas consiste em encontrar maneiras de reduzir o número de sequências a serem verificadas.

Isso rapidamente entra em detalhes técnicos, mas a idéia básica é fácil de discutir se você conhece o básico da álgebra. Suponha que estamos tentando provar um resultado algébrico como


Há uma maneira garantida de fazer isso: simplesmente aplicando as regras da álgebra para revelar cada lado, você pode ver imediatamente sua similaridade:


Por que isso funciona?Como existe uma maneira de trabalhar com essas expressões, reduza-as sistematicamente até que elas tomem um formulário padrão. É possível fazer a mesma operação em sistemas arbitrários de axiomas?

Não imediatamente. Na álgebra, isso funciona porque possui uma propriedade especial que garante que você sempre possa "mover-se" pelo caminho de simplificar expressões. Mas na década de 1970, diferentes cientistas descobriram várias vezes de forma independente (sob nomes como o algoritmo de Knuth-Bendix ou a base de Gröbner ) que, mesmo que o sistema do axioma não possua a propriedade interna necessária, é possível descobrir “adições” a esse sistema no qual ele existe

É o que acontece nas evidências típicas fornecidas pelo FindEquationalProof (com base no sistema de Valdmeister, "mestre das árvores"). Existem os chamados “Lemas críticos de pares”, que não avançam diretamente a prova, mas possibilitam o surgimento de caminhos capazes disso. Tudo é complicado devido ao fato de que, embora a expressão final que queremos obter seja bastante curta, no caminho para isso, talvez você precise passar por expressões intermediárias muito mais longas. Portanto, por exemplo, a prova do primeiro axioma de Schaeffer possui etapas intermediárias:


Nesse caso, a maior das etapas é 4 vezes maior que o axioma original:


Tais expressões podem ser representadas como uma árvore. Aqui está sua árvore, comparada com a árvore do axioma original:


E é assim que os tamanhos das etapas intermediárias se desenvolvem no decorrer das provas de cada um dos axiomas de Schaeffer:

Por que isso é tão difícil?

É de admirar que essa evidência seja tão complexa? Na verdade não. Afinal, estamos bem cientes de que a matemática pode ser complexa. Em princípio, poderia ser fácil provar todas as verdades da matemática. Mas um dos efeitos colaterais do teorema de Gödel de 1931 é que, mesmo as coisas que têm evidências, o caminho para elas pode ser arbitrariamente longo.

Este é um sintoma de um fenômeno muito mais geral, que chamo de irredutibilidade computacional . Considere um sistema controlado por uma regra simples de autômato celular (é claro que em qualquer um dos meus ensaios sempre haverá autômatos celulares). Execute este sistema.


Pode-se decidir que, se o sistema for baseado em uma regra simples, deve haver uma maneira rápida de entender o que o sistema faz. Mas isso não é verdade.De acordo com meu princípio de equivalência computacional , a operação de um sistema geralmente corresponde a cálculos, cuja complexidade coincide com quaisquer cálculos que poderíamos fazer para entender o comportamento do sistema. Isso significa que o comportamento real do sistema, de fato, corresponde a uma quantidade de trabalho computacional que, em princípio, não pode ser reduzido.

Em relação à figura acima: digamos que queremos descobrir se o padrão morre no final. Poderíamos continuar a cumpri-lo e, se tivermos sorte, acabará por degenerar em algo, cujo destino será óbvio. No entanto, em geral, não há limite superior em quanto tempo temos para gastar, de fato, na prova.

Quando algo assim acontece com evidências lógicas, acontece um pouco diferente. Em vez de iniciar algo que funcione de acordo com certas regras, perguntamos se existe uma maneira de obter um determinado resultado, executando várias etapas, cada uma das quais obedecendo a uma determinada regra. E essa tarefa, como uma tarefa computacional prática, é muito mais complicada. Mas a essência da complexidade é o mesmo fenômeno de irredutibilidade computacional, e esse fenômeno sugere que não há uma maneira geral de contornar brevemente o processo de estudar o que o sistema fará.

Desnecessário dizer que existem muitas coisas no mundo - especialmente em tecnologia e modelagem científica, bem como em áreas onde existem várias formas de regras - tradicionalmente projetadas para evitar irredutibilidade computacional e trabalhar para que o resultado de seu trabalho seja imediatamente visível, sem a necessidade de realizar uma quantidade irredutível de cálculos.

Mas uma das consequências do meu princípio de equivalência computacional é que esses casos são singulares e não naturais - ele argumenta que a irredutibilidade computacional existe em todos os sistemas do universo computacional.

E a matemática? Talvez as regras da matemática tenham sido especificamente escolhidas para demonstrar redutibilidade computacional. E, em alguns casos, é esse o caso (e, em certo sentido, isso também acontece na lógica). Mas, na maioria das vezes, parece que os sistemas de axiomas da matemática não são atípicos para o espaço de todos os sistemas possíveis de axiomas - onde a irredutibilidade computacional é inevitável.

Por que precisamos de evidências?

Em certo sentido, é necessária prova para conhecer a verdade de alguma coisa. Obviamente, especialmente em nosso tempo, as evidências desapareceram em segundo plano, dando lugar à computação pura. Na prática, o desejo de gerar algo através de cálculos é muito mais comum do que o desejo de "recuar" e construir uma prova da verdade de algo.

Na matemática pura, no entanto, muitas vezes é preciso lidar com conceitos que incluem, pelo menos nominalmente, um número infinito de casos ("verdadeiro para todos os primos" etc.) para os quais os cálculos da testa não funcionam. . E quando surgir a pergunta da confirmação (“esse programa pode terminar com um erro?” Ou “posso gastar essa criptomoeda duas vezes?”) É mais razoável tentar provar isso do que calcular todos os casos possíveis.

Mas na prática matemática real, a prova é mais do que estabelecer a verdade. Quando Euclides escreveu seus " Começos ", ele simplesmente indicou os resultados e "os deixou para o leitor". Mas, de uma maneira ou de outra, especialmente ao longo do século passado, as evidências se transformaram em algo que não acontece apenas nos bastidores, mas é o principal meio pelo qual é necessário transmitir conceitos.

Parece-me que, como resultado de alguma peculiaridade da história, as evidências são oferecidas hoje como um objeto que as pessoas devem entender, e os programas são considerados apenas algo que um computador deve executar. Por que isso aconteceu? Bem, pelo menos no passado, as evidências poderiam ser apresentadas em forma de texto - portanto, se alguém a usasse, apenas as pessoas. E os programas eram quase sempre gravados na forma de uma linguagem de computador. E por muito tempo, esses idiomas foram criados para que pudessem se traduzir mais ou menos diretamente em operações de computador de baixo nível - ou seja, o computador as entendeu imediatamente, mas as pessoas não precisam.

Mas um dos principais objetivos do meu trabalho nas últimas décadas foi mudar esse estado de coisas e desenvolver na Wolfram Language uma verdadeira "linguagem de comunicação computacional" na qual as idéias computacionais possam ser transmitidas para que possam ser entendidas por computadores e pessoas.

Essa linguagem tem muitas consequências. Um deles está mudando o papel da evidência. Suponha que analisemos algum resultado matemático. No passado, a única maneira plausível de trazê-lo à compreensão era evidenciar que as pessoas liam. Mas agora outra coisa é possível: você pode fornecer um programa para a Wolfram Language que calcule o resultado. E esta é, de muitas maneiras, uma maneira muito mais rica de transmitir a verdade do resultado. Cada parte do programa é algo preciso e inequívoco - todos podem iniciá-lo. Não existe um problema como as tentativas de entender alguma parte do texto, exigindo o preenchimento de algumas lacunas. Tudo está indicado no texto claramente.

E as evidências? Existem maneiras claras e precisas de escrever evidências? Potencialmente sim, embora isso não seja particularmente fácil. E embora a fundação da Wolfram Language já exista há 30 anos, apenas hoje uma maneira razoável parece apresentar evidências estruturalmente diretas, como um dos meus axiomas acima.

Você pode imaginar a criação de evidências no Wolfram Language da mesma maneira que as pessoas criam programas - e estamos trabalhando para fornecer versões de alto nível dessa funcionalidade que “ajudem na evidência”. No entanto, ninguém criou a prova do meu sistema de axioma - foi encontrado por um computador. E isso é mais parecido com a saída do programa do que com o próprio programa. No entanto, como um programa, em certo sentido, a prova também pode ser "executada" para verificar o resultado.

Criando clareza

Na maioria das vezes, as pessoas que usam a Wolfram Language, ou Wolfram | Alpha, querem contar alguma coisa. Eles precisam obter o resultado, sem entender por que obtiveram exatamente esses resultados. Porém, no Wolfram | Alpha, especialmente em áreas como matemática e química, um recurso popular entre os estudantes é a construção de soluções "passo a passo".


Quando o sistema Wolfram | Alpha calcula, por exemplo, uma integral, ele usa todos os tipos de técnicas algorítmicas poderosas que são otimizadas para receber respostas. Mas quando lhe pedem para mostrar as etapas dos cálculos, ela faz outra coisa: ela precisa explicar em etapas por que esse é o resultado obtido.

Não haveria benefício em explicar como o resultado foi realmente obtido; Este é um processo muito inadequado para humanos. Ela precisa entender quais operações aprendidas pelas pessoas podem ser usadas para obter um resultado. Muitas vezes, ela inventa algum truque útil. Sim, ela tem uma maneira sistemática de fazer isso, o que sempre funciona. Mas há muitos estágios "mecânicos" nele. Um “truque” (substituição, integração parcial, etc.) não funcionará no caso geral, mas nesse caso particular, dará um caminho mais rápido para a resposta.

Que tal obter versões claras de outras coisas? Por exemplo, o trabalho de programas no caso geral. Ou evidência do meu sistema de axioma.

Vamos começar com os programas. Suponhamos que escrevemos um programa e desejemos explicar como ele funciona. Uma das abordagens tradicionais é incluir comentários no código. Se escrevermos em um idioma tradicional de baixo nível, talvez seja a melhor saída. Mas toda a essência da Wolfram Language como linguagem de comunicação computacional é que a própria linguagem deve permitir a transmissão de idéias, sem a necessidade de incluir partes adicionais de texto.

Esforços devem ser feitos para tornar o programa Wolfram Language uma boa descrição do processo, bem como para tornar o texto em inglês simples uma boa descrição do processo. No entanto, você pode obter um pedaço do código da Wolfram Language que explica muito claramente como tudo funciona por conta própria.

Obviamente, muitas vezes acontece que a execução real do código leva a coisas que não seguem obviamente do programa. Mencionarei em breve casos extremos como autômatos celulares. Mas, por enquanto, vamos imaginar que criamos um programa pelo qual podemos imaginar o que geralmente faz.

Nesse caso, descobri que os ensaios de computação apresentados como Wolfram Notebooks são uma ótima ferramenta para explicar o que está acontecendo. É importante que o Wolfram Language, isso permita executar até as menores partes dos programas separadamente (com as expressões simbólicas correspondentes como dados de entrada e saída). Depois disso, você pode imaginar a sequência de etapas do programa como uma sequência de elementos do diálogo que formam a base do notebook de computação.

Na prática, muitas vezes é necessário criar visualizações dos dados de entrada e saída. Sim, tudo pode ser expresso como uma representação simbólica inequívoca. Mas é muito mais fácil para as pessoas entenderem a representação visual das coisas do que qualquer linha unidimensional semelhante a uma linguagem.

Obviamente, criar boas visualizações é semelhante à arte. Mas na Wolfram Language, fizemos muito trabalho para automatizar essa arte - geralmente com a ajuda de aprendizado de máquina bastante sofisticado e outros algoritmos que executam coisas como layout de redes ou elementos gráficos.

Que tal começar com um simples rastreamento de programa? Isso é difícil de fazer. Venho experimentando isso há décadas e nunca fiquei completamente satisfeito com os resultados. Sim, você pode ampliar e ver muitos detalhes do que está acontecendo. Mas não encontrei boas técnicas suficientes para entender toda a imagem e automaticamente forneço algumas coisas particularmente úteis.

Em algum nível, essa tarefa é semelhante à engenharia reversa. Você verá um código de máquina, um circuito de chip, o que seja. E você precisa dar um passo atrás e recriar a descrição de alto nível da qual a pessoa repeliu, que de alguma forma “compilou” o que você vê.

Na abordagem tradicional de engenharia, quando as pessoas criam um produto em etapas, sempre com a capacidade de antecipar as conseqüências do que elas criam, essa abordagem pode funcionar em princípio. Mas se você apenas vagar pelo universo da computação em busca de um programa ideal (como eu estava procurando por possíveis sistemas de axioma para encontrar um sistema de lógica), então não há garantia de que haverá “história humana” ou explicação por trás desse programa.

Um problema semelhante é encontrado nas ciências naturais. Você vê como um conjunto complexo de todos os tipos de processos se desenvolve em um sistema biológico. É possível submetê-los a "engenharia reversa" para encontrar uma "explicação"? Às vezes, pode-se dizer que a evolução com a seleção natural levará a isso. Ou que ele é freqüentemente encontrado no universo da computação, então a probabilidade de sua ocorrência é alta. Mas não há garantia de que o mundo natural seja necessariamente projetado para que as pessoas possam explicá-lo.

Naturalmente, ao modelar as coisas, inevitavelmente consideramos apenas os aspectos que nos interessam e idealizamos tudo o mais. E, especialmente em áreas como medicina, você geralmente precisa trabalhar com um modelo aproximado com uma árvore de decisão superficial, o que é fácil de explicar.

A natureza da explicabilidade

O que significa a frase "algo pode ser explicado"? Em essência, isso significa que as pessoas podem entender.

O que é exigido das pessoas para entender alguma coisa? Precisamos de alguma forma perceber isso. Pegue um autômato celular típico com comportamento complexo. O computador não apresenta problemas para executar todas as etapas de sua evolução. Com tremendo esforço e trabalho, uma pessoa pode reproduzir o trabalho de um computador.

Mas não se pode dizer que, nesse caso, uma pessoa "entenda" o que um autômato celular faz. Para isso, uma pessoa teria que falar facilmente sobre o comportamento de um autômato celular em alto nível. Ou, em outras palavras, uma pessoa deve ser capaz de “contar uma história” sobre o comportamento de um autômato que outras pessoas possam entender.

Existe uma maneira universal de fazer isso? Não, devido à irredutibilidade computacional. No entanto, pode acontecer que certos recursos importantes para as pessoas possam ser explicados em um alto nível com certas limitações.

Como isso funciona? Para fazer isso, você precisa criar uma certa linguagem de alto nível que possa descrever os recursos que nos interessam. Estudando um desenho típico do autômato celular, pode-se tentar falar não em termos de cores de um grande número de células individuais, mas em termos de estruturas de nível superior que podem ser detectadas. O principal é que você pode compilar pelo menos um catálogo parcial dessas estruturas: embora existam muitos detalhes que não se encaixam na classificação, certas estruturas são comuns.

E se queremos começar a "explicar" o comportamento de um autômato celular, começaremos nomeando as estruturas e depois falaremos sobre o que está acontecendo do ponto de vista dessas estruturas.


O caso do autômato celular tem uma característica simplificadora: como opera com base em regras determinísticas simples, possui estruturas igualmente repetidas. Na natureza, por exemplo, geralmente não encontramos uma repetição tão idêntica. Há apenas um, por exemplo, um tigre, muito parecido com o outro, portanto os chamamos de "tigres", embora o arranjo de seus átomos não seja idêntico.

Qual é o significado geral de tudo isso? Consiste em usar a idéia de representação simbólica. Dizemos que podemos atribuir um certo símbolo - geralmente essa palavra - que pode ser usado para descrever simbolicamente toda uma classe de coisas, sem ter que listar em detalhes todos os detalhes de todos os componentes dessas coisas.

Isso é semelhante à compactação de informações: usamos construções simbólicas para encontrar uma maneira mais curta de descrever coisas que nos interessam.

Suponha que geramos uma estrutura gigantesca, por exemplo, matemática:


O primeiro passo é criar algum tipo de representação interna de alto nível. Por exemplo, podemos detectar estruturas reutilizáveis. E podemos dar nomes a eles. E então mostre o "esqueleto" de toda a estrutura com a ajuda deles:


Sim, esse esquema, semelhante à “compressão de dicionário”, é útil para atingir o primeiro nível de explicabilidade.

Mas vamos voltar à prova do meu sistema de axioma. Os lemas criados nesta prova são especialmente selecionados como elementos reutilizáveis. No entanto, excluindo-os, ainda temos evidências de que as pessoas não conseguem entender imediatamente.

O que mais você pode fazer? Precisamos apresentar algum tipo de descrição de um nível ainda mais alto. O que poderia ser?

Conceito de conceitos

Se você está tentando explicar algo para alguém, será muito mais fácil fazer isso se você encontrar algo mais, mas semelhante ao que uma pessoa já pode entender. Imagine como você explicará o conceito de um drone moderno para uma pessoa da Idade da Pedra. Vai ser difícil de fazer. Mas será muito mais fácil explicar isso para uma pessoa que viveu há 50 anos e já viu helicópteros e modelos de aviões.

E, no final, a conclusão é que, quando explicamos algo, fazemos isso em uma linguagem conhecida por nós e por quem o explicamos. E quanto mais rica a linguagem, menos novos elementos temos que apresentar para transmitir o que estamos tentando explicar.

Existe um padrão que se repete ao longo da história da mente. Um certo conjunto de coisas é observado muitas vezes. Gradualmente, eles começam a entender que essas coisas são de algum modo abstratamente semelhantes, e todas elas podem ser descritas em termos de um novo conceito, descrito em alguma nova palavra ou frase.

Suponha que notemos coisas como água, sangue e óleo. Em algum momento, entendemos que existe um conceito generalizado de "líquido", e todos eles podem ser descritos como líquidos. E quando temos esse conceito, podemos começar a raciocinar em seus termos, encontrando mais conceitos - digamos, viscosidade, com base nela.

Quando faz sentido combinar as coisas em um conceito? Uma pergunta difícil que não pode ser respondida sem prever tudo o que pode ser feito com esse conceito. Na prática, no processo de evolução da linguagem e das idéias de uma pessoa, é observado um certo processo de aproximação sucessiva.

No sistema moderno de aprendizado de máquina, ocorre uma soma muito mais rápida de informações. Imagine que pegamos todos os tipos de objetos em todo o mundo e alimentamos as funções FeatureSpacePlot para ver o que acontece. Se obtivermos certos clusters no espaço de recursos, podemos concluir que cada um deles pode ser definido como correspondendo a um certo "conceito", que, por exemplo, pode ser marcado com uma palavra.

Honestamente, o que acontece com o FeatureSpacePlot - como no processo de desenvolvimento intelectual humano - é, em certo sentido, um processo passo a passo. Para distribuir objetos por espaço de recurso, o FeatureSpacePlot usa os recursos que aprendeu a extrair das tentativas anteriores de categorizar.

Bem, se aceitarmos o mundo como ele é, quais são as melhores categorias - ou conceitos - que podem ser usadas para descrever as coisas? Esta questão está em constante evolução. Em geral, todos os avanços - seja ciência, tecnologia ou qualquer outra coisa - costumam estar associados com precisão à realização da possibilidade de identificar uma nova categoria ou conceito de uma maneira útil.

Mas no processo de evolução de nossa civilização há uma certa espiral. Primeiramente, um certo conceito definido é definido - digamos, a idéia de um programa. Depois disso, as pessoas começam a usá-lo e refletem em seus termos. Logo, muitos conceitos diferentes são construídos com base nesse conceito. E então outro nível de abstração é determinado, novos conceitos baseados no anterior são criados.

A história é característica do conjunto tecnológico de conhecimento da civilização moderna e de seu conjunto intelectual de conhecimentos. Lá e há torres de conceitos e níveis de abstração indo um após o outro.

Problema de aprendizagem

Para que as pessoas possam se comunicar usando um certo conceito, precisam saber sobre isso. E, sim, alguns conceitos (como a constância de objetos) são automaticamente reconhecidos pelas pessoas simplesmente pela observação da natureza. Mas suponha que, se você olhar para a lista de palavras comuns do inglês moderno, ficará claro que a maioria dos conceitos usados ​​por nossa civilização moderna não se aplica àqueles que as pessoas conhecem, observando a natureza.

Em vez disso - o que é muito remanescente do aprendizado de máquina moderno - eles precisam de um conhecimento especial do mundo "sob supervisão", organizado para enfatizar a importância de certos conceitos. E em áreas mais abstratas (como a matemática), eles provavelmente precisam se deparar com conceitos em sua forma abstrata imediata.

Bem, mas precisaremos aprender mais e mais o tempo todo com o aumento da quantidade de conhecimento intelectual acumulado da civilização? Pode haver preocupação de que, em algum momento, nosso cérebro simplesmente não consiga acompanhar o desenvolvimento, e teremos que adicionar alguma ajuda adicional. Mas parece-me que, felizmente, esse é um daqueles casos em que o problema pode ser resolvido "no nível do software".

O problema é o seguinte: a qualquer momento da história, existe um certo conjunto de conceitos que é importante para a vida no mundo nesse período. E, sim, com o desenvolvimento da civilização, novos conceitos são revelados e novos conceitos são introduzidos.No entanto, existe outro processo: novos conceitos introduzem novos níveis de abstração, geralmente incluindo um grande número de conceitos anteriores.

Muitas vezes podemos observar isso em tecnologia. Houve um tempo em que você precisava conhecer muitos detalhes de baixo nível para trabalhar em um computador. Mas com o tempo, esses detalhes abstraíram, então agora você só precisa de um conceito geral. Você clica no ícone e o processo é iniciado - você não precisa entender os meandros da operação dos sistemas operacionais, manipuladores de interrupções, agendadores e todos os outros detalhes.

E, claro, a Wolfram Language fornece um ótimo exemplo disso. Ele se esforça muito para automatizar muitos detalhes de baixo nível (por exemplo, qual dos algoritmos deve ser usado) e permite que os usuários pensem em conceitos de alto nível.

Sim, ainda são necessárias pessoas que entendam os detalhes subjacentes às abstrações (embora eu não tenha certeza de quantos cortadores de pedras a sociedade moderna exige). Mas, na maioria das vezes, a educação pode se concentrar em um alto nível de conhecimento.

Supõe-se frequentemente que, para alcançar conceitos de alto nível no processo de aprendizagem, uma pessoa deve primeiro resumir de alguma forma a história de como esses conceitos vieram a ser historicamente. Mas geralmente - e, talvez, sempre - parece não ser assim. Você pode dar um exemplo extremo: imagine que, para aprender a usar um computador, você deve primeiro passar por toda a história da lógica matemática. No entanto, sabe-se realmente que as pessoas recorrem imediatamente aos conceitos modernos de computação, sem a necessidade de estudar algum tipo de história.

Mas como é a clareza da rede de conceitos? Existem conceitos que só podem ser entendidos através da compreensão de outros conceitos? Dado o treinamento das pessoas com base na interação com o ambiente (ou no treinamento de uma rede neural), sua ordem provavelmente pode existir.

Mas parece-me que um certo princípio, semelhante à universalidade da computação, sugere que, com um "cérebro puro" na mão, você pode começar de qualquer lugar. Portanto, se alguns alienígenas aprendessem sobre a teoria das categorias e quase nada mais, eles, sem dúvida, construiriam uma rede de conceitos onde essa teoria está na raiz, e o que conhecemos como o básico da aritmética seria estudado a partir deles. algures no análogo do nosso instituto.

É claro que esses alienígenas poderiam construir seu conjunto de tecnologias e seu ambiente de uma maneira muito diferente da nossa - assim como nossa história poderia se tornar completamente diferente se os computadores pudessem ser desenvolvidos com sucesso no século XIX, e não em meados do século XX.

Progresso da matemática

Eu sempre refleti sobre até que ponto a trajetória histórica da matemática está sujeita ao papel do acaso e em que medida era inevitável. Como já mencionei, no nível dos sistemas formais, existem muitos sistemas possíveis de axiomas nos quais você pode construir algo que se assemelha formalmente à matemática.

Mas a história real da matemática não começou com um sistema arbitrário de axiomas. Começou no tempo dos babilônios com tentativas de usar a aritmética para o comércio e a geometria para fins de desenvolvimento da terra. E a partir dessas raízes práticas, níveis subsequentes de abstração começaram a ser adicionados, o que acabou levando à matemática moderna - por exemplo, os números foram gradualmente generalizados de números inteiros positivos para racionais, depois para raízes, depois para todos os números inteiros, para frações decimais, para números complexos e algébricos. números, para quaternions e assim por diante.

Existe uma inevitabilidade desse caminho de desenvolvimento de abstrações? Suspeito, até certo ponto, que sim. Talvez seja esse o caso de outros tipos de formação de conceitos. Tendo atingido um certo nível, você tem a oportunidade de estudar várias coisas e, com o tempo, grupos dessas coisas se tornam exemplos de construções mais gerais e abstratas - que, por sua vez, determinam um novo nível, do qual se pode aprender algo novo.

Existem maneiras de sair desse ciclo? Uma possibilidade pode estar relacionada a experimentos matemáticos. Pode-se provar sistematicamente coisas relacionadas a certos sistemas matemáticos. Mas podemos apenas empiricamente notar fatos matemáticos - como Ramanujan uma vez notei que $$$e^{\pi \sqrt{163}}$



Da mesma maneira que se pode numerar sistemas de axiomas, pode-se imaginar a numeração de possíveis questões em matemática. Mas isso imediatamente levanta um problema. O teorema de Gödel afirma que em sistemas de axiomas como o relacionado à aritmética, existem teoremas "formalmente insolúveis" que não podem ser provados ou refutados na estrutura desse sistema de axiomas.

No entanto, os exemplos específicos criados por Gödel pareciam muito distantes do que realmente poderia surgir nas aulas de matemática. E, durante muito tempo, acreditava-se que, de alguma forma, o fenômeno da insolubilidade era algo que, em princípio, existe, mas não estará relacionado à "matemática real".

No entanto, de acordo com meu princípio de equivalência computacional e minha experiência no universo computacional, tenho certeza de que não é assim - e que, de fato, a insolubilidade está muito próxima, mesmo na matemática típica. Eu não ficaria surpreso se uma parte tangível dos problemas de matemática não resolvidos para hoje (a hipótese de Riemann , P = NP, etc.) for insolúvel.

Mas se há muita insolubilidade por aí, como é que tantas coisas na matemática são resolvidas com sucesso? Eu acho que isso ocorre porque os problemas resolvidos com sucesso foram escolhidos especialmente para evitar insolabilidade, simplesmente por causa de como o desenvolvimento da matemática é construído. Porque, se, de fato, formamos níveis sucessivos de abstração com base em conceitos que provamos, então estamos pavimentando o caminho que pode seguir em frente sem se transformar em insolubilidade.

É claro que a matemática experimental ou "perguntas aleatórias" podem nos levar imediatamente a uma área cheia de insolubilidade. Mas, pelo menos por enquanto, a disciplina básica da matemática não se desenvolveu dessa maneira.

E o que dizer desses "fatos aleatórios da matemática"? Sim, o mesmo que em outras áreas da pesquisa intelectual. Os “fatos aleatórios” não são incluídos no caminho do desenvolvimento intelectual até que alguma estrutura - geralmente alguns conceitos abstratos - seja construída em torno deles.

Um bom exemplo é minha descoberta favorita da origem da complexidade em tais sistemas, geralmente 30 autômatos celulares. Sim, fenômenos semelhantes já foram observados milhares de anos atrás (por exemplo, aleatoriedade em uma sequência de números primos). Mas sem uma plataforma conceitual mais ampla, poucas pessoas prestaram atenção a elas.

Outro exemplo são sequências aninhadas (fractais). Existem alguns exemplos de como eles se conheceram no mosaico do século XIII, mas ninguém prestou atenção a eles até nos anos 80, toda uma plataforma surgiu em torno dos fractais.

A mesma história se repete várias vezes: até que conceitos abstratos sejam definidos, é difícil falar sobre novos conceitos, mesmo quando confrontados com um fenômeno que os demonstra.

Suspeito que esse seja o caso da matemática: existe uma certa camada inevitável de alguns conceitos abstratos em cima de outros, que determina o caminho da matemática. É assim único? Sem dúvida não. No vasto espaço de possíveis fatos matemáticos, existem certas direções que são selecionadas para outras construções. Mas você pode escolher outros.

Isso significa que os tópicos em matemática são inevitavelmente dirigidos por acidentes históricos? Não tanto quanto você imagina. De fato, como a matemática foi descoberta repetidamente, começando com coisas como álgebra e geometria, há uma tendência notável em que diferentes direções e diferentes abordagens levam a resultados equivalentes ou correspondentes.

Talvez, até certo ponto, isso seja uma consequência do princípio da equivalência computacional e do fenômeno da universalidade computacional: embora as regras básicas (ou "linguagem") usadas em diferentes áreas da matemática sejam diferentes, no final, há uma maneira de traduzir entre elas - e no próximo nível de abstração o caminho escolhido não será mais tão crítico.

Prova lógica e automação de abstração

Voltar para as provas lógicas. Como eles estão relacionados à matemática típica? Até agora, de jeito nenhum. Sim, a prova tem nominalmente a mesma forma que a prova matemática padrão. Mas não é "amigável para pessoas de matemática". Estas são apenas peças mecânicas. Não está associado a conceitos abstratos de alto nível que serão compreensíveis para a matemática humana.

Ajudaria muito se descobríssemos que lemas de prova não triviais já apareciam na literatura matemática (acho que não, mas nossas possibilidades de pesquisa por teoremas ainda não atingiram um nível que possamos ter certeza). Mas se eles aparecerem, provavelmente nos dará uma maneira de conectar esses lemas com outras coisas da matemática e definir seu círculo de conceitos abstratos.

Mas como as evidências podem ser explicadas sem isso?

Talvez exista alguma outra maneira de realizar a prova, fundamentalmente mais fortemente relacionada à matemática existente. Mas mesmo com a evidência que temos agora, pode-se imaginar “aprimorando” novos conceitos que definiriam um nível mais alto de abstração e colocariam essa prova em um contexto mais geral.

Não tenho certeza de como fazer isso. Eu estava pensando em nomear um prêmio (algo como meu Prêmio Turing de 2007) para "transformar evidências em uma forma compreensível". No entanto, é completamente incompreensível como se pode avaliar a “explicabilidade”. Pode-se pedir para gravar um vídeo de uma hora no qual uma explicação bem-sucedida da prova seria dada, adequada para um matemático típico - mas isso seria muito subjetivo.

Mas, da mesma maneira que é possível automatizar a busca de belos layouts de redes, talvez possamos automatizar o processo de transformar evidências em explicáveis. A prova atual, de fato, sem explicação, sugere considerar várias centenas de lemas. Mas suponha que possamos definir um pequeno número de lemas "interessantes". Talvez pudéssemos, de alguma forma, adicioná-los ao nosso cânon da famosa matemática, e então poderíamos usá-los para entender a prova.

Existe uma analogia com o desenvolvimento de linguagens. Ao criar a Wolfram Language, tento identificar as “peças de trabalho computacional” que as pessoas geralmente precisam. Criamos funções incorporadas ao idioma a partir deles, com nomes específicos que as pessoas podem usar para se referir a eles.

Um processo semelhante está em andamento - embora nem tão organizado - na evolução das línguas naturais. “Pedaços de significado” que acabam sendo úteis acabam recebendo suas palavras no idioma. Às vezes, eles começam com frases que consistem em várias palavras existentes. Mas as mais influentes geralmente acabam tão longe das palavras existentes que aparecem na forma de novas palavras, que são potencialmente difíceis de definir.

No desenvolvimento da Wolfram Language, cujas funções são chamadas usando palavras em inglês, confio no entendimento geral de uma pessoa do idioma inglês (e às vezes no entendimento de palavras usadas em aplicativos comuns de computador).

Seria preciso fazer algo semelhante para determinar quais lemas adicionar ao cânon matemático. Seria necessário não apenas garantir que cada lema seria de alguma forma “essencialmente interessante”, mas também selecionar lemas que fossem “fáceis de deduzir” dos conceitos e resultados matemáticos existentes.

Mas o que torna o lema "essencialmente interessante"? Deve-se dizer que, antes de trabalhar em meu livro, culpei a escolha de lemas (ou torres) em qualquer área da matemática descrita e nomeada em livros didáticos, grande arbitrariedade e acidentes históricos.

Mas, tendo analisado os teoremas da lógica básica em detalhes, fiquei surpreso ao encontrar algo completamente diferente. Suponha que tenhamos construído todos os teoremas corretos da lógica na ordem de seu tamanho
(por exemplo, p = p será o primeiro, p AND p = p - um pouco mais tarde, etc.). Esta lista tem muita redundância. A maioria dos teoremas acaba sendo uma extensão trivial dos teoremas que já apareceram na lista.

Mas, às vezes, aparece um teorema que produz novas informações que não podem ser provadas com base nos teoremas que já apareceram na lista. Um fato notável: existem 14 desses teoremas , e eles, em essência, correspondem exatamente aos teoremas que geralmente recebem nomes nos livros didáticos sobre lógica (aqui AND é ∧, OR é ∨, e NOT é ¬.)


Em outras palavras, nesse caso, os teoremas nomeados ou "interessantes" são precisamente aqueles que fazem afirmações sobre novas informações de tamanho mínimo. Sim, de acordo com essa definição, após algum tempo, novas informações não existirão mais, pois obteremos todos os axiomas necessários para provar tudo o que é possível - embora você possa ir além, começando a limitar a complexidade das evidências admissíveis.

E os teoremas da NAND, por exemplo, os encontrados na prova? Novamente, você pode construir todos os teoremas verdadeiros em ordem e descobrir quais não podem ser provados com base nos teoremas anteriores da lista:


NAND não tem uma tradição histórica como AND, OR e NOT. E, aparentemente, não há linguagem humana na qual NAND seja denotado por uma palavra. Mas na lista de teoremas da NAND, o primeiro dos itens acima é facilmente reconhecido como comutatividade da NAND. Depois disso, são necessárias apenas algumas traduções para dar-lhes nomes: a = (a · a) · (a · a) é como dupla negação, a = (a · a) · (a · b) é como a lei da absorção (a · A) · b = (a · b) · b é semelhante a "enfraquecimento" e assim por diante.

Bem, se vamos aprender alguns "teoremas-chave" da lógica NAND, que tipo de teoremas devem ser esses? Talvez esses devam ser "lemas populares" nas provas.

Obviamente, qualquer teorema pode ter muitas provas possíveis. Mas suponha que usaremos apenas as evidências que FindEquationalProof produz. Acontece que, na prova dos primeiros mil teoremas da NAND, o lema mais popular é a · a = a · ((a · a) · a), seguido por lemas do tipo (a · ((a · a) · a)) · ( a (a ((a) a))) = a.

Quais são esses lemas? Eles são úteis para os métodos usados ​​pelo FindEquationalProof. Mas para as pessoas, elas não parecem ser muito adequadas.

E os lemas que acabam sendo curtos? a · b = b · a definitivamente não é o mais popular, mas o mais curto. (a · a) · (a · a) = a é mais popular, mas mais longo. E então existem lemas como (a · a) · (b · a) = a.

Quão úteis serão esses lemas? Aqui está uma maneira de verificar isso. Vamos examinar os primeiros mil teoremas da NAND e avaliar como a adição de lemas reduz as provas desses teoremas (pelo menos os encontrados por FindEquationalProof):


a · b = b · a é muito bem-sucedido e geralmente apara a prova em quase 100 etapas. (a · a) · (a · a) = a tem muito menos sucesso; às vezes até “confunde” o FindEquationalProof, forçando você a executar mais etapas do que o necessário (valores negativos nos gráficos). (a · a) · (b · a) = a lida bem com a contração, mas não tão boa quanto a · b = b · a. Embora, se você combiná-lo com a · b = b · a, como resultado, as reduções ocorrerão com mais frequência.

A análise pode ser continuada, por exemplo, incluindo uma comparação de quanto um lema específico encurta os comprimentos das evidências em relação ao comprimento original. Mas o problema é que, se você adicionar alguns “lemas úteis” como a · b = b · a e (a · a) · (b · a) = a, ainda haverá muitas evidências longas - isto é, muito do que é necessário Para entender.

O que podemos entender?

Existem diferentes maneiras de modelar as coisas. Por várias centenas de anos, as ciências exatas foram dominadas pela idéia de encontrar equações matemáticas que pudessem ser resolvidas para mostrar como o sistema se comportaria. Mas desde o advento do meu livro, houve uma mudança ativa na criação de programas que você pode executar para ver como os sistemas se comportarão.

Às vezes, esses programas são escritos para uma tarefa específica; Às vezes, eles são pesquisados ​​por um longo tempo. E em nosso tempo, pelo menos uma classe desses programas é derivada usando o aprendizado de máquina, pelo método de movimento reverso, a partir de exemplos conhecidos de comportamento do sistema.

E quão fácil é "entender o que está acontecendo" com esses vários tipos de modelagem? Encontrar a “solução exata” das equações matemáticas é uma grande vantagem - então o comportamento do sistema pode ser descrito por uma fórmula matemática exata. Mas mesmo quando isso não é possível, muitas vezes é possível escrever algumas declarações matemáticas abstratas o suficiente para serem relacionadas a outros sistemas e comportamentos.

Como escrevi acima, com um programa - como um autômato celular - tudo pode ser diferente. Muitas vezes acontece que encontramos imediatamente irredutibilidade computacional, o que limita nossa capacidade de percorrer um curto caminho e "explicar" o que está acontecendo.

E o aprendizado de máquina e as redes neurais? Em certo sentido, o treinamento em redes neurais é como um breve resumo da busca indutiva em andamento nas ciências naturais. Estamos tentando, começando com exemplos, deduzir um modelo de comportamento do sistema. Mas será possível entender o modelo?

E, novamente, há problemas com a irredutibilidade computacional. Mas vamos discutir um caso em que podemos imaginar como seria a situação e entender o que está acontecendo.

Em vez de usar uma rede neural para simular o comportamento do sistema, vamos criar uma rede neural que classifique alguns aspectos do mundo: por exemplo, capturar imagens e distribuí-las de acordo com seu conteúdo (“barco”, “girafa” etc.). Quando treinamos a rede neural, ela aprende a produzir a saída correta. Mas você pode imaginar esse processo como uma construção interna de uma sequência de diferenças (algo como um jogo de " vinte perguntas "), que finalmente determina a conclusão correta.

Mas quais são essas diferenças? Às vezes podemos reconhecê-los. Por exemplo, "Há muito azul na imagem?" Mas na maioria das vezes, essas são algumas propriedades do mundo que as pessoas não percebem. Talvez exista uma história alternativa das ciências naturais em que algumas delas se mostrem. Mas eles não fazem parte do cânone atual da percepção ou análise.

Se quiséssemos adicioná-los, talvez viéssemos criar nomes para eles. Mas esta situação é semelhante à situação com evidência lógica. O sistema automático criou algumas coisas que ele usa como marcos para gerar o resultado. Mas não reconhecemos esses marcos, eles não significam nada para nós.

Novamente, se descobrimos que certas diferenças específicas são frequentemente encontradas em redes neurais, poderíamos decidir que elas são dignas de nós estudá-las por nós mesmos e adicioná-las ao cânone padrão de maneiras de descrever o mundo.

Podemos esperar que um pequeno número dessas diferenças nos permita criar algo significativo? Parece que a questão é se um pequeno número de teoremas nos ajudará a entender uma prova lógica.

Eu acho que a resposta não está clara. Se você estuda, por exemplo, um grande conjunto de trabalhos científicos em matemática, pode fazer perguntas sobre a frequência de uso de vários teoremas. Acontece que a frequência dos teoremas corresponde quase perfeitamente à lei de Zipf (e, em primeiro lugar, haverá um teorema central do limite ,teorema da função implícita e teorema de Tonelli-Fubini ). O mesmo acontece provavelmente com diferenças que valem a pena conhecer ou com novos teoremas que valem a pena conhecer.

O conhecimento de vários teoremas nos dará a oportunidade de avançar o suficiente, mas sempre haverá uma cauda exponencial infinita e não chegaremos ao fim.

Futuro do conhecimento

Estudando matemática, ciência ou tecnologia, você pode ver caminhos básicos semelhantes de desenvolvimento qualitativo, consistindo na construção de um conjunto de abstrações cada vez maiores. Seria bom quantificar esse processo. Talvez seja possível calcular como certos termos ou descrições que são frequentemente encontrados ao mesmo tempo são incluídos em níveis mais altos de abstração, nos quais novos termos ou descrições, por sua vez, parecem relacionados a eles.

Pode ser possível criar um modelo idealizado desse processo usando um modelo formal de computação, como máquinas de Turing. Imagine que no nível mais baixo existe uma máquina de Turing básica sem abstrações. Agora imagine que selecionamos programas para esta máquina de Turing de acordo com algum processo aleatório específico. Em seguida, executamos esses programas e os analisamos para ver qual modelo do nível "mais alto" de computação pode reproduzir com êxito o comportamento conjunto desses programas sem precisar executar cada etapa de cada um deles.

Pode-se decidir que a irredutibilidade computacional levaria ao fato de que a criação desse modelo de computação de nível superior seria inevitavelmente mais complicada. Mas o ponto principal é que estamos apenas tentando reproduzir o comportamento conjunto dos programas, e não o comportamento separado deles.

Mas o que acontece se esse processo se repete repetidamente, reproduzindo a história intelectual idealizada do homem e criando uma torre de abstrações cada vez mais alta?

Presumivelmente, aqui podemos traçar uma analogia com fenômenos críticos na física e no método do grupo de renormalização . Nesse caso, podemos imaginar que podemos determinar a trajetória no espaço das plataformas para representar conceitos. O que essa trajetória fará?

Talvez tenha um valor fixo quando, a qualquer momento da história, houver aproximadamente a mesma quantidade de estudos que valem a pena - novos conceitos se abrem lentamente e os antigos são absorvidos.

O que isso significa para matemática? Por exemplo, que quaisquer “fatos matemáticos aleatórios” descobertos empiricamente serão considerados ao atingir um certo nível de abstração. Não há um entendimento óbvio de como esse processo funcionará. De fato, em qualquer nível de abstração, sempre existem novos fatos empíricos para os quais é preciso "pular". Também pode acontecer que "aumentar o nível de abstração" se mova mais lentamente do que o necessário para esses "saltos".

Futuro da compreensão

O que tudo isso significa para o entendimento futuro?

No passado, quando as pessoas estudavam a natureza, tinham um pequeno número de razões para entendê-la. Às vezes, eles personificavam certos aspectos dele na forma de espíritos ou deidades. Mas eles aceitaram como era, sem pensar na possibilidade de entender todos os detalhes das causas dos processos.

Com o advento da ciência moderna - e especialmente quando mais e mais de nossas vidas são gastas em ambientes artificiais dominados pelas tecnologias desenvolvidas por nós - essas expectativas mudaram. E quando estudamos os cálculos realizados pela IA, não gostamos que talvez não os entendamos.

No entanto, sempre haverá uma competição entre o que os sistemas de nosso mundo fazem e o que nosso cérebro pode calcular a partir de seu comportamento. Se decidirmos interagir apenas com sistemas que são muito mais simples do que o cérebro no poder da computação, podemos esperar que possamos entender sistematicamente o que eles estão fazendo.

Mas se queremos usar todos os recursos de computação disponíveis no universo, inevitavelmente os sistemas com os quais interagimos alcançarão o poder de processamento do nosso cérebro. E isso significa que, de acordo com o princípio da irredutibilidade computacional, nunca podemos sistematicamente "ultrapassar" ou "entender" a operação desses sistemas.

Mas como então podemos usá-los? Bem, assim como os humanos sempre usavam os sistemas da natureza. Obviamente, não conhecemos todos os detalhes de seu trabalho ou capacidade. Mas, em um certo nível de abstração, sabemos o suficiente para entender como atingir nossos objetivos com a ajuda deles.

E quanto a áreas como matemática? Em matemática, estamos acostumados a construir nosso conjunto de conhecimentos para entendermos cada passo. Mas a matemática experimental - bem como recursos como prova automática de teoremas - tornam óbvia a existência de áreas nas quais esse método não estará disponível para nós.

Vamos chamá-los de "matemática"? Eu acho que eles deveriam. Mas essa tradição é diferente da que estamos acostumados no último milênio. Ainda podemos criar abstrações lá e construir novos níveis de entendimento.

Mas em algum lugar em sua base haverá todo tipo de versões diferentes de irredutibilidade computacional, que nunca podemos transferir para o campo da compreensão humana. Isso é aproximadamente o que acontece na prova do meu pequeno axioma da lógica. Este é um exemplo inicial do que acho que será um dos principais aspectos da matemática - e muito mais - no futuro.