Fonte: Turing Community

Autor: Lin Jun Cen Feng

Wu Wenjun no trabalho (12 de maio de 1919 a 7 de maio de 2017). Fonte: Academia de Matemática e Ciências de Sistemas, Academia Chinesa de Ciências

1979 foi um ano importante na China. Muitos eventos importantes ocorreram neste ano, e também é considerado um importante ponto de virada na política, economia, tecnologia, cultura e outros campos da China, bem como um dos importantes pontos de interrupção do período na história chinesa moderna. Comparado com a magnífica nova era aberta em 1979, o início da pesquisa de inteligência artificial (IA) da China em 1979 só pode ser considerado uma onda discreta na maré histórica, mas na história da inteligência artificial da China, este é um evento inovador.

A primeira escola de inteligência artificial foi a escola do simbolismo. A maioria dos primeiros cientistas de inteligência artificial eram matemáticos e lógicos. Eles combinaram computadores com suas próprias pesquisas após o nascimento dos computadores, entrando assim no campo da inteligência artificial. Na China, também foram os matemáticos que abriram a primeira página da pesquisa em inteligência artificial. Em 1979, seja o "Método Wu" em provas de máquina que foi para o mundo, ou a realização do Simpósio de Verão de Ciência da Computação comparável à Conferência de Dartmouth, havia matemáticos por trás disso. É também a partir deste ano que a inteligência artificial da China começou a alcançar o mundo.

O proponente do "Método Wu" não é outro senão o matemático Wu Wenjun. Juntamente com Wang Xianghao e Zeng Xianchang, ele é chamado de "Três Mestres da Prova de Máquina". No final dos anos 1970, Wu Wenjun, com quase sessenta anos de idade, partiu do estudo da matemática chinesa antiga e criou um novo campo de mecanização matemática. Ele propôs o "Método Wu" para provar teoremas geométricos com computadores, que é considerado um trabalho pioneiro no campo do raciocínio automático.

1. Wu Wenjun abriu as portas para a inteligência artificial da China ir para o mundo

Em janeiro de 1979, a convite do Instituto de Estudos Avançados de Princeton, o matemático Wu Wenjun embarcou em um voo de intercâmbio para os Estados Unidos com US$ 25 mil no bolso.

Ele estava acompanhado pelo matemático Chen Jingrun. Os dois são a primeira leva de cientistas convidados a estudar e visitar os Estados Unidos após o estabelecimento das relações diplomáticas entre a China e os Estados Unidos.Eles vão estudar e fazer intercâmbio no Instituto de Estudos Avançados de Princeton por um período. O tema da conversa de Chen Jingrun é naturalmente "1+2", e o conteúdo principal da conversa de Wu Wenjun nesta viagem, além de sua antiga profissão de topologia, é mais sobre a história da matemática chinesa antiga e da mecanização matemática. para usar os 25.000 yuans que ele trouxe, compre um computador para o estudo da mecanização matemática.

Quando Wu Wenjun ganhou o primeiro prêmio de ciências naturais da Academia Chinesa de Ciências (doravante denominada "Academia Chinesa de Ciências") em 1979, a mecanização matemática tornou-se sua principal direção de pesquisa. Essa direção de pesquisa também atraiu a atenção do mundo. O método de pesquisa de Wu Wenjun é chamado de "Método Wu" no campo da prova de teoremas de máquinas. O prêmio mais alto da ciência e tecnologia inteligente da China "Prêmio de Ciência e Tecnologia de Inteligência Artificial Wu Wenjun" usa O nome de Wu Wenjun para comemorar Wu Wenjun como Conquistas de pesquisadores chineses em áreas relacionadas à IA.

