Початок розвитку штучного інтелекту в Китаї тісно пов’язаний із цим математиком

1979 рік був важливим роком для Китаю. У цьому році відбулося багато важливих подій, і він також вважається важливим поворотним моментом у політиці, економіці, науці та техніці, культурі та інших сферах Китаю та одним із важливих переломних моментів у сучасній китайській історії. Порівняно з чудовою новою ерою, яка розпочалася в 1979 році, початок досліджень штучного інтелекту (ШІ) у Китаї в 1979 році можна розглядати лише як непомітну хвилю в історичній хвилі, але в історії штучного інтелекту в Китаї це новаторство. подія.

Найпершою школою штучного інтелекту була школа символізму. Більшість перших учених штучного інтелекту були математиками та логіками. Вони поєднали комп’ютери з власними дослідженнями після народження комп’ютерів, таким чином увійшовши в сферу штучного інтелекту. У Китаї також математики відкрили першу сторінку досліджень штучного інтелекту. У 1979 році, незалежно від того, чи це був «Метод Ву» в машинних доказах, який пішов у світ, чи проведення Літнього симпозіуму з комп’ютерних наук, порівнянного з Дартмутською конференцією, за цим стояли математики. Крім того, з цього року штучний інтелект Китаю почав наздоганяти світ.

Автором «методу У» є не хто інший, як математик У Веньцзюнь. Разом із Ван Сяньхао та Цзен Сяньчаном його називають «Трьома майстрами машинного доказу». Наприкінці 1970-х років Ву Веньцзюнь, якому було майже шістдесят років, розпочав вивчення давньокитайської математики та створив нову галузь математичної механізації.Він запропонував «метод Ву» для доведення геометричних теорем за допомогою комп’ютерів, який вважається піонерська робота в галузі автоматичного міркування.

1. У Веньцзюнь відкрив двері китайському штучному інтелекту у світ

У січні 1979 року на запрошення Інституту передових досліджень у Прінстоні математик У Веньцзюнь сів на борт обмінного рейсу до Сполучених Штатів з 25 000 доларів у кишені.

Його супроводжував математик Чень Цзінжунь. Ці двоє є першою групою вчених, запрошених для навчання та відвідування Сполучених Штатів після встановлення дипломатичних відносин між Китаєм та Сполученими Штатами.Вони навчатимуться та обмінюватимуться в Інституті передових досліджень у Прінстоні протягом певного часу. Тема обміну Чень Цзінжунь, природно, "1+2", і основний зміст обміну У Веньцзюня під час цієї поїздки, на додаток до його старої професії топології, стосується історії давньокитайської математики та математичної механізації. Він хоче щоб використати 25 000 юанів, які він приніс, купити комп’ютер для вивчення математичної механізації.

Коли У Веньцзюнь отримав першу премію з природничих наук від Академії наук Китаю (надалі «Китайська академія наук») у 1979 році, математична механізація стала його основним напрямком досліджень. Цей напрямок досліджень також привернув увагу світу. Метод дослідження Ву Веньцзюня в галузі машинного доведення теорем називається «Методом Ву». Найвища нагорода китайської інтелектуальної науки та техніки «Премія Ву Веньцзюня за науку та технології штучного інтелекту» використовує Ім’я Ву Веньцзюня на честь пам’яті Ву Веньцзюня як досягнення китайських дослідників у галузях, пов’язаних зі штучним інтелектом.

Ненавмисно У Веньцзюнь відкрив двері китайським дослідженням штучного інтелекту, щоб вийти на глобальний рівень. Дослідження У Веньцзюня з історії давньокитайської математики почалися приблизно в 1974 році. У той час Гуань Чжаочжі, заступник директора Інституту математики Академії наук Китаю (далі – «Інститут математики Академії наук Китаю»), попросив У Веньцзюня вивчити давньокитайську математику. У Веньцзюнь швидко виявив важливу різницю між давньокитайською математичною традицією та сучасною західною математичною традицією, успадкованою від стародавньої Греції.Він провів ретельний аналіз давньокитайської арифметики та розвинув унікальні ідеї в багатьох аспектах.

