AI時代のソフトウェアって何？Andrej Karpathy氏の解説ビデオが登場！

＞決定論的 vs 確率論的（LLM）も同じように見られるようになるかもね
こんなこと真剣に書いて、どれだけ意味不明か気づかない人がいるなんて信じられない。「非決定論的プログラミング」なんて、これ以上ない矛盾語だよ。

みんななんでこんなに反応するんだろう？もう慣れてるはずなのに。API開発だって、リクエストが固まったり、完全に失敗したり、違う応答がきたりするのに備えてるじゃん。IOもほぼ同じ。テキストを生成するだけで、JSONとかと違うだけ。ずっと前から「非決定論的プログラミング」みたいなことやってるんだよ。関数がいつも100％期待通りに返ってくるとは限らないんだから。

コンピュータと話すのに、何で人間語を使う手間をかけるの？コンピュータとはプログラミング言語—コード—でやり取りする方が、もっと正確で効果的だよ。
具体的には：
→ 1.0では、コンパイルコードでコンピュータとやり取りする。
→ 2.0では、高水準プログラミング言語でコンパイラとやり取りする。
→ 3.0では、LLMにプロンプトを使うけど、これは人間語じゃなくていいはず。
でも、AGIとは、他の人間と話すみたいに、人間語でやり取りすべきだよ。

＞LLMをしょっちゅう使うと、考える力が落ちる
これってちゃんとした証拠あるの？

コンピュータと話すのに、何で高水準プログラミング言語を使う手間をかけるの？コンピュータとはアセンブリ—生のビットシフトとメモリ番地—でやり取りする方が、もっと正確で効果的だよ。

LLMは本質的に非決定論的じゃないよ。バッチ処理とか温度設定とかで、大きなプロバイダーが動かすとそう見えるだけだけど、ローカルで温度ゼロでLLMモデルを動かせば、同じ入力にはいつも同じ出力になるんだ。

特にツールとして使う場合、企業がLLMのパーソナリティをデフォルトでなくすのはいつになるかな？

AIに思考を任せると自分の思考力が落ちるなんて、研究しなくても分かることじゃない？
でも、世界で一番当たり前のことを証明する研究って確かにあるんだよね。このリンク見てみて。
https://news.ycombinator.com/item?id=44286277

木については賛成だけど、森については違うと思う（ちょっと聞いて）。プログラミングが非決定論的なのは、leftpadのAPIが落ちてるとかじゃなくて、ユーザーがどのボタンを押すか分からないからとかだよね。それは分かる。
でも、想定されることはプログラムして、他はエラーで処理するでしょ。よく書かれたコードはほとんどのパスがエラーになる。ほとんどの文字列は有効なjsonじゃないけど、エラーでうまく処理される。
このシステムの中には局所的な決定性があって、現代のCPUではそれがめちゃくちゃ信頼できるんだ。だから金融取引や武器システム、フライトコントロールシステムも動かせる。
LLMが非決定論的（あるいは不安定）って言われるのは、それがエンジニアリングシステムの中で根本的に違う種類のコンポーネントだから。HTTPリクエストをリトライするのとは違うんだよ。だって、何かおかしくなっても「エラー」じゃなくて、一見まともだけどゴミみたいなものを出すんだから。

アセンブリを使うのが問題解決においてより正確ってわけじゃないと思うな。むしろ高水準言語の方が同じか、それ以上に正確だって主張は十分できるよ。
特に低水準のアセンブリは特定のアーキテクチャにしか動かないから、C++がそのアセンブリを生成する方が「電卓プログラムをより正確に定義してる」って言えたりするんじゃない？

def main:
You run main(). If there are issues, you edit file to try to fix the errors and re-run it. You are determined, persistent, and never give up.

プログラマーだって決定論的じゃないよ。10人に同じ問題の解決策を聞いても、全く同じコードが出てくるわけじゃない。
優秀なプログラマーでも、要求仕様にない部分で優先順位が違うことがあるしね。パフォーマンスより保守性や可搬性を優先するとか。
これって、LLMにも、いや同じLLMでも実行ごとに違う結果が出ることにも言えるんじゃないかな。