Inadvertidamente, Wu Wenjun abriu as portas para que a pesquisa de inteligência artificial da China se tornasse global. A pesquisa de Wu Wenjun sobre a história da matemática chinesa antiga começou por volta de 1974. Naquela época, Guan Zhaozhi, vice-diretor do Instituto de Matemática da Academia Chinesa de Ciências (doravante referido como o "Instituto de Matemática da Academia Chinesa de Ciências"), pediu a Wu Wenjun para estudar matemática chinesa antiga. Wu Wenjun descobriu rapidamente a importante diferença entre a tradição matemática chinesa antiga e a tradição matemática ocidental moderna herdada da Grécia antiga. Ele realizou uma análise completa da aritmética chinesa antiga e desenvolveu percepções únicas em muitos aspectos.

Na década de 1970, os intercâmbios acadêmicos estrangeiros começaram a se recuperar gradualmente. Em 1975, Wu Wenjun foi para a França para um intercâmbio e fez um relatório sobre o antigo pensamento matemático chinês no Instituto Francês de Ciências Avançadas. Nessa época, Wu Wenjun havia restaurado a antiga prova da fórmula de Rigao e notado as características "estruturais" e "mecanicistas" da antiga matemática chinesa. No Festival da Primavera de 1977, Wu Wenjun verificou a viabilidade do método de prova de máquina de teorema geométrico por cálculo manual, e o processo durou dois meses.

A ideia original de provar o teorema da máquina vem do raciocinador de cálculo de Gottfried Wilhelm Leibniz e, posteriormente, evoluiu da lógica simbólica. Mais tarde, David Hilbert (David Hilbert) lançou o "Projeto Hilbert" em 1920 com base nisso, esperando axiomatizar estritamente todo o sistema matemático. Simplificando, se esse plano for realizado, significa que para qualquer conjectura matemática, não importa o quão difícil seja, sempre podemos saber se a conjectura está correta e prová-la ou negá-la. Isso é o que Hilbert quis dizer quando disse "Wir müssen wissen, wir werden wissen" (devemos saber, devemos saber).

No entanto, pouco tempo depois, em 1931, Kurt Gödel propôs o teorema da incompletude de Gödel, que quebrou os ideais de formalismo de Hilbert. Mas de qualquer maneira, quando Gödel fechou a porta, ele ainda deixou uma janela. A dissertação de doutorado do gênio matemático francês Jacques Herbrand lançou as bases para a teoria da prova e a teoria da recursão da lógica matemática. Depois que o teorema da incompletude de Gõdel foi proposto, Herbrand verificou sua tese e partiu. escreveu uma carta a Gödel pedindo conselhos. Gödel respondeu a Erblan, mas Erblan não conseguiu esperar pela carta e morreu em um acidente de montanhismo dois dias depois que Gödel respondeu aos 23 anos. Mais tarde, o maior prêmio no campo da prova de teoremas também recebeu o nome de El Brown, e Wu Wenjun ganhou o quarto prêmio El Brown por Outstanding Achievement in Automatic Reasoning em 1997.

Outros matemáticos complementaram o teorema de Gödel. Pouco depois de Gödel provar que "números inteiros de primeira ordem (aritméticos) são indecidíveis", Alfred Tarski provou que "números reais de primeira ordem (geométricos e algébricos) são decidíveis".

Em 1936, Turing em seu importante artigo "On Computable Numbers, with an Application to the Entscheidungsproblem" (On Computable Numbers, with an Application to the Entscheidungsproblem) da prova de Gödel de 1931 e restrições de computação Como resultado, a discussão foi retrabalhada, e a linguagem formal de Gödel baseada na aritmética geral foi substituída por uma forma simples de dispositivo abstrato agora chamada de máquina de Turing, e provou-se que todos os processos computáveis podem ser simulados por uma máquina de Turing. Esta é também uma importante base teórica para ciência da computação e inteligência artificial. A escola mais antiga de inteligência artificial - a escola de símbolos também é estendida com base em operações lógicas formais.

