中国の人工知能の始まりはこの数学者と密接に関係している

呉文軍（ウー・ウェンジュン、1919年5月12日 - 2017年5月7日）は仕事中。画像提供：中国科学院数学・システム科学研究所

リン・ジュン・チェンフェン |著者

1979年は中国にとって重要な年でした。この一年は多くの重大な出来事が起こり、中国の政治、経済、科学技術、文化などの分野における重要な転換点であり、中国近代史における重要な時期の一つともみなされています。 1979年に始まった壮大な新時代と比較すると、1979年の中国の人工知能（AI）研究の開始は歴史の流れの中では取るに足らない波としかみなせないが、中国の人工知能の歴史においては画期的な出来事である。

人工知能の最も初期の学派は記号学派でした。初期の人工知能科学者のほとんどは数学者と論理学者でした。コンピュータの誕生後、彼らはコンピュータと自らの研究を組み合わせ、人工知能の分野に参入しました。中国では、人工知能研究の第一歩を踏み出したのも数学者たちでした。 1979 年、機械証明における「ウー法」が世界的に普及したのも、ダートマス会議に匹敵するコンピュータ サイエンス サマー シンポジウムが開催されたのも、その背後には数学者がいた。中国の人工知能が世界に追いつき始めたのもこの年からだった。

「呉法」の創始者は数学者の呉文軍です。彼、王向昊、曽先昌は「機械証明の三英雄」として知られています。 1970年代後半、60歳近くになった呉文軍は、古代中国の数学の研究から始め、数学の機械化という新しい分野を開拓しました。彼は、コンピュータを使用して幾何学の定理を証明する「ウー法」を提案し、これは自動推論の分野における先駆的な研究であると考えられています。

1. 呉文軍は中国の人工知能の世界進出の扉を開いた

1979 年 1 月、プリンストン高等研究所の招待を受けて、数学者の呉文軍は 25,000 ドルをポケットに抱えて交換留学のためアメリカ行きの飛行機に乗りました。

彼に同行したのは数学者の陳景潤氏だった。二人は、中国と米国の正式な外交関係樹立後に米国で研究と訪問を行うよう招待された最初の科学者グループである。彼らは一定期間、プリンストン高等研究所で学び、交流する予定です。陳景潤氏の発表のテーマは当然「1+2」であり、呉文軍氏の発表の主な内容は、彼の古い専門分野である位相幾何学に加えて、中国古代の数学と数学の機械化の歴史に関するものでした。彼は持参した25,000ドルを使って数学的機械化の研究用のコンピューターを購入したいと考えていました。

1979年に呉文軍が中国科学院（CAS）から自然科学部門一等賞を受賞したとき、数学機械化はすでに彼の主な研究分野となっていました。この研究の方向性は世界的にも注目を集めています。呉文軍の研究方法は、機械定理証明の分野では「呉法」として知られています。中国最高の知能科学技術賞である「呉文軍人工知能科学技術賞」は、人工知能関連分野における中国人研究者としての呉文軍氏の功績を記念して同氏の名前がつけられたものである。

呉文軍氏は意図せずして、中国の人工知能研究が世界へ進出する扉を開いた。呉文軍は1974年頃から中国古代数学の歴史について研究を始めた。当時、中国科学院数学研究所（以下、「中国科学院数学研究所」という）の副所長である管昭之が呉文軍に中国古代数学の研究を依頼した。呉文軍は、古代中国の数学の伝統と古代ギリシャから受け継がれた現代西洋の数学の伝統との間の重要な違いをすぐに発見しました。彼は古代中国の算術を徹底的に分析し、多くの面で独自の洞察を展開しました。

1970年代に入ると、海外との学術交流が徐々に再開され始めました。 1975年、呉文軍は交換留学でフランスに行き、フランスの高等科学研究所で古代中国の数学思想に関する報告書を発表しました。この時、呉文君は日高の公式の古代の証明を復元し、古代中国の数学の「構成的」かつ「機械化」された特徴に注目しました。 1977 年の春節期間中、呉文軍は機械で証明された幾何学定理の方法の実現可能性を手計算で検証しましたが、この作業には 2 か月かかりました。

