CPU・GPUで並列実行できる高級言語「Bend」の開発者Victor Taelin氏は9月17日、「⁠Bend 2」の公開をXで発表した。今回公開されたBendはPythonに似た構文を持ち、開発者がアプリケーションに求める条件を記述することで、AIが生成したコードがその条件を満たすかを数学的な証明で検証できる。

開発者が条件を定め⁠、AIが実装と証明を書く

Taelin氏は、人がコードを書いたり読んだりしなくなる時代にも、AIへ意図を正確に伝える言語は必要になると考えている。Bendは、定理証明支援系Leanのような証明機能をアプリケーション開発に取り入れている。自然言語でAIに指示してコードを作らせる「バイブコーディング」でも、機能の追加・修正後に、プログラムが開発者の求める条件を満たしているか確かめる狙いがある。

Bendでは、この条件をlaw（ルール）として記述する。自然言語の指示だけに頼らず、証明によって検証できる形にする。

言語ガイドには、「⁠どの自然数でも、0を足すと元の数になる」というルールと証明の例がある。以下はコメントと末尾の呼び出し部分を省いた抜粋で、前半のlaw add_zeroがルール、後半のdef add_zero(x)が証明に当たる。

Natは自然数の型、0nは自然数の0を表している。証明では、xが0の場合と、1n+p（自然数pに1を足した数）の場合に分ける。後者では一つ小さい数pに対する証明を利用し、すべての自然数でルールが成立することを示している。

import Base

law add_zero:
  for x: Nat
  {Nat.add(x, 0n) == x : Nat}

def add_zero(x):
  match x:
    case 0n:
      {==}
    case 1n+p:
      %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
      {==}

アプリ開発では、こうしたルールと証明をファイルに分けて管理する。同ガイドが示す運用では、開発者がプログラムに満たしてほしい条件をLAWS.bendに記述し、AIにはこのファイルを変更させない。AIは実装コードを書き、そのコードが条件を満たすことを示す証明をPROOF.bendに記述する。bend PROOF.bendを実行すると、Bendが証明の正しさを検査する。未証明のルールが残っている場合や証明が成立しない場合は、検査に失敗する。

公式サイトは、証明の検査が速く、AIエージェントがコードを変更するたびに証明を確認できる点も利点に挙げている。

その活用例として、同サイトでは、AIがコードを変更しても、あらかじめ定めた条件が保たれるかを確かめるデモを紹介している。このデモでは、「⁠どのように操作しても勝利できない」という条件を設けたゲームを使い、AIに盤面の端から反対側へ移動できる機能の追加を指示した。証明を要求しない例では、勝利できてしまう変更が取り込まれた。証明を要求した例では、AIがゲーム内に壁を追加し、新機能を加えても勝利できないという条件を保った。

ただし、検証の対象は記述したルールに限られ、アプリに必要な条件が漏れなく記述されていることまで保証するものではない。

GPU並列実行を継承し⁠、初代の実行方式を変更

Taelin氏はBendを、Cのような速度、CUDAのような並列性、Pythonのような書き味を持つ言語と説明している。GPU上でも、関数とその周囲の値をまとめて扱うクロージャーや、動的なメモリ確保を利用できる。こうした高級言語の機能に対応しながら、ガベージコレクション（GC）を必要としない設計という。

処理を分割して関数を並列に呼び出すよう記述すると、実行基盤が各コアに処理を割り当てる。開発者がスレッドやロック、GPU用のカーネルを直接書く必要はない。ただし、言語ガイドによると、分割した処理の所要時間が偏ると効率が落ちるため、各処理にかかる時間をおおむねそろえる必要があるという。

なお、Bend 2では、初代Bendから実行方式を変更した[1]。初代のBendプログラムは、そのままBend 2へ引き継ぐことはできないと説明している。

Taelin氏は公開に先立つ投稿で、初代に比べて実行速度が最大100倍になり、プログラムが実行時に扱えるメモリの上限も2GBから8TBへ拡大したと説明している（速度比較の測定条件は、この投稿本文には記載されていない⁠）⁠。

実行ファイルの生成については、コンパイルに時間がかかると説明している。開発を素早く進めるには、Bendに備わるJavaScriptでの実行機能を使うよう案内している。

言語ガイドには、実行ファイルにコンパイルする方法と、JavaScriptで実行する方法が載っている。たとえば、プログラムをhello.bendに保存した場合は、実行方法や出力形式に応じて次のコマンドを使う。

# 実行ファイル「hello」を生成する
bend hello.bend -o hello

# 生成した実行ファイルを起動する
./hello

# ソースコードを検査し、JavaScriptの実行基盤で実行する
bend hello.bend

# JavaScriptファイルとして出力する場合
bend hello.bend -o hello.js

ただし、JavaScriptでの実行は単一コアで動作し、CPU・GPUへの並列化は行われない。

公開初期の制約と⁠、証明を支える実装の課題

言語と実装には、現時点でいくつかの制約がある。数値型は自然数のNat、32ビット符号なし整数のU32、32ビット浮動小数点数のF32に限られ、64ビット整数や64ビット浮動小数点数には対応していない。F32で浮動小数点演算はできるが、その演算が指定した条件を満たすことをBendの証明機能で確かめることはできないとしている。

また、Bendは証明の整合性を保つため、再帰が必ず終了することを確かめる停止性の検査も行っている。ただし、@unsafeでこの検査を無効にした関数は、証明の保証範囲から外れる。

検証を支える実装自体も開発途上にある。Taelin氏は、証明を検査する中核部分（カーネル）などは人手による詳しい監査を受けた一方、実行コードへ変換するコンパイラにはAIが生成した未監査のコードが多く残ると説明した。また、証明の規則を形式的に記述したものとカーネル実装には差があり、現段階では誤った証明を受け入れてしまう不具合があり得るとしている。

Bendのソースコードは、Apache License 2.0でGitHubに公開されている。対応環境はLinuxとmacOSで、GPU実行にはそれぞれCUDA 12とMetalを使う。Windowsには直接対応していないが、Linux環境を動かすWSLを通じて利用できる。

このほか、Taelin氏はBend本体とは別に、証明に特化した有償のAIエージェント「Bender」の提供も予告した。記事執筆時点の公式ページでは、APIを数日以内に公開する予定としている。