AIが書いたログイン処理を数学で証明　約5,000行の通販サイトで試す

AIにアプリのコードを丸ごと書かせる開発が増えています。1回の作業で数万行から数十万行のコードができることもあり、人がすべての行を読んで確かめるのは、現実的ではなくなりつつあります。今回の発表は、AIが書いたコードを「仕様どおりか」を証明で確かめる方法についてです。開発の現場に関係しない人には、今すぐ変わることはありません。

Microsoft Researchのブログによると、PDD Kit（ピーディーディー・キット）は、人の意図を「仕様」に書き直し、AIのコードがその仕様をすべての入力で満たすことを証明する道具です。ここでいう仕様とは、「このプログラムは何をすべきか」を厳密に書いた約束事のことです。証明が届かない部分は、テストで確かめるとしています。

PDD Kitは、GitHubのSpec Kit（仕様づくりを支える公開ツール）と似た位置づけと説明されています。Spec KitはMITライセンスで公開されたオープンソースです（GitHubのSpec Kitのページ、11/7確認）。

証明に使うのは、Verus（ヴェラス）という証明言語です。Rustというプログラミング言語のための言語で、Microsoft Researchを含む複数の大学や研究機関が共同で開発しています。PDD Kitは、今のところこのVerusで証明を組み立てます。

ログイン処理の証明で、既存のバグも見つかった

検証の対象は、Rustで作られた通販サイト「Pet Store」のログイン処理です。バックエンドはAxumとSQLite、画面はLeptosで書かれ、WebAssemblyにコンパイルされています。全体で約5,000行で、在庫、割引、注文、決済も扱います。ただ、今回はログインに絞って検証しました。

開発者がAIに渡した依頼は、2文だけでした。「正しいパスワードのときだけトークンを発行すること」と、「管理者のアカウントにだけ管理者用のトークンを発行すること」です。トークンは、ログイン後の本人確認に使われる許可証のようなものです。

結果として、Verusはコードを堅くしただけでなく、既存のバグも見つけました。そのうえで、仕様に照らしてログインの不具合がないことを証明できたとしています。開発者は意図を確かめただけで、生成されたコードを1行ずつ読むことはなかったそうです。

仕様の書き方にも、注意すべき点がありました。「正しいパスワードのときだけトークンが出る」という条件だけでは、誰も通さないログイン処理でも満たしてしまいます。そこで開発者は、「正しいパスワードなら必ずトークンが出る」も求めました。両方を求めて、初めて両方向に成り立つ条件になります。AIだけに任せると、どちらか一方を黙って選んでしまうおそれがあるとされています。

PDD Kitは、こうした食い違いを計画の段階で質問として出します。開発者は、ソースを開かなくても、答えを選べるようになっています。

証明が届かない部分は、テストで確かめる

証明にも限界があります。PDD Kitが挙げているのは、次のような部分です。

• bcryptによるパスワードの暗号化（ハッシュ化）、sqlxによるデータベース操作、jsonwebtokenによるトークンの署名は、証明の外にあるライブラリの中の処理です。
• データベースの今の中身や現在の時刻は、プログラムの外から入ってくる情報で、証明できません。
• 処理が終わるか、どのくらい速いかは、仕様に含まれていません。
• エラーメッセージが分かりやすいかなど、人が判断する部分です。

証明の外にある部分は、テストで確かめます。ユニットテスト（部品ごとの試験）や、画面を端から端まで動かすテストが使われます。ブラウザを操作するAIや、パソコンの画面を操作するAIも使えるとしています。ただし、テストが通ったことは「試した入力では動いた」という証拠にとどまります。そのため、PDD Kitは証明とは分けて扱っています。

証明とテストの境目は、TCB（信頼の基盤）と呼ばれます。証明が前提として信じるコードのことです。PDD Kitは、この境目をはっきりさせて、一つひとつを人が承認するよう求めます。

編集部の見方では、この仕組みが効くのは、仕様をどこまで言葉にできるかにかかっています。ログインのように「何が正しいか」を一文にしやすい機能ほど、向いているように見えます。一方で、画面の使いやすさや処理の速さは、今回の証明の対象ではありません。