2012年に始まったプロジェクト「ロボットは東大に入れるか。」国立情報学研究所の新井紀子教授をプロジェクトリーダーとする。人工知能の研究は既に40年以上の歴史がある。その研究成果を再編し、新たな知見を得ることを研究目的とする。人工知能研究の初期より、自動定理証明が研究されてきたこともあり、今回のプロジェクトでは東大に入学できるAIを完成させることが出来るかの検証も目的とされた。ここでは比較的良好な結果の出た東大入試数学のソルバーについて調べてみた。数学の問題は、当然自然言語で記述されているので、それを入力する。次にそれを解析して、一階述語論理式に変換し、ソルバーによって同値変形、数値解析を行い答を見出す、或いは命題を証明する。作成した東ロボくんに東大理系数学問題、ベネッセ模試、代ゼミ模試、駿台模試などを解かせたところ、6題中2題から4題完答したと言う。二次試験については期待するレベルに到達できた。しかし、センター試験では苦戦を強いられ、偏差値は60点台に到達しなかった。二次試験では偏差値は76.8点に到達。センター試験を苦手とする東ロボくん。国語、英国、社会は二次試験でも苦手であった。昨年の11月、東ロボくんを東大に合格させるプロジェクトを終了する旨が発表された。数学については、問題の自動解答の研究は継続することとなった。改良すべき点は、自然言語処理部分である。数式処理への落とし込み部分にはZF集合論が使用されている。その上で、論理式が評価されている。他に、大切な要素技術としては限量記号消去法だ。
最後に、こうした研究で注意すべきは、AIにより、何が出来るではなく、何が出来ないかである。出来ない部分に、人間の知能の特性が含まれているという視点が最も重要だと、私は考える。
