Bend：AIのミスを証明で防ぐ言語
原題: Bend – A language that blocks AI mistakes via proof, on CPU and GPU
なぜ重要か
AIエージェントによるコード生成が普及する中、「読まずに信頼する」ための数学的検証の仕組みが実用的なツールとして登場した点は業界全体の品質保証アプローチに影響を与えうる。
プログラミング言語「Bend」が公開された。C言語並みの実行速度を持ちながら、GPU上では最大100倍の並列処理が可能。最大の特徴は「LAWS.bend」ファイルに記述したルールをLean・Rocq同様の証明検査器で検証する仕組みで、AIエージェントが生成したコードがルールに違反する場合はコミット自体をブロックする。型検査は最大1秒で完了する。
Bendは、AIコード生成時代における「信頼の担保」を目的として設計されたプログラミング言語だ。Pythonに近い構文を持ちながら、ネイティブコードにコンパイルされ、シングルコアでC相当、16コアまたはGPU上では最大100倍の速度で動作する。Apple M4 Maxでのベンチマーク結果を公式サイトで公開している。
最も注目すべき機能が「LAWS.bend」だ。開発者は「絶対に破ってはいけないルール」をこのファイルに宣言形式で記述する。AIエージェントがコードを変更するたびに`bend PROOF.bend`を実行し、すべての法則が数学的に証明できる場合のみコミットが許可される。証明できなければAIは自動的に再試行を強いられる。公式サイトのデモでは、ゲームの「勝利不可能」ルールをLAWS.bendに定義した場合と定義しない場合を比較。LAWSなしではAIのバグがそのままマージされ、LAWSありでは違反コードが完全にブロックされた様子を示している。
型検査器はLeanやRocqと同じ証明検査器として機能するが、中規模コードベースで数分かかることのある既存ツールと異なり、最大1秒で処理を完了する。これにより、AIエージェントが変更ごとにリアルタイムで検証を回せる設計になっている。
並列処理については、スレッドやロック、GPUカーネルの記述が不要で、処理を2分割するだけでBendが自動的に利用可能なすべてのコアに分散・統合する。現在はLinuxとmacOSのバックエンド用途に最適化されており、まだ開発途上であることを開発チームは明示している。インストールは1行のcurlコマンドで完了し、AGENTS.mdへの設定追加でAIエージェントとの連携が始まる。