機械定理証明の元々のアイデアは、ゴットフリート・ヴィルヘルム・ライプニッツの微積分学とそこから発展した記号論理学から生まれました。その後、デイヴィト・ヒルベルトはこれを基にして、数学体系全体を厳密に公理化することを望み、1920年に「ヒルベルト・プラン」を立ち上げました。簡単に言えば、この計画が実現すれば、どんなに難しい数学的推測であっても、その推測が正しいかどうかを常に知ることができ、それを証明または反証できることになります。これは、ヒルベルトが「Wir müssen wissen, wir werden wissen」（我々は知らなければならない、我々は知るであろう）と言ったことの意味です。

しかし、その後まもなく、1931年にクルト・ゲーデルがゲーデルの不完全性定理を提唱し、ヒルベルトの形式主義的理想は完全に打ち砕かれました。しかし、何があっても、ゲーデルはこのドアを閉めたときに窓を残しました。フランスの天才数学者ジャック・エルブランの博士論文は、数理論理学の証明理論と再帰理論の基礎を築きました。ゲーデルの不完全性定理が提案された後、ヘルブラントは自分の論文をチェックし、「ゲーデルの結果と私の結果は矛盾していない」という一文を残し、ゲーデルに助言を求める手紙を書いた。ゲーデルはヘルブラントに返事を書いたが、ヘルブラントはその手紙を見ることなく亡くなっていた。彼はゲーデルの返答の2日後に登山中の事故で23歳で亡くなった。後に定理証明の分野で最高の賞もエルブラウンにちなんで名付けられ、呉文軍は1997年に自動推論における優れた業績に対して第4回エルブラウン賞を受賞した。

他の数学者もゲーデルの定理に付け加えた。ゲーデルが「一階の整数（算術）は決定不可能である」ことを証明した直後、アルフレッド・タルスキは「一階の実数（幾何学と代数）は決定可能である」ことを証明し、これも機械証明の基礎を築きました。

1936年、チューリングは重要な論文「計算可能数について、その実現問題への応用」の中でゲーデルの1931年の証明と計算上の限界を再検討し、万能算術に基づくゲーデルの形式言語を、現在チューリングマシンと呼ばれる単純な抽象装置に置き換え、すべての計算可能なプロセスがチューリングマシンでシミュレートできることを証明した。これは、コンピュータサイエンスと人工知能の重要な理論的基礎でもあります。人工知能の最も初期の学派である記号学派も、形式的な論理演算に基づいて拡張されました。

呉文軍に戻りましょう。 1970年代には、コンピューターを生産する北京ラジオ第一工場で働き、その頃からコンピューターや機械定理証明に触れ始めた。 「コンピューターの力をどのように活用し、それを自身の数学研究に応用するか」が呉文軍の関心事となった。その後、呉文軍は古代中国数学の歴史を研究し始め、古代中国数学の幾何学的代数的傾向とアルゴリズム的思考をまとめました。彼は古代中国の数学と西洋の数学の考え方の違いを発見した後、異なる方法を使って幾何学の定理を機械的に証明することに決めました。

当時、呉文軍は多くの外国の論文を読み、機械証明を完全に理解していました。当時、機械定理証明における最先端の研究は、数理論理学者の王浩によるものでした。西南学院大学数学科在学中、著名な哲学者であり「中国哲学の第一人者」である金月林に師事した。その後、アメリカのハーバード大学に留学し、著名な哲学者・論理学者ウィラード・フォン・クワイン（WVクワイン）の指導のもと、クワインが創始した形式公理体系を学び、博士号を取得しました。 1953年という早い時期から、王昊は機械を使って数学の定理を証明する可能性について考え始めていました。

1958 年、王浩は IBM 7041 コンピュータ上の命題論理プログラムを使用して、「数学原理」のすべての一階論理定理を証明しました。翌年、彼は命題論理定理200個すべての証明を完了した。王浩之の研究の重要性は、定理を証明するためにコンピューターを使用する可能性を示したことにある。 1977年に中国に帰国後、彼は我が国の科学技術の長期的な発展に影響を与えたいくつかのセミナーに参加し、中国科学院で6回の特別講演を行い、国内の機械実証研究に大きな影響を与えました。

