弊社は2010年に少年プログラマー制度を導入し、22歳以下の才能あふれるプログラマーにマシンと給料を与え、あとは好きにしてなさい、という形態を採用しています。

　過去にこの少年プログラマー制度から生まれたenchant.jsは今や広く世界的に使われるフレームワークとなり、この制度に応募してきた少年のうち何人かはUEIの正社員として、若くして一翼を担うリーダーとして活躍しています。

　この制度の変わったところは、基本的に若くて才能があれば資源と時間は渡すが、特に仕事は頼まないということです。

　少年というのはただそれだけで、目覚ましい成果を上げることがあるのです。
　もちろん全員が全員、目覚ましい成果を上げるわけではありませんが、そのうちの何人かは本当に素晴らしい成果を挙げて今日の会社の根源的な価値を生み出していることは疑いようもありません。

　その中の一人に、とても変わった子がいて、最初に彼が来たのは高校生の頃だったのですが、その頃から定理証明支援系言語という、非常に特殊な分野のプログラミング言語に興味を持っていて、大学に進学し、博士課程に進学したあとも、ときどき会社に遊びに来ては、彼の最新の研究成果を教えてくれるのです。

　彼は定理証明支援系言語、そして自動証明器のエキスパートで、コンピュータを使って様々な数学的証明を行ってきました。

　久しぶりに聞いた彼の話は、以前よりずっとわかりやすくなっており、彼の成長も感じられて大変感慨深い体験だったのですが、同時にそれまで遠巻きにしか見ていなかった定理証明支援系言語、そして自動証明器というものが、実はディープラーニングと真逆の方向性を指向していることに気づいて俄然興味が湧いてきました。

　ディープラーニングを始めとする機械学習の場合、基本的には問題がどのようなものであるか、特徴量はどのようなものであるかということを最初からあまり規定しません。

　それを先に規定してしまうと、うまくいかないからです。
　データはぼんやり扱って、ぼんやり学習させると、全体としてはなんとなく上手くいく、その上手くいく確率が98%くらいまで行けば、それはそれでいいじゃないか、というのが機械学習の基本的スタンスです。

　しかし98%上手くいくというものは、確実に2%間違えるものということです。
　この性質は、機械学習を実用的に扱おうとすると障害になります。

　通常、機械や部品は与えられた条件下では100%に限りなく近い再現性を必要とされます。
　2%も間違うというのは100回に二回、100秒間に2杪、100日間でまるまる2日は確実に間違えるということですから、これでは使えません。しかし人間だって、3カ月一度もミスを侵さないなんてことはないわけですから、人間と同等の間違い率なら許そうよ、というのが最近の風潮です。

　ところが機械はそもそも人間以上の働きを期待されて作られます。
　その最たるものがコンピュータの計算です。

　人間には到底不可能な大量の計算を瞬時にこなすからこそ、コンピュータは重宝されているのです。
　そのコンピュータが、人間並みの判断力を持つようになったからといって、なにが嬉しいのだろう?というのが大方の見方です。

　しかし、世界は予想以上に早く進歩しています。

　たとえばほんの数ヶ月前、早稲田大学で開発された、白黒からカラーに変換するニューラルネットワークはこんな感じでした。

出典:http://hi.cs.waseda.ac.jp/~iizuka/projects/colorization/ja/

　白黒写真の持つ、局所的な特徴と、広域的な特徴をそれぞれ別のネットワークに学習させ、最後に統合するというやや複雑な方式です。やろうとしていることを考えると、この構造は理にかなっています。

　しかし、同じことをもっと単純なニューラルネットワークでもできることがわかっています。

http://richzhang.github.io/colorization/

　筆者はこの２つの結果を見たとき、「こんなに単純に白黒からカラー写真に変換できるのならば、理論上、なんだって変換できるのではないか」と思いました。

　しかし筆者がそんなことを妄想している間に、実際にそれを作ってしまった人たちが居ます。

出典:https://arxiv.org/pdf/1611.07004v1.pdf

　「pix2pix」は、敵対的生成学習によって２つの画像のペアを学習させ、学習後には任意の画像からもう一方のペアを自動生成するという技術です。

　たとえば、航空写真と地図の組み合わせを学習させると、航空写真から自動的に地図を生成したり、また逆に地図から航空写真を生成したりといったことができます。