У 1970-х роках міжнародні академічні обміни почали поступово відновлюватися. У 1975 році У Веньцзюнь поїхав до Франції за обміном і зробив доповідь про давньокитайську математичну думку у Французькому інституті передових наук. У цей час У Веньцзюнь відновив стародавній доказ формули Рігао і помітив «структурні» та «механістичні» характеристики стародавньої китайської математики. На Весняному фестивалі 1977 року Ву Веньцзюнь перевірив можливість використання методу машинного доказу геометричної теореми шляхом розрахунків вручну, і процес тривав два місяці.

Оригінальна ідея машинного доведення теорем походить від обчислення Готфріда Вільгельма Лейбніца, а пізніше розвинулась із символічної логіки. Пізніше Девід Гільберт (David Hilbert) запустив «Проект Гільберта» в 1920 році на цій основі, сподіваючись строго аксіоматизувати всю математичну систему. Простіше кажучи, якщо цей план реалізується, це означає, що для будь-якої математичної здогадки, якою б важкою вона не була, ми завжди можемо знати, чи здогадка правильна, і довести або спростувати її. Саме це мав на увазі Гільберт, коли сказав «Wir müssen wissen, wir werden wissen» (ми повинні знати, ми повинні знати).

Однак незабаром після цього, у 1931 році, Курт Ґодель запропонував теорему Ґоделя про неповноту, яка зруйнувала ідеали формалізму Гільберта. Але в будь-якому випадку, коли Гедель зачинив двері, він все одно залишив вікно. Докторська дисертація геніального французького математика Жака Ербрана заклала основу для теорії доказів і теорії рекурсії математичної логіки.Після того, як була запропонована теорема про неповноту Ґоделя, Ербранд перевірив свою тезу та пішов. Одним словом, Гедель і мої результати не суперечать один одному, і я написав листа Геделю за порадою. Ґодель відповів Ерблану, але Ерблан не дочекався листа. Він загинув у альпінізмі через два дні після того, як Ґодель відповів у віці 23 років. Пізніше найвища нагорода в галузі доведення теорем також була названа на честь Ель Брауна, а У Веньцзюнь отримав четверту премію Ель Брауна за видатні досягнення в автоматичному міркуванні в 1997 році.

Інші математики доповнили теорему Геделя. Невдовзі після того, як Гедель довів, що «цілі числа першого порядку (арифметичні) нерозв’язні», Альфред Тарскі довів, що «дійсні числа першого порядку (геометричні та алгебраїчні) є розв’язними». Це також закладає основу для машинних доказів.

У 1936 році Тюрінг у своїй важливій статті «Про обчислювані числа, із застосуванням до Entscheidungsproblem» (Про обчислювані числа, із застосуванням до Entscheidungsproblem) про доказ Геделя 1931 року та обмеження обчислень. В результаті обговорення було перероблено, і формальну мову Геделя, засновану на загальній арифметиці, було замінено простою формою абстрактного пристрою, яка тепер називається машиною Тьюрінга, і було доведено, що всі обчислювані процеси можуть бути змодельовані машиною Тьюрінга. Це також важлива теоретична основа для інформатики та штучного інтелекту. Найперша школа штучного інтелекту - школа символів також розширена на основі формальних логічних операцій.

Повертаючись до Ву Веньцзюня, він працював на пекінській фабриці радіо № 1, яка виробляла комп’ютери в 1970-х роках, і в той час він почав контактувати з комп’ютерами та машинним доведенням теорем. «Як повною мірою використати потужність комп’ютера та застосувати її до власних математичних досліджень» стало тим, чим цікавиться Ву Веньцзюнь. Пізніше У Веньцзюнь почав вивчати історію давньокитайської математики та узагальнив геометричну алгебраїчну тенденцію та алгоритмічне мислення давньокитайської математики. Відкривши різні способи мислення між стародавньою китайською математикою та західною математикою, він вирішив використати інший метод для машинних доказів геометричних теорем.

