AIが証明を書く時代、数学者は証明を読むのをやめない。では計算機科学者は？
Wir müssen wissen – wir werden wissen
100年前、Hilbertは数学の完全かつ無矛盾な基礎を求めたが、GödelとTuringがその不可能性を証明した。それでも型理論はLeanなどの証明支援系として成熟し、いまAIエージェントがその上で定理を証明し始めている。計算機科学者である著者は、AI生成コードを読まないことが当たり前になりつつある現状に警鐘を鳴らす。プログラムは証明でもあるのだから、数学者が証明を理解しようと努めるのと同じ態度でコードに向き合うべきだと主張する。
機械に思考を明け渡せば、私たちは最後にはひどい目に遭う。AIに医療相談を任せて命を落とす事例が増えていることを考えてみてほしい。機械の言葉を当然のものとして受け取るほど、私たちは自分自身の運命を制御できなくなるのだ。
HNでの議論
15- dragontamer
「愚かなる不可知論 ignorabimus に反対して、我々のスローガンは Wir müssen wissen – wir werden wissen（我々は知らねばならない――我々は知るであろう）である」。
翻訳に早くたどり着きたい人のために言っておくと、IMO、タイトルの意味とブログ記事全体の主張を7段落目まで引っ張るのはちょっと不公平だと思う。
- t0mek
「我々はコンピューティングにおいても同じ姿勢を取るべきだ。抽象化を使い、リファクタリングし、スコープを洗練させ、高水準言語を発明して採用する。コードを頭の中に収められるようになるまで」。
これは本当だと思いたい。しかし反例として、我々の C や Golang のプログラムから生成されたマシンコードやアセンブリを頭の中に収める必要があるだろうか？ それともむしろ、Golang のコードこそが十分に優れた高水準の抽象化なのだろうか？
もしそうなら、さらに進んで、設計ドキュメントを頭に収めるのに適したコードとみなし、Golang のプログラムを派生物として扱うべきだということになるのだろうか？ あるいは設計ドキュメントもまた低水準すぎて、「アプリを作ってくれ、間違いは犯すな」という漠然とした雰囲気で実は十分なのだろうか？
正しい抽象化のレベルとは何か？ どうやってそれを見つけるのか？
- user2342
「Muss man wissen!（知らねばならない！）」