話を元に戻すと、王昊が『数学原理』で以前に証明した命題論理定理と、呉文軍が達成しようとした幾何学定理の機械証明との間には、まだギャップが残っています。前者は記号論理要素が多く、後者は推論要素が多くなります。当時、海外では幾何学の定理を機械で証明する研究が数多く行われていましたが、すべて失敗に終わりました。

2. 古代中国の数学思想の機械化から「呉法」へ

呉文軍氏の意見では、失敗の経験も非常に重要であり、失敗によってどの道が塞がれているかがわかるという。デカルトの考えに触発され、彼は座標を導入して幾何学の問題を代数の問題に変換し、それを古代中国の数学的考えに従って機械化しました。呉文軍はデカルトの考えと古代中国の数学的考えを組み合わせ、一般的な問題を解決するための方法を提案しました。

すべての問題は数学の問題に変換でき、すべての数学の問題は代数の問題に変換でき、すべての代数の問題は連立方程式を解く問題に変換でき、連立方程式を解くすべての問題は単一変数の代数方程式を解く問題に変換できます。

古代中国の数学と現代の西洋の数学は、2つの異なる体系です。呉文軍は、現代数学における三角関数、微積分、因数分解法、高次方程式の解法などの「現代のツール」の助けを借りずに、当時の古代人の知識と習慣的な考え方に基づいて、『周比算経』と『九章算書』の「太陽高図」「大導関数による求一法」「平方根の増乗法」の証明方法を復元しました。彼は、古代中国の数学には独自の特徴があり、秦九紹の方法は構成的かつ機械化可能であり、高次代数方程式の数値解は小型の計算機を使用して得られると考えていた。当時は高性能な計算設備がなかったにもかかわらず、呉文軍が古代中国の数学の次元削減の考え方を研究に最大限活用できたことも称賛に値する。

この考えに基づいて呉文軍が証明した最初の定理はフォイエルバッハの定理であり、「三角形の 9 点円は、その内接円と 3 つの外接円に接する」ことを証明しました。これは平面幾何学における最も美しい定理の一つであり、呉文軍の美的センスがよく表れています。当時はコンピューターがなかったので、呉文軍は手作業で計算をしました。 「Wu メソッド」の特徴は、多数の多項式を生成することです。証明プロセスに関係する最大の多項式には、数百の項が含まれます。この計算は非常に難しく、どのステップでも間違いがあると、その後の計算が失敗します。 1977年の春節に、呉文軍は初めて手計算によって幾何学の定理の機械証明の方法を検証することに成功しました。その後、呉文軍は北京第一ラジオ工場で製造された万里の長城203でシムソンの定理を証明した。

呉文軍は1977年に『サイエンス中国』に関連研究論文「初等幾何学の決定問題と機械化証明」を発表し、その論文を王昊に送った。王昊氏は呉文軍氏の研究を高く評価し、返信で呉文軍氏に既存の代数パッケージを使用し、呉氏の方法をコンピューターに実装することを検討するよう提案した。王昊は、当時中国と米国のトップ学者が使用していたコンピュータの違いに気づいていなかった。Great Wall 203 は機械語を使用できたが、異なるコンピュータの命令システムは汎用的ではなく、既存の代数パッケージを使用しても機能しなかった。そのため、後に呉文軍は中国科学院数学研究所を訪れた外国人からもらった小型計算機を借りて、与えられた命題を代数形式に変換し、秦九紹の方法を使って高次方程式の解を計算した。

呉文軍の幾何学定理の機械証明に関する研究は、関昭志から強力な支援を受けました。関昭之はかつてフランスに留学し、中国科学者協会フランス支部の創設者の一人でした。彼は優れた愛国心ある知識人の集団を団結させ、呉文軍もその一人であった。当時、呉文軍が勤務していた中国科学院数学研究所内の人間関係は複雑だった。ある派閥は、機械による証明を行うことは「異端」であると信じ、彼が位相幾何学の研究に従事し続けることを期待していました。位相幾何学と関数解析から制御理論に転向した管昭志は、特に彼を支援し理解を示し、呉文軍がやりたいことは何でもできると言った。その後、1979年に管昭之が自身の研究所を設立し、中国科学院システム科学研究所を設立すると、呉文軍も管昭之に続いて中国科学院システム科学研究所に加わった（図1-1）。