У той час У Веньцзюнь прочитав багато іноземних статей і повністю зрозумів машинний доказ. На той час найпередовіші дослідження з машинного доведення теорем були зроблені математичним логіком Ван Хао.Під час навчання на факультеті математики Південно-західного асоційованого університету він навчався у відомого філософа та «першої людини в китайській філософії» Цзіня Юелін, а потім вступив до Гарвардського університету в Сполучених Штатах.Відомий філософ і логік Віллард фон Куїнн (WV Quine) вивчав формальну систему аксіом, засновану Куайном, і отримав докторський ступінь. Уже в 1953 році Ван Хао почав думати про можливість доведення математичних теорем за допомогою машин.

У 1958 році Ван Хао використовував програму пропозиційної логіки на комп’ютері IBM 7041, щоб довести всі логічні теореми першого порядку в «Принципах математики», і завершив доведення всіх 200 теорем пропозиційної логіки в наступному році. Значення роботи Ван Хаочжі полягає в оголошенні про можливість використання комп’ютерів для доведення теорем. Коли він повернувся до Китаю в 1977 році, він взяв участь у кількох симпозіумах, які стосувалися довгострокового розвитку науки і техніки моєї країни, і прочитав 6 спеціальних лекцій в Академії наук Китаю, що мало значний вплив на вітчизняні машинопробні дослідження.

Ближче до дому все ще існує розрив між попередніми доказами теорем пропозиційної логіки Ван Хао в «Принципах математики» та машинними доказами геометричних теорем, яких хоче досягти У Веньцзюнь. Перше містить більше компонентів символічної логіки, тоді як друге має компоненти міркування.. У той час за кордоном проводилося багато досліджень з машинних доказів геометричних теорем, але всі вони закінчувалися провалом.

По-друге, від механізації давньокитайської математичної думки до «методу Ву»

На думку У Веньцзюня, досвід невдач також дуже важливий, він підкаже вам, які дороги не працюватимуть. Натхненний думкою Декарта, він перетворив геометричні проблеми на алгебраїчні, ввівши координати, а потім механізував це відповідно до давньокитайського математичного мислення. У Веньцзюнь навіть поєднав картезіанську думку з давньою китайською математичною ідеєю та запропонував шлях вирішення загальних проблем:

Усі задачі можна перетворити на математичні задачі, усі математичні задачі можна перетворити на алгебраїчні задачі, усі алгебраїчні задачі можна перетворити на задачі на розв’язування рівнянь, а всі задачі на розв’язування рівнянь можна перетворити на розв’язування задач з одними змінними Задачі на алгебраїчні рівняння.

Стародавня китайська математика та західна сучасна математика — дві різні системи. У Веньцзюнь відновив «Чжоу Бі Суань Цзін» відповідно до знань і традиційного мислення та міркувань стародавніх на той час без використання «сучасних інструментів», таких як тригонометричні функції, обчислення, розкладання на множники та рішення рівнянь високого порядку в сучасній математиці. Методи доказування «Рігао Тушуо», «Даяньцюйшу» та «Цзенченкайфаншу» в «Дев'яти розділах Шушу». Він вважає, що давньокитайська математика має свої унікальні особливості.Метод Цинь Цзюшао має характеристики конструкції та механізації, а чисельне розв’язання алгебраїчних рівнянь високого порядку можна отримати за допомогою невеликого калькулятора. За відсутності на той час високопродуктивного обчислювального обладнання У Веньцзюнь зміг повною мірою використати давньокитайські математичні ідеї для проведення досліджень щодо зменшення розмірності, що також похвально.