Voltando a Wu Wenjun, ele trabalhou na Beijing Radio No. 1 Factory que produzia computadores na década de 1970, e nessa época ele começou a ter contato com computadores e prova de teoremas de máquinas. "Como fazer pleno uso do poder do computador e aplicá-lo à sua própria pesquisa matemática" tornou-se o que interessa a Wu Wenjun. Mais tarde, Wu Wenjun começou a estudar a história da matemática chinesa antiga e resumiu a tendência algébrica geométrica e o pensamento algorítmico da matemática chinesa antiga. Depois de descobrir as diferentes formas de pensar entre a matemática chinesa antiga e a matemática ocidental, ele decidiu usar um método diferente para fazer provas mecânicas de teoremas geométricos.

Naquela época, Wu Wenjun leu muitos artigos estrangeiros e entendeu completamente a prova da máquina. Naquela época, a pesquisa mais avançada sobre a demonstração do teorema da máquina veio do lógico matemático Wang Hao. Durante seus estudos no Departamento de Matemática da Southwestern Associated University, ele estudou com o famoso filósofo e "a primeira pessoa na filosofia chinesa" Jin Yuelin, e depois foi para a Universidade de Harvard nos Estados Unidos.O famoso filósofo e lógico Willard von Quinn (WV Quine) estudou o sistema formal de axiomas fundado por Quine e obteve um doutorado. Já em 1953, Wang Hao já havia começado a pensar na possibilidade de provar teoremas matemáticos com máquinas.

Em 1958, Wang Hao usou um programa de lógica proposicional em um computador IBM 7041 para provar todos os teoremas de lógica de primeira ordem em "Principles of Mathematics" e completou a prova de todos os 200 teoremas de lógica proposicional no ano seguinte. A importância do trabalho de Wang Haozhi está em anunciar a possibilidade de usar computadores para provar teoremas. Quando ele voltou para a China em 1977, ele participou de vários simpósios que afetaram o desenvolvimento de longo prazo da ciência e tecnologia do meu país e deu 6 palestras especiais na Academia Chinesa de Ciências, que tiveram um impacto significativo na pesquisa doméstica de provas de máquinas.

Mais perto de casa, ainda há uma lacuna entre as provas anteriores de teoremas de lógica proposicional de Wang Hao em "Principles of Mathematics" e as provas mecânicas de teoremas geométricos que Wu Wenjun deseja alcançar. O primeiro tem componentes lógicos mais simbólicos, enquanto o último tem componentes do raciocínio. Naquela época, havia muitos estudos no exterior sobre provas mecânicas de teoremas geométricos, mas todos falharam.

Em segundo lugar, da mecanização do antigo pensamento matemático chinês ao "Método Wu"

Na visão de Wu Wenjun, a experiência do fracasso também é muito importante, ela vai te dizer quais estradas não vão funcionar. Inspirado pelo pensamento de Descartes, ele transformou problemas geométricos em problemas algébricos introduzindo coordenadas e depois os mecanizou de acordo com o antigo pensamento matemático chinês. Wu Wenjun até combinou o pensamento cartesiano com o antigo pensamento matemático chinês e propôs uma rota para resolver problemas gerais:

Todos os problemas podem ser transformados em problemas matemáticos, todos os problemas matemáticos podem ser transformados em problemas algébricos, todos os problemas algébricos podem ser transformados em problemas de resolução de equações e todos os problemas de resolução de equações podem ser transformados em problemas de equação algébrica de variáveis simples.

A matemática chinesa antiga e a matemática moderna ocidental são dois sistemas diferentes. Wu Wenjun restaurou o "Zhou Bi Suan Jing" de acordo com o conhecimento e pensamento e raciocínio habituais dos antigos naquela época, sem usar "ferramentas modernas", como funções trigonométricas, cálculo, fatoração e soluções de equações de alta ordem na matemática moderna. Os métodos de prova de "Rigao Tushuo", "Dayanqiuyishu" e "Zengchengkaifangshu" em "Nove Capítulos de Shushu". Ele acredita que a matemática chinesa antiga tem suas próprias características únicas. O método de Qin Jiushao tem as características de construção e mecanização, e a solução numérica de equações algébricas de alta ordem pode ser obtida com uma pequena calculadora. Na ausência de equipamentos de computação de alto desempenho na época, Wu Wenjun foi capaz de fazer pleno uso das antigas ideias matemáticas chinesas para conduzir pesquisas sobre redução de dimensionalidade, o que também é louvável.