1980年代初頭の中国科学院システム科学研究所の元オフィスビル（現在の栄科ビル）（左から：徐国之、呉文軍、インドの学者、管昭之）

より複雑な定理を証明するには、より優れたマシンが必要です。当時中国科学院音響研究所所長であった王徳昭院士が呉文軍に指導を与えた。彼は、中国科学院副院長で党委員会書記の李昌がいつどこに現れるかを呉文軍に伝え、呉文軍は本当に李昌をそこに見た。李昌は非常に心が広い人でした。 1950年代にハルビン工業大学（以下、「HIT」と略す）の学長を務めていた間、彼はHITを国内の一流大学に成長させた。 1954年に特定された国内の主要6大学のうち、ハルビン工業大学は北京に所在しない唯一の大学である。李昌氏も呉文軍氏の活動に多大な支援を与えた。呉文軍が米国でコンピューターを購入するために使用した2万5000ドルの外貨は、李昌の特別承認を受けたものだった。このコンピューターによって、多くの定理がすぐに証明されました。

1970 年代は機械による定理証明の黄金時代でもありました。 1976年、2人のアメリカ人数学者が高速コンピュータを使用し、1,200時間の計算時間を費やして四色定理を証明し、100年以上も数学者が解けなかった問題を解決しました。既約集合と必然集合は有限なので、四色定理は証明できます。四色定理の「地図の色付け」問題は、地図の数が無限にあるように見えますが、実際には2,000以上の基本図形にまで減らすことができ、あとはコンピュータの計算能力を使って総当たり方式で一つずつ証明することができます。例えで言えば、このアプローチはルービックキューブを解くようなものです。つまり、一度分解して再び組み立てるのです。エレガントではありませんが、機能します。 GPT-3 は「多大な努力で素晴らしい成果を上げる」と言われていますが、実は、4 色定理の証明が「多大な努力で素晴らしい成果を上げる」ことの起源です。

しかし、コンピュータの計算能力を使って定理を力ずくで証明するというこのアプローチは、一般化できません。定理証明の最初のステップ、つまり定理の形式化には、完全かつ厳密な記述が必要です。これに関して、ある数学者に関するちょっとした話があります。天文学者、物理学者、数学者が列車でスコットランドへ旅行していました。彼らは窓の外に黒い羊を見つけました。そして天文学者はため息をつき始めました。「なぜスコットランドの羊はみんな黒いのだろう？」物理学者は訂正した。「スコットランドには黒い羊もいると言うべきだ。」最も厳密な表現は数学者によるものです。「スコットランドには少なくとも天と地が一つずつあり、少なくとも羊が一匹いて、その羊の少なくとも片側は黒い。」数学の問題は「これも証明する必要があるか？」と「これも証明できるか？」の 2 つのカテゴリに分けられるというジョークもあります。このことから、証明が他の数学者に認められることがいかに難しいかが分かります。同様に、対話型定理証明器で定理を形式化するには、推論の「自動化」を完了するためのすべての技術的詳細を記入し、最終的に定理の証明を実行可能だが計算集約的なソリューションに置き換える必要があります。言い換えれば、この方法は依然として数学者の定理の理解に依存しており、「1 つの理論、1 つの証明」しか達成できず、これはコンピュータ支援による定理の証明としか見なすことができません。

そのため、四色定理がコンピュータによって証明された後、王昊を含む一群の論理学者は、四色定理は証明されたのかという異なる意見を表明した。このタイプの証明は伝統的な証明と見なされ、コンピュータは補助的な計算の役割のみを果たします。ジョルジュ・ゴンティエが、論理的推論のすべてのステップをコンピュータで実行し、四色定理の完全なコンピュータ化された証明を完了したのは、2005 年になってからでした。人々はコンピュータを使って何百もの数学の定理を証明してきましたが、これらの定理のほとんどはすでに知られており、「機械知能」はまだ数学に実質的な貢献をしていません。

