証明でAIのミスを防ぐ新言語「Bend」海外で期待と懐疑が交錯
姉妹サイトの新着
他サイトの新着
- 5chまとめMAP【朗報】自治会、自然消滅しそう
- ニュース速報まとめMAP花畑エリアの素敵な飲食スポットの数々 #足立 #飲食 #カフェ
- なんJ傑作まとめアンテナMAP【激怒】活動家グレタさん、人気歌手エド・シーランさんを痛烈批判「被害者はパレスチナの人々しかいない」・・・・・・・・・
- アニメ声優まとめアンテナMAP【画像】トリコの三虎さん、フローゼの服を常時着ている変態だった
- VTuberまとめアンテナMAP【にじさんじ】9/24(木)18:00から、月ノ美兎の誕生日を記念した『誕生日グッズ＆ボイス2026』販売決定！
- だめぽアンテナ【悲報】ヤニ猫のカンサイねこ、人間ち〇ぽに堕ちてしまうｗｗｗｗｗ
- ヌルポあんてな有識者「ガソリンの本当の値段は220円。補助金で無理やり安くしてる状態だがそろそろやばい」
- 2chまとめアプリ+彼女が友達とか言ってSNSの男と頻繁に連絡とってるんだが
- News人【オーバーロード】AFORCE「オーバーロード」トレフィグ【予約開始】他
- ブルーアンテナ俺の最愛の幼馴染の話をしようと思う
- ウマーあんてな藤井風さんの免許証、レベチｗ
- ２ちゃんマップソロキャンプ特化のキャンプ場を作ろうと思う。
- おまとめ米イラン戦争ついに終わる？ちょｗトランプ大統領ｗｗｗ
- カオスアンテナ【衝撃】磯野家のちゃぶ台、11人でも使用可能なことが発覚ｗｗｗ
- 即まとch諸費用込み230万円でボロ空き家購入 天井崩落に「タダでも住みたくない」の声
- おまとめアンテナ【おまいう】ロシア外務省「日本は満州事変の歴史を銘記すべき。再軍事化は必ず過ちを繰り返すことになる」
- 憂国あんてな|●|【速報】玉城デニー氏 辺野古転覆事故について「事故の原因は誰にあるのか､捜査中で発言できず､対応に不手際があったように受け取られた」
- リアルな海外の反応アンテナ【PICK UP】【海外のお前ら 海外の反応】海外「日本の田舎での暮らしって実際どんな感じなの？」（海外の反応）
- ライムアンテナ鹿目まどかのえっちな画像を貼りなさい
- とろたまヘッドラインAC長野パルセイロ、松本山雅FCとの対戦を「NAGANO DERBY」と呼称すると発表 「この呼び名に賛否があることも、承知しています」
Hacker Newsで、AIコーディングエージェント向けの新言語「Bend」が話題になっていた。開発したのはHVM(並列計算モデル)で知られるVictor Taelin氏らのチームで、AIがコードを書き換えるたびに、あらかじめ定めた「法則」が数学的に成り立っているかを証明でチェックし、崩れていれば書き直させる仕組みを謳う。コンパイル先はCUDAやMetalで、GPU上での並列実行もうたっている。スレでは、この「証明」の実用性やベンチマークの不在を疑う声、コミット履歴をフォースプッシュで消したことへの批判、そして形式検証がFacebook級の現実のソフトウェアに通用するのかという論争が交わされた。
Bend ― 証明によってAIのミスを防ぎ、GPU上で動く新言語
出典: bend-lang.com / 元記事はこちら
「バグのない、高速なvibeコーディングアプリを楽しもう!」→ 詐欺くさい。そのベンチマークはどこにあって、どうやって再現すればいいんだ?
『AIたちに何をしてほしいか、曖昧さのない形で伝える方法がまだ必要だ』とあるけど、本当にそうか? AIがここまで生産的なのは、曖昧な部分は勝手に解釈してくれるおかげで、こちらが逐一指定する量が減っているからだと思う。
>>8 いや、両方必要だよ。
問題は、その『法則』全部をvibeコーディングで書かないといけなくて、しかもその法則自体が間違ってるかもしれないってことだ。
>>9 冗談はさておき、法則自体を書くのは簡単で、それが成り立つことの証明をAIが担う、という発想だと思う。ただ複雑な法則を表現しようとするほど、この前提は怪しくなりそうだけど。
>>9 至言。
質問です。他の言語でテストを書くのと比べて、これは実用面で何が違うんですか?
証明自体が自然言語で書けるようにならない限り、人間には広まらないと思う。証明を読むだけでも認知負荷が高いのに、書くとなればなおさら。
>>11 同意だけど、自然言語には曖昧さがある。AIの出力には前提条件を必ず含めるべきだし、『プロンプト』という言葉自体を『会話』に置き換える必要が本当にあると思う。
Victor TaelinのHVMの仕事がきっかけで、コンパイル先としてのinteraction combinatorsに興味を持った。今は大学の研究でその実装に取り組んでいる。Bend 2.0のリリース、見られて嬉しい。
>>12 それなら、Marc Thatcherの博士論文がinteraction netsを扱っていて興味を持つはず。乗法線形論理の証明ネットを通してinteraction netsを解説していて、生産性解析など独自の貢献もある。[1] https://hdl.handle.net/10779/uos.32024301
リリースおめでとうございます。質問ですが、この並列処理はM系のGPUでも動きますか? ページにはCUDAでの並列処理と書いてあるのに、性能数値はMacのものが出ています。
『ポストAGIの世界に生きている』という主張が変だな。真のAGIを実現した企業なんてまだどこにもないのに。
>>15 そんな主張はどこにも見当たらないけど。
READMEとガイドを読んだ。一つだけ言えることがある。NP困難問題も解いてみたらどうだろう。作者ならこれより難しい問題をすでに解いているんだから、簡単にできると思う。
Ada/SPARKと比べてどうなのか聞いてみたい。
Windows非対応? 公理的なF32? Slopjective-C 3.0の方で我慢しとくよ。
いいチームがついてる。SSL証明書まで耐量子仕様とはね。
懐疑的な人ばかりで、誰も実際に試してないのか。自分は後で試してみる。見た感じは悪くないし、文法も好み。主張の真偽はわからないけど、試す価値はありそう。GPUの話は、Macでも動くのか、それともGPUを選ばないのか気になる。
claude: 1コミット 追加1,722,119行、削除0行。CakeMLのように、ClaudeがBendの正しさを形式的に証明したということなのか? こんなディストピアな仕組みでどうして誰かが働きたがるんだ。コードを証明したいならLeanかCoqで直接やるか、やらないかのどちらかにしろ。
GitHubにはコミットが1つだけで、しかもコンパイラすら見当たらない。コンパイラはどこにあるんだ?
>>24 自分も今初めて見ているところだけど、コンパイラはこれ https://github.com/bendlang/bend/blob/main/bend2/comp.ts じゃないの?
>>24 コンパイラはcomp.tsにあって、ランタイムも同じ場所にある。正直きれいなファイルじゃなくて、今はその場しのぎの部分やAIスロップも多い。読む価値があるものを探しているなら、カーネル(bend.ts)を読んでほしい。
興味深いけど、形式的なソフトウェア検証が答えになるとは思えない(これってそういう話だよね? ちょっとわかりにくいけど)。現実世界の多くのプログラムに対しては難しすぎてスケールしない。Facebookをどうやって形式検証するんだ? しばらくは普通のテストとコードの目視確認でやっていくしかないと思う。
>>25 EC2くらいの規模でも現実世界として十分? 6月の話だけど→ https://aws.amazon.com/blogs/compute/aws-nitro-isolation-eng… AppleのPQ暗号ライブラリの話も5月に出てる→ https://security.apple.com/blog/formal-verification-corecryp… Microsoftも7月に似た話をしている→ https://www.microsoft.com/en-us/research/blog/verifying-rust…
コメント欄で『vibeコーディングだ!』って言われるのにうんざりしてる。これはAI向けに作られたツールなんだから、作者が全部手書きしろとでも思ってるのか? ドキュメントにClaudeっぽい言い回しが少しあるからって、全体が無監督のスロップだと思うのか?
>>2 証明されることを前提に最初から設計された言語というアイデアは好きだし、コーディングエージェントの存在を考えると説得力がある。他の人がまだ気づいていない良いアイデアだと思うから、誤解されたり口汚く叩かれたりするのも覚悟しておいた方がいい。
他サイトの新着
>>2 こんにちは作者さん。質問なんですが、あのボード/旗のアニメーションはBendのコンパイル時チェックとどう関係しているんですか? 実際にBendがチェックを走らせているところを直接見せているんでしょうか?
>>31 チェックはアニメーションとアニメーションの間で行われている。AIがコードを編集するたびに、Bendはすべての法則がまだ数学的に成り立っているかを確認する。成り立っていなければAIはやり直す。だからあのアニメーションは、Bendが関わっている場合といない場合でアプリに何が起きるかを示しているだけ。
>>2 正直『Bend』だけの方がHNのタイトルとしては優れてる。詳しい説明はホームページに書けばいい。
>>16 何度もある。理由らしい理由はまだ示されていない。https://github.com/bendlang/bend/activity?ref=main 一度はフォースプッシュして、2行だけのREADMEを残して他は全部意図的に消し去っている。消される前のバージョン: https://github.com/bendlang/bend/tree/814453670d0e0d6777c131…
>>42 コミット履歴には個人情報や、SupGenのような独自コードもかなり含まれていたから、squashしただけだよ。それが問題になるとは思わなかった。なぜ問題なんだ?
>>16 TaelinのXを見れば、codexやfableたちがどうBendを『折ろう』としたかの武勇伝が書いてある。LLMが関わっていることを恐れているなら、もう恐れなくていい。実際に使われているから。
>>16 curl -fsSL https://bend-lang.com/install.sh | sh …うーん、sudoが必要なのか。
>>16 GitHub上では44人のコントリビューターがいて、41人がプルリクエストをマージしている。……それなのに、彼らの仕事はもう何も残っていないってこと?
>>16 そう、コミット履歴には個人情報やAIスロップがかなり含まれている。それが君にとって問題なのか? なぜ?
>>27 はは、何十年も前から警告されてきたのに、現実にアシモフの世界を書いている真っ最中だな。
>>28 その言い回しは直すよ、ありがとう。要するに、Bendは1つの.cファイルにコンパイルされて、そのファイルがマクロ経由でMetalかCUDAのどちらかにコンパイルされる、というだけの話。ほとんどのユーザーには関係ない部分のはず。ランタイムをCとMetalとCUDAの3回書き直すのではなく、ファイルを小さく保ってコードを最大限使い回すために自分が見つけたやり方に過ぎない。
>>38 その通り。人間が証明を書くのが得意なら、そもそもコードを直接書いているはずだ。
>>40 あ、そのリンク404になる。
この話題の背景と論点
Bendは並列計算基盤HVMで知られるVictor Taelin氏らが開発する言語で、2.0でAIコーディングエージェント向けに「証明」機能を加えた。AIがコードを編集するたびに、あらかじめ書いた「法則」が数学的に成り立つかをBendが検査し、崩れていればAIに書き直させる仕組みで、1つの.cファイルにコンパイルしてCUDAまたはMetal向けにマクロ展開する。スレでの意見の割れ目は大きく2つ。ひとつは「vibeコーディング」を売り文句にする姿勢への懐疑と、AIが人手を離れて法則自体を書く以上、その法則が間違っている可能性は残るという指摘。もうひとつは開発の透明性で、GitHub上で41人が関わったプルリクエスト履歴をフォースプッシュで2行のREADMEに圧縮した経緯に批判が集まり、作者は「私的情報や独自コードが含まれていたため」と釈明した。形式検証が実用規模のソフトウェアに通用するかという論点では、AWSのNitro、AppleのPQ暗号、Microsoftのverified Rustなど実例を挙げた反論も出ており、机上の空論とは言い切れない状況が背景にある。
※本記事は5ch(Hacker News)スレッド「Bend – A language that blocks AI mistakes via proof and runs on GPUs」より抜粋・要約して構成しています。
この記事のリアクション
まだコメントはありません。