Першою теоремою, яку У Веньцзюнь довів згідно з цією ідеєю, була теорема Фейєрбаха, яка доводила, що «коло з дев’ятьма точками трикутника дотикається до його вписаного кола та трьох описаних кіл». Це одна з найкрасивіших теорем у площинній геометрії, яку можна побачити в естетиці У Веньцзюня. У той час не було комп’ютера, тому У Веньцзюнь рахував вручну. Однією з характеристик "методу Ву" є те, що буде згенеровано велику кількість поліномів. Найбільший поліном, який бере участь у процесі доведення, має сотні елементів. Це обчислення дуже складне, і будь-яка помилка на одному кроці спричинить наступні обчислення до провал. На Весняному фестивалі 1977 року Ву Веньцзюнь вперше успішно перевірив метод машинного доказу геометричної теореми шляхом обчислення вручну. Пізніше Ву Веньцзюнь довів теорему Сімсона на Great Wall 203, виробленому Пекінським радіозаводом № 1.

У Веньцзюнь опублікував відповідну дослідницьку статтю «Проблеми визначення елементарної геометрії та механізоване доказ» у «Chinese Science» у 1977 році та надіслав статтю Ван Хао. Ван Хао високо відгукувався про роботу Ву Веньцзюня і написав у відповідь, щоб запропонувати У Веньцзюню використати існуючий пакет алгебри та розглянути можливість реалізації методу Ву за допомогою комп’ютера. Ван Хао не усвідомлював різницю між комп’ютерами, якими в той час користувалися провідні вчені Китаю та Сполучених Штатів: Great Wall 203 може використовувати машинну мову, але системи інструкцій різних комп’ютерів не є універсальними, і це неможливо. використовувати існуючий пакет алгебри. Отже, пізніше Ву Веньцзюнь просто позичив невеликий калькулятор з Інституту математики Академії наук Китаю як подарунок від іноземця, який відвідав Інститут математики Академії наук Китаю, перетворив дане положення в алгебраїчну форму, а потім використав метод Цінь Цзюшао для обчислення рівняння вищого порядку.

Дослідження Ву Веньцзюня щодо машинного доказу геометричних теорем були рішуче підтримані Гуань Чжаочжі. Гуань Чжаочжі навчався у Франції, був одним із засновників французького відділення Китайської асоціації вчених, об'єднав групу видатних патріотично налаштованих інтелектуалів, серед яких і У Веньцзюнь. У той час в Інституті математики Китайської академії наук, де працював Ву Веньцзюнь, були складні відносини.Одна фракція вважала, що виконання машинних доказів є «бунтівним», і сподівалася, що він продовжуватиме займатися топологічними дослідженнями; Гуань Чжаочжі, який перейшов від топології та функціонального аналізу до теорії управління, особливо підтримав і зрозумів його.Скажімо, що У Веньцзюнь може робити все, що забажає. Пізніше, коли в 1979 році Гуань Чжаочжі заснував Інститут системних наук Академії наук Китаю, У Веньцзюнь пішов за Гуань Чжао в Інститут системних наук Академії наук Китаю (рис. 1-1).

Малюнок 1-1 Оригінальна офісна будівля Інституту системних наук Академії наук Китаю (тепер будівля Жунке) на початку 1980-х років (зліва: Сюй Ґуочжі, Ву Веньцзюнь, індійський вчений Гуань Чжаочжі)

Щоб довести складніші теореми, потрібні кращі машини. Академік Ван Дечжао, тодішній директор Інституту акустики Китайської академії наук, дав пораду У Веньцзюню. Він сказав У Веньцзюню, коли і де Лі Чанг, секретар партгрупи та віце-президент Академії наук Китаю, з’явиться, але У Веньцзюнь справді спіймав його. Лі Чанг був дуже відкритим. Коли він працював президентом Харбінського технологічного інституту (надалі «HIT») у 1950-х роках, він перетворив HIT на національний першокласний університет. Серед шести ключових національних університетів, визначених у 1954 році, Харбінський технологічний інститут є єдиним, який не розташований у Пекіні. Лі Чанг також надав велику підтримку роботі Ву Веньцзюня.Обмін Ву Веньцзюня 25 000 доларів США на купівлю комп'ютера в Сполучених Штатах був спеціально схвалений Лі Чангом. За допомогою цього комп’ютера було швидко доведено багато теорем.

