Bend 0.1リリース：AIの誤りを形式的証明でブロックする高速なCPU/GPU対応言語

TL;DR

Bend 0.1は、AIエージェントがコードを書ける高速で並列処理に対応した言語として登場。組み込みの証明システムにより、ユーザーが定義した法則を破る変更はすべてブロックされる。

Bendが提供すると主張するもの

Cレベルのパフォーマンス：ネイティブバイナリは単一コアでCに近い速度で実行され、GPUでは最大124倍の高速化を達成。
証明駆動の安全性：型チェックは証明チェックも兼ねる。ユーザーはLAWS.bendに法則を記述し、AIが生成したコードは、コンパイラが検証するPROOF.bendを出力しなければならない。
ゼロエフォートの並列処理：ランタイムは利用可能なすべてのCPUコアやGPUスレッドに自動的に作業を分散。明示的なスレッド処理やカーネルコードは不要。
エージェント向けツール：短いAGENTS.mdのスニペットで、LLMベースのエージェントにBendの使い方（bend guide、bend PROOF.bendなど）を教えることができる。

パフォーマンス数値（Apple M4 Max）

ベンチマーク	1コアBend	16コアBend	GPU Bend
型チェック（証明）	0.38 s（Leanの19.2 s、Isabelleの5分以上）	—	—
ランタイム（ライフゲーム）	7.80 s（≈1× C）	0.65 s（≈12×）	0.06 s（≈124×）
Leanとの型チェック速度向上	≈50×	—	—

サイトでは単一コアで7.8 s、16コアで0.65 s、GPUで0.06 sを表示しており、スケーリングの主張を裏付けている。

「法則」がAIの誤りをブロックする仕組み

LAWS.bendに、プログラムが決して破ってはいけない不変条件を法則として宣言する（例を参照）。
AIが実装と対応するPROOF.bendを書く。
Bendの証明チェックが証明を検証。証明が失敗すれば変更は却下され、AIは再試行する必要がある。

# 法則：勝利に至る移動シーケンスは存在しない。
law you_cant_win:
  for moves: List<Move>
    board = replay(start(), moves)
    is_won(board) == False{}

AIがプレイヤーが勝てるルールを追加しようとすると、コンパイラは法則違反を報告し、コードのマージを拒否する。このプロセスにより、潜在的なバグが定理に変換され、存在するためには証明が必要になる。

コミュニティのフィードバック – 強みと懸念

svachalek（HNコメント） – 「cronジョブを移植したが、システムは動いたが、多くの低レベルな算術補題（例：U32.add_comm）が必要だった。これらの補題はプロジェクト間で再利用可能だが、現在のライブラリには不足しており、証明の負荷を増加させている。」

RomanKornev – 「法則は新しい機能に合わせて編集可能だが、それでは目的を果たせない。一部の法則は凍結されなければならず、そうでなければ人間がボトルネックのままになる。」

jwpapi – 「Bendがすべての可能な移動シーケンスをどのように証明しているのか不明。大きな状態空間では網羅的な検証は現実的ではない可能性がある。」

tintor – 「興味深いビジネスモデル：人間よりも速く証明を更新できる有料エージェント。」

plastic041 – 「リポジトリは20kスターだが、最近のコミットは1件のみで、問題やPRも非常に少ないため、透明性と長期的なメンテナンスについて疑問が残る。」

mccoyb – 「Bendはアフィン型を備えたQTTに見えるが、密な配列カーネルではCUDAやFutharkに匹敵しない可能性がある。強みはバランスの取れた再帰的ADTワークロードにある。」

shantnutiwari – 「LLMは単に法則を無視したり、回避する可能性があり、静的証明チェック以上の堅牢な強制メカニズムが必要になる。」

これらのコメントは、より豊富な標準ライブラリの補題、不変法則に関するガバナンス、複雑な領域における証明生成のスケーラビリティに対する懐疑的な見方といった実用的な課題を浮き彫りにしている。

討論から得られたよくある質問

並列ランタイムはApple Silicon GPUで動作しますか？ サイトではCUDAを宣伝しているが、Apple M4 Maxの数値を示しており、ユーザーから明確化を求められている。
法則は実行時にどのように強制されますか？ 証明はコンパイル時に検証される。生成されたバイナリには法則自体の実行時ガードは含まれない。
既存のエコシステムと互換性がありますか？ 今のところスタンドアロン言語。Rust風のマクロなど、統合計画はまだ議論中。
無限ループや非終了はどうなるのですか？ 言語はソフトな再帰制限（約2⁴⁸−1）を強制し、終了性を保証する。他の証明志向言語のバウンデッド再帰と同様。

はじめ方

curl -fsSL https://bend-lang.com/install.sh | sh

LLMエージェントがBendの使い方を知るため、AGENTS.mdに以下のスニペットを追加する：

Bendを使用する際は：
- `bend guide`を実行して学ぶ
- 重要なルールは`LAWS.bend`に記述する
- コミットする前に`bend PROOF.bend`を実行する
- 可能な限りコードを並列化する

その後、単にエージェントに「Bendを使用する」と指示するだけでよい。

詳しく学ぶには

ガイド – 完全な言語仕様（bend guideでGitHubのGUIDE.mdを出力）。
BendTT – アフィン依存型理論に関する論文（paper/BendTT.pdf）。
BendRT – CPUおよびGPU向け並列ランタイムに関する論文（paper/BendRT.pdf）。
GitHubリポジトリ – https://github.com/bendlang/bend（問題は主なフィードバックチャネル）。

今後の展望

Bend 0.1は、ネイティブ速度のコンパイル、CPU/GPUへの自動並列化、そしてAI生成バグに対する証明ベースのガードを組み合わせた言語が可能であることを示している。コミュニティの初期反応はパフォーマンスと革新性を称賛しつつも、実用的な課題を指摘している：より豊富な補題ライブラリ、透明なプロジェクトガバナンス、LLMが宣言された法則を回避しようとする際の堅牢な強制メカニズム。プロジェクトが成熟するにつれ、既存コードベースとの統合の程度と、実世界の巨大状態システムへの証明ワークフローのスケーラビリティが、その影響力にかかっている。