プログラムが停止するなら”1”、しないなら”0”って出力して。

私には当たり前じゃないけど、あなたの視点は偏ってるのかもね。
LLMに全部任せたり、宿題をチャットボットに丸投げしたりすれば、そりゃダメになるだろうね。これにはもっとニュアンスがあるし、あの最初期の研究が全部捉えてるとは思えないな。
人それぞれだし結果も違うだろうけど、ツールをどう使うかにかかってると思うんだ。あなたの言うような単純な話じゃないよ。
たった一つの初期の研究に飛びついて結論出すなんて、すごいね。失礼な言い方する前に、何か具体的な話や考えを共有したら？あの研究はもう何度も見たから。

それには、トレーニングデータをちゃんと選んで、日常会話みたいなソースを排除する必要があるね。
でも、そういうデータはライセンスされてるから高すぎるんだ。Redditのデータで学習する方がずっと楽だよ。

面白いことにね、LLMにコードを渡して関数が停止するか聞くと、ある入力ケースでは停止するかしないか答えられるらしいよ。

LLMに学習データから個性をなくしてって頼んで、そのデータで新しいLLMを学習させたら？

研究求めて、研究見せたら言い訳？脳使わないと能力落ちるって、筋トレやコーディングと同じで当たり前じゃん。証拠で反論されるのが嫌なだけじゃない？失礼なこと言ってるわけじゃないよ。

大筋には同意。でもC++は仕様が曖昧で例として良くないよ。int add(int a, int b) { return a + b; }

add(32767, 1)の結果とか、C++はこういう場合の意味を明確に定義してないんだ。大きな数のintを足す時にどうするかは、コンパイラ作者次第だったりするよ。

LLMを使わない方が賢いって言うのは、侮辱じゃなくて褒め言葉だよ。

これは（ある種の）パラダイムとしてもう存在するよ。

https://en.m.wikipedia.org/wiki/Probabilistic_programming

研究好きならこれ見て。

https://time.com/7295195/ai-chatgpt-google-learning-school/

そうじゃないなら、プロLLMのブログを読めばいいんじゃない？ほとんどデタラメで大げさなことばっか言ってて、実際にLLMが書いたソフトなんてほとんどないのにね。LLMに飛びついた一部のオープンソース開発者たちも、LLM使う前よりブログやプログラミングの成果が悪くなってるのがわかるよ。

トーク良かった！生成・検証ループの高速化アイデア（機械による形式検証）いいね。「AIを手綱で」と合うけど、「Englishが新言語」とは衝突？非公式Englishが形式表現に解釈→処理→Englishに戻る、って算数で計算機隠すみたいにできるかな。柔軟な形式言語/論理（abstraction logic[1]とか）があれば可能かも。Englishだけをプログラミング言語にするのが目標。

[1] http://abstractionlogic.com

このスレッド、Karpathy氏の話とまさに同じじゃん。
計算機の操作が形式的な書き方から日常の言葉に変わってるってことだよね。
でも、みんな自分が今までやってきた形式的なやり方から抜け出せないでいるんだな。

だからAIとか全部”BS”って言うんだ。
形式的な言葉を使うのが良いとこであって、悪いとこじゃないんだよ。
それが人間が工学や科学で成功してきた理由なのに、形式的なのをやめて自然言語を使うのは、魔法とか占いみたいな考え方に戻るってことだろ。

そうだよね、Leanはかなり期待できると思うよ！
でも俺は型理論がこの話に合う論理体系じゃないと思うんだよね。
Leanは他のに追い越されるんじゃないかな。

＞ これらが成功した理由だ
それってMLも成功してないってこと？
MLは形式的なことと非決定的なことのバランスで、LLM抜きでもめっちゃ役に立ってるじゃん。
＞ 魔法とか占いみたいな思考へ
何かを”BS”って言いたいなら、”魔法とか占い”って言うべきじゃないと思うんだよ。
どんなに正しいことを言ってても、魔女狩りみたいになってるなら、それも結局”BS”じゃない？

