Bend、lawとproofでagentの変更を機械検査してGPU実行
これは何?Bendは、Python風の構文、dependent typeによる証明、native CPU/GPU実行を一つにした新しいprogramming languageです。
LAWS.bendへ守る性質を書き、agentが実装とPROOF.bendを作り、compilerが証明を検査します。projectはsingle-coreでC相当、同じbinaryをmulti-coreやGPUで並列実行できるとしていますが、性能値はproject側のbenchmarkです。証明が保証するのは記述したlawだけで、作者も未指定の挙動までは守れないとdiscussionで明言しています。
形式証明はagentが意図を理解した証拠ではなく、人が明文化した不変条件を守る強いgateです。仕様化できない期待、law同士の整合、benchmarkの再現性は別にreviewする必要があります。
- 読むべき人
- programming language researcher、AI coding platform engineer、GPU programmer、formal methods利用者
- HN
- 588 points / 301 comments