現在、おれはGPU並列アルゴリズムライブラリ「massively」をAI（というかチャッピー）と一緒に作っているが、IDEによってソフトウェア開発技法が進歩したのと同様に、AIによってソフトウェア開発技法が進歩したと感じている。
AIを使う上で、AIに対して「いかに問題を解かせるか」という技術が重要になってくるわけだが、おれはこれについてはmap型とreduce型の2つがあるという整理をしている。map型というのは問題自体を簡単にすることであり、reduce型というのは問題を分割統治することである。
massivelyは、CubeCLという基盤の上にGPU並列アルゴリズムを構築するものだが、これは非常に難易度の高い仕事であり、おれ自身もはや「きっとこんな感じのことをしてはるんやろな」レベルでしか理解していない。つまり、ユーザがアルゴリズムを実行しようとするとそれは型として運ばれ、ディスパッチャーという機構によって最適なカーネルコードとディスパッチされる。そしてディスパッチされるカーネルコードはきっとこんな感じのアルゴリズムを実装しているのだろうという程度でしかもはや把握していない。コードレベルでmassivelyが正しいことをしているのかを把握することは人間にはかなり厳しい。
そんなmassivelyだがどうにかして正しいことを証明しなければならないわけだが、おれはそのためにチャッピーにCPU実装を書かせ、proptestを使ってGPU実装とCPU実装を網羅的に比較することにした。これによって、おれはCPU実装が正しいことを納得すれば、GPU実装も正しいことを納得出来ることになった。つまり、GPU→CPUという次元下げを行ったのである。これはmap型の問題解決法といえる。CPU実装なら容易に読めるから、難易度を100万から1に落としたようなものだ。
これは当たり前の発想かも知れないが、もしAIがなければ実行することはかなり難しい。アルゴリズムは50個近くあり、そのCPU実装を書くこと自体は出来るかも知れないが、proptestまで書くとなると相当にうんざりするだろう。実際にチャッピーが書いたものは高度なマクロ生成を使った理路整然としたコードなのだが、このようなものにたどり着くことすら難しいと思うし、そうなれば莫大な時間がかかるだろう。莫大な時間がかけてゴミを作る。人間にはその程度の仕事しか出来ないのだ。
つまりAIがなければ結局、やらないとなった可能性が高い。それはIDEがなくVIMやemacsで開発していた時代に、色々億劫でコードがどんどんボロボロになっていったのと同様に。しかしAIを使えば、その仕事はものの10分で出来たのである。IDEを使うとプロジェクト全域のリネームが1秒で終わるのと同様に。
こういう、AI以前には実質的に実行不可能であった技法が可能になり、ソフトウェア開発技法はより進化するであろうと思う。特に今回使ったような、より簡単な別の問題を解かせた上でそれとこれとをproptest的な技法で接続するというのは技法として一般化出来ると思うし、より高度な証明ベースの技法も使われるようになるだろうと思う。実際、ADAのような先進的なブロックチェーンでは、スマートコントラクトの検証にLean4を使うという試みがなされているようだ。概念的には今回おれがmassivelyで行った技法と、「正しいことがより確からしい世界に射影して検証する」ということだろうから、似たようなものなのではないだろうか。