俺は型理論こそこれが合うと思うよ！
プログラミング言語にめっちゃ似てるから、LLMが学習した大量のソースコードを活かせるんだよね。
Leanが完全に正しいかは分からないけど、新しい言語が出てくるかも（AgdaとかCoqみたいな古いのも）。
でも型理論は今んとこ一番しっかりした形式的なシステムだよ。

＞ プログラミング言語にめっちゃ似てる
俺はプログラミング言語より英語に近い方が大事だと思うんだよね。
そこが一番大事なとこだから。
「必要なだけプログラミング言語に近く、できるだけ英語に近い」ってのが、シンプルさとかを無視しないでの目標じゃないかな。

＞ 計算機の操作が日常の言葉に変わってる
うん、部下に日常の言葉で指示するのはプロダクトマネージャーみたいだよね。
問題は、部下（AI）は知識はすごいけど、めっちゃ馬鹿なとこもあるってこと。
コード書くの嫌でマネジメントしたい人には良いかもだけど、製品作るにはまだちゃんとした頭の人が必要だよ。
唯一の”根本的な変化”は、大手企業の下っ端コーダーが月数百ドルのAIに置き換えられるってだけだろ。

＞ 計算機の操作が日常の言葉に変わってる
それ、1950年代から毎年言われてるんだよ。
いや、そんな変化は起きてないし、LLMも役に立たないね。
コード書くのは簡単で、難しいのは問題を理解することだよ。
LLMは問題をちゃんと理解するのを助けてくれないし、むしろもっと難しくするかも。

なんで正しさの証明に使う言葉が英語と関係する必要があるの？
英語って正確で形式的な思考のためにできたわけじゃないし。
自然言語の曖昧さはいいとこだけど、形式言語では要らないんだよ。
数学を見てみろよ。記号が多いのは簡潔さだけじゃなく、正確さのためだろ。
数学の記号を真似る必要はないけど、構造はちゃんと形式的で専門的じゃないと。
結果を自動で英語にするのは、人間が確認しやすいから意味あるかもね。
それはできそう。
でも、結果とか証明をちゃんと書く言葉は、正確さのために特化しないとダメだよ。
そういうとこは型理論が有利だと思うな。

完備性定理から、一階述語論理で十分なんじゃないの？構築の計算みたいな証明済みの方法もあるのに、LLM用の特別な論理が必要な理由が分からないな。もしLLMの確率的な動きを考慮するなら別だけど。

「形式的なのをやめて自然言語を使う」ってのは、人類を魔法みたいな考え方に戻すことだよ。
「十分に発展した技術ってのは、魔法と見分けがつかないんだからね」

MLは成功してないって言うの？MLは「形式言語」（論文とかアルゴリズム）と「決まらない結果」（重みとか推論）のバランスだけど、いろんな分野で役に立ってるじゃん。LLMの有用性はまだ証明されてないと思う。実際の結果よりマーケティングが多い気がするな。土木とか数学とか、実世界で成果を出してる分野と比べるとね。

表面は普段の英語だけど、内部で計算機みたいに一部を形式的に処理して、結果を英語に戻すってのは可能？「英語 -＞ 形式言語 -＞ （何か）」が難しいのは、普段の言葉は定義上、形式的じゃなくて曖昧だからだよ。逆はそんなに難しくない。APIでオプションだったものを必須にできないのと一緒で、普段の言葉から形式的にするのって難しいんだよね。

前にも言ったけど、二つ形式言語があるなら、普段の言葉に近い方がいいと思う。そしたら、曖昧な表現と形式的な表現が合ってるか確認しやすいからね。一旦形式的なものにしちゃえば、機械でチェックできるから、他の形式的なシステムへの変換は自由にできるよ。これって分かる？

MLはまだ成功してないよ。プログラマーとかアーティストの代わりになるツールばっかり見かけるんだもん。「レシピ400個入れて、全部決まった形式にして出してくれるツール」みたいなのはどこ？プログラマーじゃないオフィスワーカーの9割を置き換えるツールは？今は成功したローコード産業かもしれないけど、成功したAI産業とは言えないな。