O primeiro teorema que Wu Wenjun provou de acordo com essa ideia foi o teorema de Feuerbach, que provou que "o círculo de nove pontos de um triângulo é tangente ao seu círculo inscrito e três círculos circunscritos". Este é um dos mais belos teoremas da geometria plana, que pode ser visto na estética de Wu Wenjun. Não havia computador naquela época, então Wu Wenjun calculou à mão. Uma das características do "método de Wu" é que um grande número de polinômios será gerado. O maior polinômio envolvido no processo de prova possui centenas de itens. Esse cálculo é muito difícil e qualquer erro em uma etapa fará com que os cálculos subsequentes sejam falhar. No Festival da Primavera de 1977, Wu Wenjun verificou com sucesso o método de prova de máquina de teorema geométrico pela primeira vez por cálculo manual.

Wu Wenjun publicou o artigo de pesquisa relacionado "Problemas de determinação de geometria elementar e prova mecanizada" na "Ciência chinesa" em 1977 e enviou o artigo a Wang Hao. Wang Hao elogiou o trabalho de Wu Wenjun e escreveu de volta para sugerir que Wu Wenjun usasse o pacote de álgebra existente e considerasse a implementação do método de Wu com um computador. Wang Hao não percebeu a diferença entre os computadores usados pelos principais estudiosos da China e dos Estados Unidos na época: a Grande Muralha 203 pode usar linguagem de máquina, mas os sistemas de instrução de diferentes computadores não são universais e não é viável para usar o pacote de álgebra existente. Então, mais tarde, Wu Wenjun simplesmente pegou emprestada uma pequena calculadora do Instituto de Matemática da Academia Chinesa de Ciências como presente de um estrangeiro que visitou o Instituto de Matemática da Academia Chinesa de Ciências, converteu a proposição dada em uma forma algébrica, e então usou o método de Qin Jiushao para calcular a equação de ordem superior.

A pesquisa de Wu Wenjun sobre a prova mecânica de teoremas geométricos foi fortemente apoiada por Guan Zhaozhi. Guan Zhaozhi estudou na França e foi um dos fundadores da filial francesa da Associação Chinesa de Cientistas, reunindo um grupo de destacados intelectuais patrióticos, e Wu Wenjun era um deles. Naquela época, o Instituto de Matemática da Academia Chinesa de Ciências, onde Wu Wenjun trabalhava, tinha relações complicadas. transferiu-se da topologia e da análise funcional para a teoria do controle, apoiou-o particularmente e o compreendeu.Digamos que Wu Wenjun pode fazer o que quiser. Mais tarde, quando Guan Zhaozhi estabeleceu o Instituto de Ciência de Sistemas da Academia Chinesa de Ciências em 1979, Wu Wenjun seguiu Guan Zhao para o Instituto de Ciência de Sistemas da Academia Chinesa de Ciências (Figura 1-1).

Figura 1-1 O edifício de escritórios original do Instituto de Ciência de Sistemas, Academia Chinesa de Ciências (agora Edifício Rongke) no início dos anos 1980 (da esquerda: Xu Guozhi, Wu Wenjun, estudioso indiano, Guan Zhaozhi)

Para provar teoremas mais complicados, são necessárias máquinas melhores. O acadêmico Wang Dezhao, então diretor do Instituto de Acústica da Academia Chinesa de Ciências, deu conselhos a Wu Wenjun. Ele disse a Wu Wenjun quando e onde Li Chang, secretário do grupo do partido e vice-presidente da Academia Chinesa de Ciências, apareceria, mas Wu Wenjun realmente o pegou. Li Chang tinha a mente muito aberta. Quando atuou como presidente do Harbin Institute of Technology (doravante referido como "HIT") na década de 1950, ele transformou o HIT em uma universidade nacional de primeira classe. Entre as seis principais universidades nacionais identificadas em 1954, o Harbin Institute of Technology é a única que não está localizada em Pequim. Li Chang também deu grande apoio ao trabalho de Wu Wenjun. A moeda estrangeira de Wu Wenjun de 25.000 dólares americanos para comprar um computador nos Estados Unidos foi especialmente aprovada por Li Chang. Com este computador, muitos teoremas foram provados rapidamente.