1970-ті також були золотим віком машинного доведення теорем. У 1976 році двоє американських математиків довели теорему чотирьох кольорів, використовуючи високошвидкісний електронний комп’ютер із 1200 годинами часу обчислень, і розв’язали складну задачу, яку математики не розв’язували понад 100 років. Причина, чому можна довести теорему чотирьох кольорів, полягає в тому, що незвідні множини та неминучі множини скінченні. Проблема «розфарбовування карти» теореми чотирьох кольорів, здається, має нескінченно багато відображень, але насправді їх можна віднести до більш ніж 2000 видів базових форм, а потім використовуйте обчислювальну потужність комп’ютера для грубої сили та перевіряйте їх одну за одною. Метафорично кажучи, цей підхід схожий на розкладання кубика Рубіка — розбирання кубика та складання його знову — неелегантно, але ефективно. Зараз ми говоримо, що GPT-3 «творить чудеса з великими зусиллями», але насправді доказ теореми про чотири кольори є предком «чудес з великими зусиллями».

Однак цю практику використання обчислювальної потужності комп’ютера для доказів теорем грубою силою не можна узагальнити. Перший крок у доведенні теореми, формалізація теореми, вимагає повного та строгого формулювання. З цього приводу є невелика історія про одного математика. Астроном, фізик і математик їхали поїздом до Шотландії. Вони побачили за вікном чорну вівцю. Астроном почав зітхати: «Чому в Шотландії всі вівці чорні?» Фізик поправив: «Треба сказати, що деякі вівці в Шотландії чорні". Найсуворіший вислів походить від математиків: "У Шотландії існує принаймні один світ, і є принаймні одна вівця, і ця вівця чорна принаймні з одного боку". Є ще такий жарт: сказав, що математичні задачі поділяються на дві категорії: одна — «це теж треба довести?», а друга — «це теж можна довести?». Звідси ми бачимо, як важко визнати доказ іншим математикам. Подібним чином, щоб формалізувати теорему в інтерактивному засобі доведення теорем, необхідно заповнити всі технічні деталі, щоб завершити «автоматизацію» міркувань і, нарешті, замінити теорему здійсненною, але обчислювально інтенсивною ідеєю вирішення проблеми. доказ. . Іншими словами, цей метод все ще покладається на розуміння теорем математиками та може досягти лише «однієї теорії та одного доказу», які можна розглядати лише як комп’ютерні докази теорем.

Тому після того, як теорему чотирьох кольорів було доведено за допомогою комп’ютера, група логіків, включаючи Ван Хао, висунула різні думки: чи доведена теорема чотирьох кольорів? Такий метод доказу вважається традиційним доказом, а комп’ютер відіграє лише роль допоміжного обчислення. Лише у 2005 році Жорж Гонтьє завершив повний комп’ютеризований доказ теореми чотирьох кольорів, і кожен крок її логічного виведення завершувався комп’ютером. На даний момент люди довели сотні математичних теорем за допомогою комп’ютерів, але більшість із цих теорем відомі, а «машинний інтелект» ще не зробив реального внеску в математику.