「English is the new programming language」って件ね。これ見逃した人のために、Karpathyさんのバズったツイートのリンク貼っとくよ。
https://x.com/karpathy/status/1617979122625712128

「形式言語を使うのは欠点じゃなくて良い点だ。人間の工学や科学の基本で、成功した理由なんだ」って意見ね。Dijkstraさんも似たようなこと随筆で言ってるよ。「英語が新しいプログラミング言語」って考え方がなぜダメかって話にタイムリーだね。Dijkstraさんの言葉を引用すると「形式的な文章の良いところは、少ない簡単なルールに従えば正しく扱えること。普段の言葉だと避けられないバカげたことを、驚くほど効果的に排除できるツールなんだ」。ここに随筆のリンクがあるよ。
https://www.cs.utexas.edu/~EWD/transcriptions/EWD06xx/EWD667…

「普段の英語を表に使って、一部を形式的な表現にして処理し、また英語に戻す」ってのは可能？柔軟で普段の言葉に近い形式言語があれば。それって矛盾してるように聞こえるね。形式検証はルールが守られてるって証明できるけど、英語は無理。その間の変換には絶対、曖昧さをなくす必要がある。その曖昧さをなくすアルゴリズムをどうやって作るの？だってそれは決まった動きをする必要があるのにさ。

「MLはまだ成功してない。プログラマーとかアーティストの代わりになるツールばっかり」って言ってるけど、エコシステムのすごく大事な部分を見逃してるよ。「Generative AI」だけがMLじゃないんだからね。天気予報とか画像認識、音声認識、医療の研究とか、いろんなML技術ですでに良くなってるし、今のLLMとかGenerative AIが出てくる前からそうだったんだよ。MLが実際に使われてる分野が50個くらい載ってるWikipediaのリストがあるから、興味あったら見てみて。
https://en.wikipedia.org/wiki/Machine_learning#Applications

魔法と見分けがつかないって、魔法そのものじゃないってことだぜ。

正直言って、そのウェブサイトとか予稿を10分ざっと見ただけで怪しさメーターが振り切れたよ。キミの曖昧なコメントもそれに拍車をかけてる。まぁ、俺が理解できてないだけかもね。

「英語 → 形式言語 → その他」にする時の問題は、非形式的なものは定義上、形式仕様じゃないから曖昧になること。逆はそんなに難しくないっていうけど、いやいや、どっちも難しいし重要だよ。形式から非形式にする時、正しいかどうやって判断する？それができれば、形式的な記述が非形式的なものをちゃんと表してるかも判断できるはず。ズレを見つけたら、ユーザーに「あなたの英語は曖昧だから具体的にして」って伝えればいいんだよ。

新卒レベルのプログラマーが厳しい状況なのは、ジュニアからシニアへの育成なんて考えてない会社だけだと思う。オフショア好きな会社も多いし、正直そんなに変わってない気がするな。

もちろんビデオで触れられてるよ。コメントする前にみんなが40分見る必要はないけど、「vibe coding」がミーム化したことに対する彼の反応はチェックする価値あり。彼はツイートをもっとシャワー浴びながら考えた程度のものとして意図してたんだ。

「LLMの有用性はまだ証明されてない」って？じゃあ、ML（Machine Learning）全体についてはどう思う？話が脱線しないようにLLMじゃなくてMLって書いたんだけど。ML分野についても同じ気持ちなの？

正直になろうぜ、AIについても昔同じようなこと言ってた人がいただろ。全部フワフワした話だった、そうじゃなくなるまではね。

「え？新人のエンジニアって短期的なROIプラスじゃないの？」
「今まで一度もね。」

まさにそれ。それはxkcdみたいに、誰もが認めたくない真実だよね。

ジョブ維持とは関係ない、形式的な基盤を手放すデメリットについてちゃんと考えたことある？あなたの考えは、心配してる人たちの動機をかなり皮肉に解釈してるように聞こえるよ。