「証明」によりAIの誤りを阻止しGPU上で動作する高速プログラミング言語「Bend」、C言語並みの処理速度・CUDAによる並列処理・Leanによる形式的証明・Python風の構文

「 Bend 」はAIが犯すかもしれない誤りを「証明」によってブロックすることを目指す新たなプログラミング言語です。

Bendはポスト AGI の経済社会において人間がコードの記述や読解から解放される未来を見据え、AIに対して意図を明確に伝えるための手段として開発されました。Bendは「法律(Laws)」によって意図をより正確に表現し、「証明(Proofs)」によってAIがプロンプトを正しく実装したかを検証します。また、高速なコンパイラにより実行速度も確保されています。

Bendはネイティブコードへのコンパイルを行うため、単一コアではC言語に近い速度で動作します。さらに16コアやGPUを利用すれば、単一コアの100倍近い速度での実行が可能です。 シンボリック回帰 を用いたベンチマークでは1コアで3.01秒、16コアで0.27秒、GPUで0.53秒と従来の言語と比較して高速な実行結果を示しています。

Bendの型チェッカーは証明チェッカーとしても機能するため、LeanやRocqのような言語が数分かかるような中規模コードベースのコンパイルをBendは1秒以内に完了させます。つまり、AIエージェントはソースコードの変更結果を迅速にチェックできるということです。1万2800定義を含むコードベースでのコンパイル時間は、IsabelleやAgdaが5分以上かかるのに対し、Leanは36.2秒、Rocqは5.99秒、そしてBendはわずか0.29秒です。

Bendはスレッド・ロック・カーネルの記述なしにタスクを複数のコアに分散させることができ、効率的に並列処理を実行します。

LAWS.bendで宣言された法律はAIのコーディングに対するルールとなり、AIが違反するコードを生成することを数学的に不可能にします。例として、ゲームで「勝利不可能」という法則を定義した場合を考えます。

新機能としてAIに「ボードをぐるっと一周させてくれ」と指示したとします。

法律がない場合、新機能をマージすることで「勝利不可能」という法則が覆されてしまうかもしれません。

法律によりBendは「勝利不可能」の法則が維持されるコード変更のみを許可するため、AIによるコード生成の信頼性が飛躍的に向上します。

Bendを使いたい場合、導入は非常に簡単に行えます。まず公式サイトにあるスクリプトを実行してインストールし、AIエージェントにBendを使用するよう指示するだけです。なお、「AGENTS.md」に以下の通り記述することが推奨されています。

- use `LAWS.bend` to keep important rules

- run `bend PROOF.bend` before committing

Bendはバグのないバイブコーディングに貢献する可能性を秘めた画期的なプログラミング言語です。まだまだ未完成な言語であるため不具合報告を歓迎しているとのことです。

高性能AIモデル「MiMo-V2.6-Pro」と「MiMo-V2.6-Flash」が無償公開される、GPT-5.6 Solに近い性能 - GIGAZINE

GPT-5.2-Codex・Claude Code・Gemini CLI・Mistral Vibeにマインスイーパーを開発させるとこうなる - GIGAZINE

爆速進化したブラウザ「Firefox Quantum」は何がどう変化したのか？

You can read the machine translated English article Bend is a high-speed programming languag… .

本文の著作権はGigazineにあります。