Bend 2の「バイブコーディングの罠」：LLMが形式検証の常識を見落とす
Bend 2 and the Vibe-Coding Trap
Bend 2はAI時代のプログラミング言語として、人間が「法則」を書き、AIが実装と証明を生成することを売りにしている。しかし、デモでは58行の仕様に対して442行の証明が必要となり、形式検証の標準的な手法（SPARKなど）を使えば12のチェックで同じ性質を証明できる。著者は、バイブコーディングが問題領域の調査を怠り、何十年も遅れた設計を生み出す罠だと指摘する。
バイブコーディングは、はるかに優れた解決策が存在することに気づくのに十分な知識を得る前に、実質的な解決策を構築することを可能にしてしまう。
HNでの議論
222- hmokiguess
> 問題は、バイブコーディングによって、はるかに優れた解決策が存在することに気づくのに十分なほど問題について学ぶ前に、実質的な解決策を構築できてしまうことだ。
この例とBendはさておき、私はこれが今日の「知覚される知能」との最大の闘いだと思っている。何か動くものを作るのは得意だが、自分が知らないことを知らないときに、それを指摘するのは得意ではない。
優れた自己認識と規律がなければ、教育して軌道修正することはできない。
とはいえ、これはすべてに当てはまると思う。これは非常に人間的であるため、この罠に陥りやすい。私たちは自分が知らないことを単に知らないので、古い解決策を再訪して、今では新しい情報があり、それをはるかに優れたものに置き換えられることに気づくのは珍しいことではない。
ここに新しいものや変わったものは何もないと思う。もし変わったことがあるとすれば、私たちがこれを経験する速度だけだ。LLMはフィードバックサイクルをより簡単かつ迅速に実現する。
さてBendに戻ると、自分の作品を公開し、それを恥じずに、オープンソースでさえも、フィードバックを受け入れる姿勢は大いに役立つだろう。
私がより心配しているのは、販売され、人々が依存しているLLM製製品の多くのクローズドソース実装が、多くの異なる思考者からのこの素晴らしい批判を受けていないことだ。
- pu_pe
このプロジェクトに関する元の議論（https://news.ycombinator.com/item?id=49746163）は非常に奇妙だ。著者が何かの有名人であるかのような指摘や、彼を支持するランダムなアカウントが多く、本質的な議論はほとんどない。
そのリリースのデモさえもうまく動かない。
- z7
> 問題の分野は形式検証である。Bendのウェブページやコードベースのどこにもこの2語が現れないのは注目に値する。開発者は、その分野が存在することに気づかずに、その分野を中心に言語全体を構築したようだ。
開発者のXアカウントを確認したところ、形式検証について多数の投稿を書いているので、この特定の主張（「その分野が存在することに気づかずに」）は誤りのようだ。
- thomasahle
> これがBendと異なる点は、ここで提供しているものが、LLMに442行の証明を第一原理から構築するのに時間とトークンを浪費させることなく、プログラムの正しさを証明するために必要なすべてであることだ。GNATproveを実行すると、`Success: all checks proved (12 checks).`が得られる。
GNATproveはSMTソルバーを使用しており、つまり基本的には力ずくの証明システムだ。
はい、力ずくの証明は記号的証明（lean、bendなど）よりも簡単だ。なぜなら証明を提供する必要がないからだ。すべて自動だ。
しかし、力ずくの証明はほとんど関心のあるものにスケールしない。だからこそ形式検証は30年間ニッチな分野だった。今、LLMが_実際の_証明を書けるようになるまでは。
- johnfn
著者が形式検証を知らないと非難するのはかなり印象的だ。数分の調査で即座に反対の証拠が出るのに（https://x.com/victortaelin/status/2100942399132312059?s=46、https://x.com/victortaelin/status/2100374221671051472?s=46）。
- captainmuon
Bend 2を詳しく見たわけではないが、「ひどく壊れているか、現在の最先端から数十年遅れている」と呼ぶのは少し厳しいように思う。明らかに形式検証言語には問題があり、その分野で何か別のものへの需要があり、問題は使いやすさと構文だ。Haskellのように見えるものを学びたくないし、Curry-Howard対応を頭に叩き込まれたくもない。C++テンプレートメタプログラミングのように見え、感じるもので条件を書きたくない。数年前のCoqのようなものでのHello Worldを覚えているが、それは基本的に「まず、ペアノ整数を構築する」から始まり、それを使ってある計算が有界であることを証明していた。なぜなら、整数をネイティブに表現できなかったようだからだ？
ただC#やJavaScriptなどで書き、同じ構文で事前条件やチェックなどを付け加えられるようにしたいだけだ。依存型付けと契約による設計を大衆のために。
- mentalgear
> Bendの著者は、これが形式検証の分野における現在の標準であることを完全に見落としている。その分野が存在することさえ知っているかどうかも怪しい。代わりに、冗長な仕様とさらに冗長な証明を必要とするシステム全体を思いついた。言語とコンパイラ全体をバイブコーディングする前に少し調査していれば、著者は何を求めるべきかを知っていたので、結果は大幅に改善されただろう。
> この例はBendを超えて重要だ。バイブコーディングは、ひどく壊れているか現在の最先端から数十年遅れている設計を実装することをあまりにも簡単にする。なぜなら、調査を一切せずに即座に結果を得られるからだ。関数が形式的に正しいことを基本原則から証明を構築して証明できる言語をLLMに求めると、喜んでそうするだろう。コンピュータがすでにLLMなしで複雑な証明を構築でき、作業の99%を排除できることを提案するために立ち止まることは決してない。あなたが作っているものが、すでにほとんど既存の作業として存在し、それを基に構築できることを決して教えてくれない。
---
だからこそ、実質的なものを構築するためのLLMリクエストはすべて「まず先行研究を調査せよ」から始めるべきだ。もちろん、ある時点で（出力をオープンソースで共有すれば）すべてが収束し、堅固な標準パターンとライブラリができ、同じ些細で基本的なものを世界中で何兆ものトークンを浪費して再構築する必要がなくなるかもしれない。それぞれがその静かなlit […]
- wg0
README.md[0]からの注目すべき行：
> - コンパイラ（カーネルではない）は99% AIによって書かれており、まだ完全に監査されていない。
> - 文字列は文字のリンクリストであるため、テキスト処理は遅い。