機械定理証明の元のアイデアはゴットフリート ヴィルヘルム ライプニッツの微積分推論に由来し、その後記号論理から発展しました。その後、デヴィッド・ヒルベルト（デイヴィッド・ヒルベルト）はこれに基づいて1920年に「ヒルベルト・プロジェクト」を立ち上げ、数学体系全体を厳密に公理化することを望んだ。簡単に言うと、この計画が実現すれば、どんなに難しい数学的予想であっても、その予想が正しいかどうかを常に知り、それを証明または否定できることを意味します。これは、ヒルベルトが「Wir müssen wissen, wir werden wissen」（我々は知らなければならない、我々は知らなければならない）と言ったことの意味です。
中国の人工知能の始まりはこの数学者と密接に関係している
出典: チューリングコミュニティ
著者: リン・ジュンセン・フォン
1979 年は中国にとって重要な年でした。この年は多くの大きな出来事が起こり、中国の政治、経済、科学技術、文化などの分野における重要な転換点、中国現代史における重要な時代の区切りの一つとみなされている。 1979 年に開かれた壮大な新時代と比較すると、1979 年に中国で人工知能 (AI) 研究が始まったことは、歴史の流れの中では目立たない波としか見なされませんが、これは中国の人工知能の歴史において画期的なことです。イベント。
人工知能の最も初期の学派は象徴学派でした。初期の人工知能科学者のほとんどは数学者や論理学者でした。彼らはコンピューターの誕生後、コンピューターと独自の研究を組み合わせて、人工知能の分野に参入しました。中国でも、人工知能研究の最初のページを開いたのは数学者でした。 1979 年に機械証明の「呉法」が世界に広まったときも、ダートマス会議に匹敵するコンピュータ サイエンス サマー シンポジウムの開催も、その背後には数学者がいた。中国の人工知能が世界に追いつき始めたのもこの年からです。
「呉法」の提唱者は、ほかならぬ数学者の呉文君である。王香豪、曽献昌とともに「機証の三巨匠」と呼ばれる。 1970 年代後半、60 歳近くになった呉文君は、古代中国数学の研究から出発し、数学的機械化という新しい分野を創造し、幾何学定理をコンピュータで証明する「呉法」を提案しました。自動推論の分野における先駆的な研究。
1. 呉文君は中国の人工知能が世界へ進出する扉を開いた
1979年1月、数学者のウー・ウェンジュンはプリンストン高等研究所の招待で、ポケットに2万5000ドルを持って米国行きの交換便に乗った。
彼には数学者の陳京潤氏が同行した。両氏は中米国交樹立後、米国への留学・訪問に招待された最初の科学者で、プリンストン高等研究所で一定期間研究・交流する予定。陳京潤氏の交流の話題は当然「1+2」であり、今回の呉文君氏の交流の主な内容は、トポロジーという彼の古い専門職に加えて、むしろ古代中国の数学と数学的機械化の歴史に関するものである。彼が持ってきた25,000元を使って、数学的機械化の研究のためにコンピューターを購入しました。
1979 年に呉文軍が中国科学院 (以下、「中国科学院」という) から自然科学部門の一等賞を受賞したとき、数学的機械化が彼の主な研究方向となっていました。この研究方向性は世界からも注目を集めており、呉文君の研究手法は機械定理証明の分野では「呉法」と呼ばれており、中国の知能科学技術の最高賞「呉文君人工知能科学技術賞」を受賞している。呉文軍の名前は、AI関連分野における中国研究者の功績として呉文軍を記念して付けられました。
ウー・ウェンジュン氏は、図らずも中国の人工知能研究が世界に進出する扉を開いた。呉文君による古代中国数学史の研究は 1974 年頃から始まりました。当時、中国科学院数学研究所（以下、「中国科学院数学研究所」）の副所長である関昭志は、呉文君に古代中国数学の研究を依頼した。呉文君は、古代中国の数学的伝統と、古代ギリシャから受け継がれた現代西洋数学の伝統との重要な違いをすぐに発見し、古代中国の算術を徹底的に分析し、多くの側面で独自の洞察を開発しました。
1970年代に入ると、海外との学術交流が徐々に回復し始めた。 1975年、呉文君は交換留学のためフランスに行き、フランス高等科学研究所で古代中国の数学的思想について報告した。この時、呉文君はリガオの公式の古代の証明を復元し、古代中国の数学の「構造」と「機械的」特徴に気づきました。 1977 年の春節に、呉文君は手計算による幾何定理機械証明法の実現可能性を検証し、そのプロセスは 2 か月間続きました。
機械定理証明の元のアイデアはゴットフリート ヴィルヘルム ライプニッツの微積分推論に由来し、その後記号論理から発展しました。その後、デヴィッド・ヒルベルト（デイヴィッド・ヒルベルト）はこれに基づいて1920年に「ヒルベルト・プロジェクト」を立ち上げ、数学体系全体を厳密に公理化することを望んだ。簡単に言うと、この計画が実現すれば、どんなに難しい数学的予想であっても、その予想が正しいかどうかを常に知り、それを証明または否定できることを意味します。これは、ヒルベルトが「Wir müssen wissen, wir werden wissen」（我々は知らなければならない、我々は知らなければならない）と言ったことの意味です。
しかし、その直後の 1931 年に、クルト ゲーデルはゲーデルの不完全性定理を提案し、ヒルベルトの形式主義の理想を打ち砕きました。しかしとにかく、ゲーデルがドアを閉めたとき、彼はまだ窓を残しました。フランスの天才数学者ジャック・エルブランドの博士論文は、数理論理学の証明理論と再帰理論の基礎を築きましたが、ゲーデルの不完全性定理が提案された後、ヘルブランドは彼の論文をチェックして去ったのです。ゲーデルにアドバイスを求める手紙を書きました。ゲーデルはエルブランに返信したが、エルブランは手紙を待てず、ゲーデルが返信した２日後に登山中の事故で23歳で亡くなった。その後、定理証明の分野における最高賞もエル・ブラウンにちなんで命名され、1997 年にウー・ウェンジュンは自動推論における顕著な業績に対して第 4 回エル・ブラウン賞を受賞しました。
他の数学者がゲーデルの定理を補足しました。ゲーデルが「一次整数 (算術) は決定不可能である」ことを証明した直後に、アルフレッド タルスキーは「一階実数 (幾何および代数) は決定可能である」ことを証明しました。これは機械証明の基礎も築きました。
1936 年、チューリングは、ゲーデルの 1931 年の証明と計算制限に関する重要な論文「計算可能な数について、エンシャイドゥング問題への応用」(計算可能な数について、エンシャイドゥング問題への応用) を発表しました。その結果、議論は次のように練り直されました。そして、一般的な算術に基づくゲーデルの形式言語は、現在チューリング マシンと呼ばれる単純な形式の抽象装置に置き換えられ、すべての計算可能なプロセスはチューリング マシンでシミュレートできることが証明されました。これは、コンピューターサイエンスと人工知能の重要な理論的基礎でもあります。人工知能の最も初期の学派である記号学派も、形式論理演算に基づいて拡張されました。
ウー・ウェンジュンの話に戻りますが、彼は 1970 年代にコンピューターを生産する北京ラジオ第一工場で働いており、その頃からコンピューターと機械定理の証明に触れ始めました。 「コンピュータの能力を最大限に活用し、それを自分の数学研究にどのように応用するか」が、ウー・ウェンジュン氏の関心となっている。その後、呉文君は古代中国数学の歴史を研究し始め、古代中国数学の幾何代数的傾向とアルゴリズム的思考を要約しました。古代中国の数学と西洋数学の考え方の違いを発見した後、彼は別の方法を使って幾何学定理の機械証明を行うことにしました。
当時、呉文君は多くの外国の論文を読み、機械証明を完全に理解していました。当時、機械定理の証明に関する最先端の研究は、数理論理学者の王昊氏によるもので、彼は南西連合大学数学科在学中、有名な哲学者で「中国哲学の第一人者」金氏に師事しました。有名な哲学者で論理学者のウィラード・フォン・クイン（WV クワイン）は、クワインが創設した形式公理系を研究し、博士号を取得しました。 1953 年の時点で、Wang Hao はすでに数学の定理を機械で証明する可能性について考え始めていました。
1958 年、Wang Hao は IBM 7041 コンピュータの命題論理プログラムを使用して、『数学原理』のすべての一次論理定理を証明し、翌年には 200 個の命題論理定理すべての証明を完了しました。 Wang Haozhi 氏の研究の重要性は、定理を証明するためにコンピューターを使用する可能性を発表したことにあります。 1977 年に中国に帰国すると、我が国の科学技術の長期的発展に影響を与えるいくつかのシンポジウムに参加し、中国科学院で 6 回の特別講演を行い、国内の機械実証研究に大きな影響を与えました。
さらに近いところでは、Wang Hao 氏の「数学原理」における命題論理定理の以前の証明と、呉文君氏が達成しようとしている幾何定理の機械的証明の間には、まだギャップがあります。前者にはより多くの記号論理要素があり、後者にはより多くの記号論理要素が含まれています。推論の要素。当時、海外では幾何定理の機械証明に関する研究が数多く行われていましたが、いずれも失敗に終わりました。
第二に、古代中国の数学的思考の機械化から「呉法」へ
ウー・ウェンジュン氏の見解では、失敗の経験も非常に重要であり、それはどの道がうまくいかないかを教えてくれます。デカルトの思想に触発されて、彼は座標を導入することで幾何学的問題を代数問題に変換し、古代中国の数学的思考に従って機械化しました。ウー・ウェンジュンは、デカルトの思想と古代中国の数学的思想を組み合わせて、一般的な問題を解決するルートを提案しました。
すべての問題は数学的問題に変換でき、すべての数学的問題は代数問題に変換でき、すべての代数問題は方程式を解く問題に変換でき、方程式を解くすべての問題は単一変数の代数方程式問題を解くことができます。
古代中国の数学と西洋の現代数学は 2 つの異なる体系です。呉文君は、現代数学における三角関数、微積分、因数分解、高次方程式の解などの「現代の道具」を使わずに、当時の古代人の知識と習慣的な思考と推論に従って『周碧算経』を復元した。 『書書九章』の「李高土書」、「大燕秋意書」、「曾城開方書」の証明方法。彼は、古代中国の数学には独自の特徴があり、秦九韶の方法には建設と機械化の特徴があり、高次の代数方程式の数値解は小型の電卓で得られると考えています。当時、高性能の計算機がなかった中で、呉文君は古代中国の数学的考え方を駆使して次元削減の研究を行うことができ、これも賞賛に値します。
この考え方に従って呉文君が証明した最初の定理はフォイエルバッハの定理で、「三角形の9点の円は内接円と3つの外接円に接する」ことを証明した。これは平面幾何学の最も美しい定理の 1 つであり、呉文君の美学に見ることができます。当時はコンピューターがなかったため、呉文君は手計算で計算しました。 「Wu 法」の特徴の 1 つは、大量の多項式が生成されることです。証明プロセスに含まれる最大の多項式には数百もの項目があります。この計算は非常に難しく、1 つのステップでエラーが発生すると、その後の計算に影響を及ぼします。失敗。 1977 年の春節に、呉文軍は手計算による幾何定理の機械証明方法の検証に初めて成功し、その後、北京ラジオ第一工場で製造された万里の長城 203 上でシムソンの定理を証明しました。
呉文君は 1977 年に関連研究論文「初等幾何学決定問題と機械化証明」を『中国科学』に発表し、その論文を王皓に送った。 Wang Hao は Wu Wenjun の研究を高く評価し、Wu Wenjun が既存の代数パッケージを使用し、Wu の手法をコンピュータで実装することを検討するよう提案する返事を書きました。王昊氏は、この時点では中国と米国の一流の学者が使用するコンピューターの違いを理解していなかった。万里の長城203は機械語を使用できるが、異なるコンピューターの命令システムは普遍的ではなく、実現不可能だった。既存の代数パッケージを使用します。そこで、後に呉文君は、中国科学院数学研究所を訪れた外国人からの贈り物として、中国科学院数学研究所から小型の電卓を借りて、与えられた命題を代数形式に変換した。そして、Qin Jiushao の方法を使用して高次の方程式を計算しました。
Wu Wenjun の幾何定理の機械証明に関する研究は、Guan Zhaozhi によって強力にサポートされました。関昭志はフランスに留学し、中国科学者協会フランス支部の創設者の一人であり、傑出した愛国的知識人のグループをまとめ、呉文君もその一人でした。当時、呉文君が勤務していた中国科学院数学研究所は複雑な関係にあり、ある派閥は機械証明を行うことは「反逆的」であると信じ、トポロジーの研究を続けることを望んでいたが、関昭志氏はトポロジーと機能解析から制御理論に転向した呉文君は、特に協力的で理解してくれました。その後、1979 年に関昭志が中国科学院システム科学研究所を設立すると、呉文君も関昭に従い中国科学院システム科学研究所に着任しました（図 1-1）。
より複雑な定理を証明するには、より優れたマシンが必要です。当時中国科学院音響研究所所長だった学者の王徳昭氏は呉文軍氏にアドバイスを与えた。彼は呉文軍に、党グループ書記で中国科学院副院長の李昌がいつどこに現れるかを告げたが、呉文軍は本当に彼を捕まえた。李昌氏は非常にオープンな性格で、1950年代にハルビン工業大学（以下、HIT）の学長を務めたとき、HITを国内一流の大学に育て上げました。 1954 年に指定された 6 つの国家重点大学のうち、北京にないのはハルビン工業大学だけです。李昌は呉文軍の活動にも多大な支援をしており、呉文軍が米国でコンピューターを購入するための25,000米ドルの外貨交換は李昌から特別に承認された。このコンピュータを使用すると、多くの定理がすぐに証明されました。
1970 年代は機械定理証明の黄金時代でもありました。 1976年、2人のアメリカ人数学者が1200時間の計算時間を持つ高速電子計算機を使って四色定理を証明し、数学者が100年以上解決できなかった難問を解決した。 4 色定理が証明できる理由は、既約集合と不可避集合が有限であるためです。4 色定理の「マップの色付け」問題は、無限に多くのマップがあるように見えますが、実際にはそれ以上のものに帰することができます。 2000種類の基本的な形状をコンピュータの計算能力を使って総当たりで一つ一つ証明していきます。比喩的に言えば、このアプローチはルービック キューブを解くようなもので、キューブを分解して元に戻すようなもので、洗練されていませんが効果的です。今ではGPT-3を「苦労して奇跡を起こす」と言いますが、実は四色定理の証明は「苦労して奇跡を起こす」の元祖なのです。
ただし、コンピューターの計算能力を使用して力ずくで定理の証明を行うこの手法は一般化できません。定理証明の最初のステップである定理の定式化には、完全かつ厳密な定式化が必要です。この点に関して、ある数学者についてのちょっとした話があります。天文学者、物理学者、数学者が列車でスコットランドへ旅行しました。窓の外に黒い羊が見えました。天文学者はため息をつきました。「なぜスコットランドの羊はみんな黒いのでしょう？」と物理学者は訂正しました。 「スコットランドの羊は黒いです。」そして最も厳密な表現は数学者によるものです：「スコットランドには少なくとも 1 つの世界が存在し、少なくとも 1 匹の羊がいます。そしてこの羊は少なくとも片面が黒いです。」もう 1 つのジョークがあります。は、数学の問題は「これも証明する必要がある？」と「これも証明できる？」という２つのカテゴリーに分けられると述べました。このことから、証明が他の数学者に認められることがいかに難しいかがわかります。同様に、インタラクティブな定理証明器で定理を形式化するには、推論の「自動化」を完了するために技術的な詳細をすべて入力し、最終的に定理を実行可能だが計算量が多い問題解決のアイデアに置き換える必要があります。 。言い換えれば、この方法は依然として数学者の定理理解に依存しており、コンピューターを利用した定理の証明としか考えられない「一理論一証明」しか達成できません。
したがって、4 色定理がコンピュータによって証明された後、Wang Hao を含む論理学者のグループはさまざまな意見を提出しました。「4 色定理は証明されたのか?」この種の証明方法は伝統的な証明とみなされ、コンピュータは補助的な計算の役割を果たすだけです。ジョルジュ ゴンティエが 4 色定理のコンピュータによる証明を完全に完了したのは 2005 年になってからであり、その論理的導出のすべてのステップはコンピュータによって完了されました。現在、人々はコンピューターを使って何百もの数学の定理を証明していますが、これらの定理のほとんどは既知のものであり、「機械知能」はまだ数学に本格的な貢献をしていません。
機械定理の証明はアルゴリズムに依存します。初期段階では、研究者はすべての問題を解決するスーパーアルゴリズムを見つけようとすることがよくありましたが、ウー・ウェンジュンは古代中国の数学的アイデアを幾何学定理の機械証明の分野に適用し、「1種類1証明」を達成しました。この点は Wang Hao 氏も同意しており、彼は自分の初期の研究が、まず比較的制御可能なサブフィールドを見つけてから、その特性に応じて最も効果的なアルゴリズムを見つけるという、Wu Wenjun が使用した方法と共通点があると信じていました。サブフィールド。呉文君は1979年に米国を訪問した際、ロックフェラー大学にも行き、王皓を訪問し、彼の業績は機械定理の分野で高く評価され、王皓の強い推薦と一定の関係があった。
「呉法」は実際に普及し、1980 年代に機械定理証明の最初のブレークスルーをもたらしました。これは、呉文君の機械定理証明コースを聞いた米国の留学生、周賢青のおかげです。周仙青さんは当初、機械証明分野で呉文君の大学院の学位を取得したいと考えていましたが、微分幾何学が苦手だと考えていたため、試験に合格できないのではないかと心配し、最終的に大学に入学しました。中国科学技術大学（以下、「中国科学技術大学」という）の博士号を取得し、その後ダイ・ペイとして中国科学院計算技術研究所に赴任しました。この点で、私は呉文君の幾何学的設計を監査しました。証明コース。
1981年、周仙青はテキサス大学オースティン校に留学したが、当時テキサス大学オースティン校は定理証明の王として知られていた。周仙青はロバート・ボイヤーに呉文君の研究について話しましたが、ボイヤーはそれがとても新鮮だと思ったので質問を続けましたが、周仙青はそれが幾何学を代数学に変換していることだけを知っていて、具体的な詳細を説明することができませんでした。
その後、ウディ・ブレッドソー氏は周仙青氏ともう一人の学生である王鉄成氏にデータ収集を依頼し、周仙青氏の博士論文は呉氏の手法を実現したものであった。ウー・ウェンジュンはすぐに2つの論文を送り、両方ともブレッドソーに署名した。次の 2 年間で、これら 2 つの論文はテキサス大学オースティン校によってほぼ 100 回コピーされ、世界中に送信され、ウーのメソッドは広く知られるようになりました。
1983年、アメリカのコロラド州で機械による定理の証明に関する全国学術会議が開催され、周賢青は「呉法を用いた幾何定理の証明」と題する報告を行った。 Zhou Xianqing が開発した一般的なプログラムは、モーラーの定理、シムソンの定理、フォイエルバッハの九点円定理、デザルグの定理などのより難しい定理の証明を含む、130 を超える幾何定理を自動的に証明できます。その後、この会議の論文集は1984年に『現代数学』シリーズ第29巻として米国で正式に出版され、呉文君から送られた関連論文2編も収録された。
1986年6月、チューリング賞受賞者のジョン・ホップクロフト（John Hopcroft）らが自動幾何学的推論に関するセミナーを開催し、そのセミナーの報告の一部が『インテリジェンス』特集号の『人工知能』の紹介記事に掲載されました。特別版では、呉文君が提案した代数幾何学の新しい方法を特別に紹介しており、ビジョン、ソリッドモデリングなどにも重要な応用価値があります(図1-2)。それ以来、ホップクロフト氏は中国の多くの大学と緊密に連携しており、上海交通大学、北京大学、香港中文大学（深セン）に彼が率いる研究機関を持っています。彼の中国語コンプレックス。