今まで考えてきたことを例によって図で位置づける。
もちろん回り道へ。
単に「問題」ではなく、様々なコトから問題となる過程が広いということだ。
そして、単なる「解決」だけではなく、そこから新しい問題が生成される。
そういうことだったのかと腹に落ちた。
今日ついにこんなニュースが出た。
AIが数学オリンピックの難問証明 ひらめき獲得 数学者「ついに」：朝日新聞デジタル (asahi.com)
ＡＩが証明してしまうのだ。「解くこと」はＡＩでもできてしまう。
この問題をAlphaGeometryというＡＩが解いてしまったというのだ。
AlphaGeometry＝DD＋ARの記号演繹エンジン＋GPT４の仕組み
ARは代数規則、幾何学的規則。角度とか比率とか距離の追跡とか・・・
DDは演繹規則、つまり演繹的データベース。
多分証明はAIでもできると思っていたけど、予想をはるかに超える。
しかし、AlphaGeometryは証明ができた時、うれしいと感じないと思う。
AlphaGeometry: 数学オリンピック金メダリスト級(幾何学限定)の「ファスト＆スロー」なハイブリッド生成AI - GMOインターネットグループ グループ研究開発本部
これを読むと人間と同じことをしている。
スローが論理的推論で、ファストがアブダクション（仮説設定）。
幾何の証明の場合では、アブダクション（仮説設定）は補助線を引くことに当たる。
人間の場合はファスト⇨スローだが、AlphaGeometryは逆でスロー⇨ファストだというが、人間も同じことをしている。（人間の証明の仕方も二段階になっている）
論理推論の方は機械的だけど、アブダクションをできるのがすごいと思う。
これができるのが「言語モデル(LM)を使って、補助線の追加を行います」と書いてある。ファストは「言語モデル」なのだろう。
人間の行ってきたアブダクションをデータ化すれば可能だと思う。
それにしても、人間はそれをすべてデータ化しているわけではないのにアブダクションができるというのがすごい。
ついでにAlphaGeometryがこの問題をさらに一般化したと書いてある。
試しにやってみた。こちらの方がAlphaGeometryがやったのよりきれいだと思う。