　また、昼間の写真と同じ場所から撮影した夜景の写真のペアを学習させると、昼間の写真から自動的に夜景を生成することができます。

　信じられないかもしれません。
　こんなことができるのですから、当然、白黒画像からカラー画像を生成することもできます。

　さらに凄いことが出来ます。

　カバンの輪郭とカバンの写真のペアを学習させると、カバンの輪郭だけから、それっぽいカバンの写真を生成することができます。

　建物の写真と、その建物のどの部分が窓でどの部分が壁で、どの部分が扉なのか、という画像情報(ラベル情報)のペアを学習させると、ラベル情報を与えるだけで建物の写真が生成されます。

　そして一番驚くべきことは、これまで、白黒からカラー、縮小された画像から拡大された画像など、画像処理をするときにはそれぞれ専用のニューラルネットワークを作っていました。

　ところが、pix2pixは、およそ画像同士のペアであれば、どうやら、なんであろうと学習することができるようなのです。

　この成果は控えめに言っても驚異的です。
　今後の画像生成系ニューラルネットワークは、このpix2pixのような方式を基準として、細かな改良を加えていくことになるでしょう。ある意味で画像学習および生成というタスクに関してはpix2pixは非常に広範囲な汎用性を持っていることになるからです。

　さて、とはいっても、ニューラルネットワークの世界は「正解でなくても許される」ということが大前提です。

　戒めしたpix2pixの出力結果(Output)も、本当の正解(Ground Truth)とは違います。
　でも興味深いのは、Ground Truthに比べると、AIからの出力結果(output)のほうがより自然に見えることもあるということです。

　特にカバンの場合は、Ground Truthでは奇抜すぎる色合いになっていたとしても、AIからの出力結果ではわりと無難で落ち着いた質感になっています。「こういうカバンがあってもいいよね」というレベルの出力です。

　一方で、Coqによる自動証明器が目指すものは、完全な数学的証明をプログラミングだけでやることです。

自動証明器は、人間の理性の精緻ともいうべき、数学的真理をコンピュータの支援によって成し遂げるという試みです。

　しかしどうやら、まだまだ完全に自動的になんでもかんでも証明するということはできず、コンピュータによる自動証明器はあくまでも「支援」に留まっているそうです。

　数学が扱おうとする論理体系は、人間が理屈に理屈を積み重ね、無駄という無駄を全て削ぎ落とした、透明で純粋な結晶体です。

　しかも面白いのは、それが透明で純粋で完全無欠であることが分かっているものの、それでもなお、その美しくまばゆく光る究極の論理体系の全貌を見た人は居ないということです。

　数学には未だ数多くの謎があり、その謎を追求することこそが真理の追求であると考える人達が居ます。

　しかし数学もかなり高度になってくると、人間の頭だけでは証明することが物理的に困難になってきます。

　20世紀後半から、数学的定理の証明にコンピュータの支援を要する場合があることが明らかになってきました。たとえばグラフ理論における四色問題です。世界中の数学者を百年以上悩ませ続けたこの問題の証明には、コンピュータが用いられました。

　数学の証明ではしばしば重要なキーを握る「場合分け」が、人間には処理することが不可能なほど膨大になる可能性があり、そうした場合にプログラムによる検証が効果的であることがこのときわかったのです。

　ディープラーニングは生物の神経細胞の構造を真似することで知能を獲得しようとしています。
　しかし一方で、数学者たちはコンピュータが機械であるという性質を利用して、自分たちの迫りたい数学的真理の高みを目指しています。

　同じ知性や知能に対する真摯な探究心であるというのに、アプローチが真逆であることに驚きます。

　今は機械学習の進歩が目覚ましいので注目を集めてはいますが、最終的に定理証明支援系言語やなんらかの数学的証明のような、純粋な論理体系と機械学習による知能が融合したとき、人工知能は真の人工知能になるのかもしれません。

　熱っぽく証明を語る若者の姿を見て、なんとか彼の言ってる内容の1/100でも理解しようと唸った朝でした。そして、会社の事業には全く関係ないことを熱っぽく語る人が身近に居てよかったと感謝する瞬間でもあります。そうでもなければ筆者にとって一生縁のない世界だったかもしれないのです。そして、こういう話はとても、想像力を掻き立ててくれます。彼と出会えて良かった、そう思いました。

　こういうお金の使い方は、経営者でないと難しいかもしれませんね。