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

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

Bend
https://bend-lang.com/

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

Bendの主な特徴は以下の通りです。

・高速な実行速度
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はスレッド・ロック・カーネルの記述なしにタスクを複数のコアに分散させることができ、効率的に並列処理を実行します。

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

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

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

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

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

When using Bend:
- run `bend guide` to learn it
- use `LAWS.bend` to keep important rules
- run `bend PROOF.bend` before committing
- parallelize the code whenever possible

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