A década de 1970 também foi a idade de ouro da prova de teoremas da máquina. Em 1976, dois matemáticos americanos provaram o teorema das quatro cores usando um computador eletrônico de alta velocidade com 1200 horas de tempo de cálculo e resolveram o difícil problema que os matemáticos não resolviam há mais de 100 anos. A razão pela qual o teorema das quatro cores pode ser provado é que conjuntos irredutíveis e conjuntos inevitáveis são finitos. 2.000 tipos de formas básicas e, em seguida, use o poder de computação do computador para força bruta e prove-as uma a uma. Falando metaforicamente, essa abordagem é como resolver um cubo de Rubik - desmontar o cubo e montá-lo novamente - deselegante, mas eficaz. Agora dizemos que o GPT-3 "faz milagres com grande esforço", mas na verdade a prova do teorema das quatro cores é o ancestral dos "milagres com grande esforço".

No entanto, essa prática de usar o poder de computação do computador para provas do teorema da força bruta não pode ser generalizada. O primeiro passo na prova do teorema, a formalização do teorema, requer uma formulação completa e rigorosa. Neste ponto, há uma pequena história sobre um matemático. Um astrônomo, um físico e um matemático viajaram de trem para a Escócia. Eles viram uma ovelha negra do lado de fora da janela. O astrônomo começou a suspirar: "Por que todas as ovelhas na Escócia são pretas?" O físico corrigiu: " Deve-se dizer que algumas as ovelhas na Escócia são pretas." A expressão mais rigorosa vem dos matemáticos: "Na Escócia existe pelo menos um mundo, e há pelo menos uma ovelha, e esta ovelha é preta pelo menos de um lado." Há outra piada, disse que os problemas matemáticos são divididos em duas categorias: uma é "isso também precisa ser provado?", e a outra é "isso também pode ser provado?". A partir disso, podemos ver como é difícil para uma prova ser reconhecida por outros matemáticos. Da mesma forma, para formalizar um teorema em um provador de teorema interativo, é necessário preencher todos os detalhes técnicos para completar a "automação" do raciocínio e, finalmente, substituir o teorema por uma ideia de solução de problemas factível, mas computacionalmente intensiva. . Em outras palavras, este método ainda depende da compreensão dos teoremas dos matemáticos e só pode alcançar "uma teoria e uma prova", que só podem ser consideradas como provas de teoremas auxiliadas por computador.

Portanto, depois que o teorema das quatro cores foi provado por computador, um grupo de lógicos, incluindo Wang Hao, apresentou opiniões diferentes: O teorema das quatro cores foi provado? Este tipo de método de prova é considerado como prova tradicional, e o computador desempenha apenas o papel de cálculo auxiliar. Não foi até 2005 que Georges Gonthier concluiu a prova computadorizada completa do teorema das quatro cores, e cada etapa de sua derivação lógica foi concluída por um computador. Atualmente, as pessoas provaram centenas de teoremas matemáticos com computadores, mas a maioria desses teoremas é conhecida e a "inteligência da máquina" ainda não deu uma contribuição real para a matemática.

