ディープラーニングとRPAで客が呼べる終わりの始まりって感じ・・・

７月２９日、マルレクの

RPAは「推論エンジン」の夢を見るか

を聞いてきたのでメモ。
ごめん、最後のほう、ぼーっとしてて、あんまりメモとってない。

---

もう一つのAI技術：ディープラーニング以外
　→人工知能ディープラーニングで何でもできる？

・第一部　RPAとディープラーニング
　→ディープラーニングに対する現実的な評価
　第三部　機械による推論は可能？

・第二部　複数の人工知能技術
　→考える機械を構成できる？何かが欠けている

　自動証明：ロボットでなくて、ガンダムやエヴァっぽいロボット
　　→人間が必要で、操作する

・数学的推論：ディープラーニングから一番遠い
　源流：１９３０年代　照明可能性、計算可能性
　１９７０年代　型の理論

・新しい型の理論 Homotopy Type Theory
　コンピューターのプログラムが行っていることは、数学的推論に他ならない
　coq
　プログラム：証明する過程
　Deep Specification　誤りのないプログラムを作る

・AI　VS　RPA

・ソフトバンクのRPA+AI

・大規模事例
　Skymind
　　不正請求の判定
　　保険業のワークフローの自動化

・Amazon Sage Maker：統合して作る

・テレコム業界：SIM　BOX　Fraud　詐欺対策

・羊毛党

・ルールエンジンとの併用：AutoEncoder

・ビッグソフトウェア
　→カノニカル：

・ニューラルネットで論理的推論
　ニューラルネット：外部メモリを持たない
　DNC

・人間の脳とのちがい

・DNCが取り組んだ３つの課題

・実験結果をどう見るか
　　baaBi task: あまり成績よくない
　　グラフで表現された知識を大規模システムで処理
　　Prologでできる？

・ディープラーニング万能論の終わりの始まり
　センサーとしてのディープラーニング技術とセンサーだけではできないこと
　　→センサーがあっても・・・

・Simonの予言から学ぶ
　自動証明：Logical Theorist
　→General Problem solver(GPS)
　→Elementary Perceiver and Memorize(EPAM)
　命題論理：とけた
　述語論理：１９６５年のロビンソンのResolution Proncipalへ　

・第五世代コンピューター、Parallel Distributed Processing

第二部：複数の人工知能技術
　数学・科学　→機械による数学的・論理的推論
　　　↑　　　　大きな飛躍
　　文字　　　→知識表現
　　　↑
　　言語能力　→自然言語
　　　↑　　　　大きな飛躍
　感覚・運動　→ディープラーニング


第三部　機械による数学的推論は可能か？
・１９３０年代　証明可能性＝計算可能性
　ラッセルの逆理→型の理論
　ゲーデルの不完全性定理：無矛盾性証明→できない
　　→証明とは何か、計算とは何か
　ゲーデル・チャーチ・チューリング：同じこと
　
・１９７０年代　「プログラム」＝「証明」？
　チャーチ：ラムダ計算
　カリー・ハワード対応：型つきラムダ計算→coq
　ｐ：P
　ｐは。命題Pの証明である
　ｐは、型P

・２０１０年代
　全数学理論をコンピューター

証明をめぐる問題
・誤った証明
・正しいことの判定が難しい証明
・膨大な証明（有限単純群の分類問題」

コンピューターで数学！
・四色問題 Coqで
・最近はE8

Program as Proof
・Coqのプログラムはある型をもつ定理の証明として走る
・Deep　Spec
　事例：Kami　Project
　暗号化