機械による定理の証明はアルゴリズムに依存します。初期の段階では、研究者はすべての問題を解決するスーパーアルゴリズムを見つけようと試みることが多かったが、呉文軍は古代中国の数学の考え方を幾何学定理の機械証明の分野に応用し、「1つのタイプ、1つの証明」を実現した。この点については王昊氏も同意しており、自身の初期の研究と呉文軍氏が使用した方法には共通点があると考えていた。つまり、まず比較的制御可能なサブフィールドを見つけ、次にこのサブフィールドの特性に基づいて最も効果的なアルゴリズムを見つけるという点だ。 1979年に呉文軍が米国を訪問した際、彼はわざわざロックフェラー大学を訪れ、王昊を訪ねた。彼の研究が機械定理コミュニティで高く評価されたのも、王昊氏の強力な推薦によるものでした。

「ウー法」は実際に普及し、1980年代にウー・ウェンジュンの機械定理証明講座を受講した米国留学中の中国人学生、周先青のおかげで機械定理証明は最初のブレークスルーを達成しました。周先青さんはもともと呉文軍さんの機械証明プログラムの大学院課程に応募したかったのですが、微分幾何学が自分の弱点だと思い、入学試験に失敗するのではないかと心配していました。最終的に、彼は中国科学技術大学（以下、「USTC」という）に入学し、その後、中国科学院計算技術研究所で研修を受け、そこで呉文軍の幾何学証明講座を聴講した。

1981年、周先卿はテキサス大学オースティン校に留学した。当時、テキサス大学オースティン校は定理証明の王者と考えられていました。同校の2つの研究グループが定理証明の最高賞であるエルブラン賞を受賞した。周先青はロバート・ボイヤーに呉文軍の研究について話したが、ボイヤーはそれを非常に興味深く感じ、質問を続けた。しかし周先青はそれが幾何学を代数に変換するものであることしか知らず、具体的な詳細を説明することはできなかった。

その後、ウッディ・ブレッドソーは周先青ともう一人の学生である王鉄成に情報収集を依頼した。周先青の博士論文は呉の方法の実践だった。ウー・ウェンジュンはすぐに、彼の署名が入った2つの記事をブレッドソーに送った。その後の2年間で、この2つの論文はテキサス大学オースティン校によって100回近くコピーされ、世界中に送られ、ウーの手法は広く知られるようになりました。

1983年、米国コロラド州で全米定理機械証明学術会議が開催されました。周先卿氏は会議で「呉氏の方法を用いた幾何学定理の証明」と題する報告を行った。周先卿氏が開発した汎用プログラムは、モーラーの定理、シムソンの定理、フォイエルバッハの九点円定理、デザルグの定理など、より難しい定理の証明を含む、130以上の幾何学定理を自動的に証明することができます。その後、この会議の議事録は1984年にアメリカの「現代数学」シリーズの第29巻として正式に出版され、呉文軍が送った2つの関連論文も収録されました。

1986 年 6 月、チューリング賞受賞者のジョン・ホップクロフトらが自動幾何学的推論に関するセミナーを開催しました。セミナーのレポートの一部は、1988 年 12 月の「人工知能」特別号に掲載されました。特集号の巻頭記事では、呉文軍が提唱する新しい代数幾何学の手法を具体的に紹介し、この手法は幾何学的推論の進歩に大きく貢献しただけでなく、人工知能の3大応用問題（ロボット工学と動作計画、マシンビジョン、ソリッドモデリング）においても重要な応用価値を持っているとしている（図1-2）。ホップクロフト氏はそれ以来、多くの中国の大学と緊密に協力し、上海交通大学、北京大学、香港中文大学（深圳）の研究機関を率いてきました。おそらく呉文軍と呉法芳が彼の中国コンプレックスの始まりだったのだろう。

1988年の人工知能特集号の冒頭にあるウーの手法の概要

——インタラクションの問題——

中国における人工知能の発展についてご存知ですか？