A prova de teoremas de máquina depende de algoritmos. No estágio inicial, os pesquisadores frequentemente tentavam encontrar um superalgoritmo para resolver todos os problemas, mas Wu Wenjun aplicou antigas ideias matemáticas chinesas ao campo da prova mecânica de teoremas geométricos, alcançando "um tipo, uma prova". Este ponto também foi acordado por Wang Hao. Ele acreditava que seus primeiros trabalhos tinham algo em comum com o método usado por Wu Wenjun, ou seja, primeiro encontre um subcampo relativamente controlável e depois encontre o algoritmo mais eficaz de acordo com as características deste subcampo. Quando Wu Wenjun visitou os Estados Unidos em 1979, ele também foi à Rockefeller University para visitar Wang Hao. Seu trabalho foi valorizado no campo do teorema da máquina, que teve uma certa relação com a forte recomendação de Wang Hao.

O "método Wu" realmente se espalhou, fazendo o primeiro avanço na prova do teorema da máquina na década de 1980, graças a Zhou Xianqing, um estudante estrangeiro nos Estados Unidos que ouviu o curso de prova do teorema da máquina de Wu Wenjun. Zhou Xianqing originalmente queria fazer a pós-graduação de Wu Wenjun na área de prova de máquina, mas ele achava que a geometria diferencial era sua fraqueza, então ele estava com medo de não conseguir passar no exame, então ele finalmente foi admitido na Universidade. de Ciência e Tecnologia da China (doravante denominada "Universidade de Ciência e Tecnologia da China"), e mais tarde fui para o Instituto de Tecnologia de Computação da Academia Chinesa de Ciências como Dai Pei. curso de prova.

Em 1981, Zhou Xianqing foi para a Universidade do Texas em Austin para estudar no exterior. Naquela época, a Universidade do Texas em Austin era conhecida como a rei da prova de teoremas. Zhou Xianqing mencionou o trabalho de Wu Wenjun para Robert Boyer. Boyer achou que era muito novo, então ele continuou a perguntar, mas Zhou Xianqing sabia apenas que estava transformando geometria em álgebra e não podia explicar os detalhes específicos.

Depois disso, Woody Bledsoe pediu a Zhou Xianqing e outro estudante Wang Tiecheng para coletar dados. A tese de doutorado de Zhou Xianqing foi a realização do método de Wu. Wu Wenjun rapidamente enviou dois artigos, ambos assinados por Bledsoe. Nos dois anos seguintes, esses dois artigos foram copiados pela Universidade do Texas em Austin quase uma centena de vezes e enviados para todo o mundo, e o método Wu tornou-se amplamente conhecido.

Em 1983, a Conferência Acadêmica Nacional sobre Prova de Teoremas por Máquinas foi realizada no Colorado, EUA.Zhou Xianqing apresentou um relatório intitulado "Prova de Teoremas de Geometria Usando o Método de Wu" na conferência. O programa geral desenvolvido por Zhou Xianqing pode provar automaticamente mais de 130 teoremas geométricos, incluindo provas de teoremas mais difíceis, como o teorema de Moller, o teorema de Simson, o teorema do círculo de nove pontos de Feuerbach e o teorema de Desargues. Posteriormente, a coleção de artigos desta conferência foi publicada oficialmente em 1984 como o 29º volume da série "Matemática Contemporânea" nos Estados Unidos, e dois artigos relacionados enviados por Wu Wenjun também foram incluídos nela.

Em junho de 1986, o vencedor do Prêmio Turing John Hopcroft (John Hopcroft) e outros organizaram um seminário sobre raciocínio geométrico automático, e parte do relatório do seminário foi incluído no "Artificial Na edição especial de "Inteligência", o artigo de introdução de a edição especial apresenta especialmente o novo método de geometria algébrica proposto por Wu Wenjun. Visão, modelagem sólida) também tem valor de aplicação importante (Figura 1-2). Desde então, Hopcroft trabalhou em estreita colaboração com muitas universidades na China. Ele tem institutos de pesquisa liderados por ele na Shanghai Jiao Tong University, na Peking University e na Chinese University of Hong Kong (Shenzhen). Wu Wenjun e Wu Fafang são provavelmente o começo de seu complexo chinês.

Figura 1-2 Uma visão geral do método de Wu no capítulo de abertura da edição especial de "Inteligência Artificial" em 1988