Машинне доведення теорем спирається на алгоритми. На ранній стадії дослідники часто намагалися знайти супералгоритм для вирішення всіх проблем, але Ву Веньцзюнь застосував давні китайські математичні ідеї до області машинного доказу геометричних теорем, досягнувши «одного типу, одного доказу». З цією думкою погодився і Ван Хао.Він вважав, що його рання робота мала щось спільне з методом, який використовував Ву Веньцзюнь, тобто спочатку знайти відносно контрольоване підполе, а потім знайти найефективніший алгоритм відповідно до характеристик цього підполе. Коли Ву Веньцзюнь відвідав Сполучені Штати в 1979 році, він також відвідав Університет Рокфеллера, щоб відвідати Ван Хао.Його робота була оцінена в галузі машинної теореми, яка мала певний зв'язок із сильною рекомендацією Ван Хао.

«Метод Ву» справді поширився, зробивши перший прорив у машинному доведенні теорем у 1980-х роках завдяки Чжоу Сянціну, іноземному студенту в Сполучених Штатах, який прослухав курс машинного доведення теорем Ву Веньцзюня. Чжоу Сяньцін спочатку хотів отримати диплом Ву Веньцзюня в області машинного доказу, але він вважав, що диференціальна геометрія була його слабкістю, тому він боявся, що він не зможе скласти іспит, тому він нарешті був прийнятий до університету. науки і технологій Китаю (далі «Університет науки і технологій Китаю»), а пізніше пішов до Інституту обчислювальної техніки Академії наук Китаю як Дай Пей. У зв’язку з цим я провів аудит геометричної роботи Ву Веньцзюня доказовий курс.

У 1981 році Чжоу Сянцін поїхав навчатися за кордон до Техаського університету в Остіні.Тоді Техаський університет в Остіні був відомий як король доведення теорем. Чжоу Сяньцін згадав про роботу Ву Веньцзюня Роберту Боєру. Боєр вважав, що вона дуже свіжа, тому він продовжував запитувати, але Чжоу Сяньцін знав лише, що вона перетворює геометрію на алгебру, і не міг пояснити конкретні деталі.

Після цього Вуді Бледсо попросив Чжоу Сяньціна та іншого студента Ван Течена зібрати дані.Докторська дисертація Чжоу Сяньціна була реалізацією методу Ву. У Веньцзюнь швидко надіслав дві статті, обидві з яких він підписав Бледсо. Протягом наступних двох років ці дві статті були скопійовані Техаським університетом в Остіні майже сто разів і розіслані по всьому світу, і метод Ву став широко відомим.

У 1983 році в Колорадо (США) відбулася Національна академічна конференція з машинного доведення теорем, на якій Чжоу Сянцін виступив з доповіддю «Доведення геометричних теорем за допомогою методу Ву». Загальна програма, розроблена Чжоу Сянціном, може автоматично доводити понад 130 геометричних теорем, включаючи докази складніших теорем, таких як теорема Моллера, теорема Сімсона, теорема Фейєрбаха про дев’ятиточкове коло та теорема Дезарга. Згодом збірник доповідей цієї конференції був офіційно опублікований у 1984 році як 29-й том серії «Сучасна математика» в Сполучених Штатах, і дві пов’язані статті, надіслані У Веньцзюнем, також були включені до нього.

У червні 1986 року лауреат премії Тьюринга Джон Хопкрофт (John Hopcroft) та інші організували семінар з автоматичного геометричного мислення, і частина доповіді семінару була включена в «Штучний У спеціальному випуску «Інтелекту», вступна стаття про спеціальне видання спеціально представляє новий метод алгебраїчної геометрії, запропонований Ву Веньцзюнем (Vision, solid modeling) також мають важливе прикладне значення (рис. 1-2). Відтоді Хопкрофт тісно співпрацює з багатьма університетами Китаю. Він має науково-дослідні інститути під його керівництвом у Шанхайському університеті Цзяо Тун, Пекінському університеті та Китайському університеті Гонконгу (Шеньчжень). У Веньцзюнь і У Фафан, ймовірно, є початком його китайський комплекс .

Рисунок 1-2 Огляд методу Ву у першому розділі спеціального видання «Штучного інтелекту» за 1988 рік