生成 AI で JSON Reference コアから形式検証コードまで書いてみた

生成 AI で実装するのは、もう珍しくありません。最近は「ちょっとした関数」どころか、そこそこのまとまりを一気に書いてくれます。

今回試したのは、その先です。

JSON Schema まわりで使う JSON Pointer / local $ref の小さなコア実装を題材にして、TypeScript の実装コードだけでなく、

• unit test
• property-based testing
• Python の参照モデル
• Z3 を使った差分検証コード
• Rocq の proof のたたき台

まで、かなりの部分を生成 AI と対話しながら作ってみました。

結論からいうと、思った以上に広い範囲を書けました。ただし、同時にかなりはっきり分かったことがあります。

それは、AI がたくさん書けることと、その成果物を信用できることは別だということです。

そこで今回は、「AI にかなり広く書かせたコードの束を、どうやって信用できる形に持っていくか」という観点で、今作っている verified-json-reference-parser の話を書きます。

コードは OSS として公開しています。

• GitHub: https://github.com/YChinen/verified-json-reference-parser
• npm: https://www.npmjs.com/package/@ychinen/verified-json-reference-parser

なぜ題材を JSON Pointer / local $ref に絞ったのか

最初にやったのは、問題を小さく切ることでした。

JSON Schema 全体を題材にすると、AI が書いたコードの品質を追うには広すぎます。validation、reference resolution、URI、キーワード評価、エラー報告など、関心事が多すぎて、どこに問題があるのかを切り分けにくいからです。

一方で、JSON Pointer と local $ref は小さいのに境界条件が多いです。

• pointer 文字列の parse
• token の escape / unescape
• array index の扱い
• object / array / primitive の traversal
• # と #/... の local reference 解決

このくらいのサイズだと、AI にかなり書かせても、人間が意味論を追いきれます。しかも、ちょうど「実装は小さいが、雑にやると壊れる」領域です。

今回の Phase 1 スコープはこんな感じです。

このとき強く感じたのは、AI を使うときほど「小さく切る」ことの価値が上がる、ということです。

AI は広い範囲のコードを書けます。でも、広い範囲の正しさをそのまま保証してくれるわけではありません。だから、まず人間側が「検証可能なサイズ」に問題を落とす必要がある。これ自体が、かなり重要な設計判断でした。

実装より先に、意味論を固定した

AI にコードを書かせる前に、先に固定したのは「何を正しいとするか」でした。

このライブラリでは、コア操作はすべて Result<T> を返します。

export type Result<T> =
  | { ok: true; value: T }
  | { ok: false; kind: "InvalidPointer" | "TypeMismatch" | "NotFound" };

失敗は 3 種類だけです。

• InvalidPointer
• TypeMismatch
• NotFound

数は少ないですが、この区別を最初に固定しておくのがかなり効きました。

入力例	結果	理由
parsePointer("/a~2b")	InvalidPointer	~2 は不正な escape
get(["x"], ["foo"])	TypeMismatch	配列に非数値 token を適用
get(["x"], ["01"])	TypeMismatch	index token が canonical でない
get(["x"], ["1"])	NotFound	index は妥当だが範囲外
get({a:{}}, ["a","b"])	NotFound	object key が存在しない
get({a:1}, ["a","b"])	TypeMismatch	primitive の先を辿っている

ここで大事なのは、たとえば "/01" を InvalidPointer にしていないことです。

"/01" は pointer 文字列としては syntactically valid です。問題は、それを array に適用したときに、Phase 1 の index 規則に合わないことです。だからこれは parse の失敗ではなく traversal の失敗で、TypeMismatch になります。

この区別を先に決めておくと、AI が書いたコードを評価しやすくなります。実装コードだけでなく、test も spec も oracle も、「どの入力に対して何を返すべきか」という基準が共有できるからです。

逆に、ここが曖昧だと、AI はいくらでももっともらしい実装を書けてしまいます。全部 NotFound に寄せることも、全部 InvalidPointer に寄せることも、見た目はそれなりに自然です。でも、それでは意味論が固定されません。

つまり、AI に広く書かせるほど、人間が最初に握るべきなのは prompt の細かさより semantic contract の方でした。

実装のコアはかなり小さい

現在の public API の中心は次の 4 つです。

• parsePointer
• formatPointer
• get
• resolveLocalRef

全体の関係はこんな感じです。

内部表現としては、Pointer を readonly string[] にしています。

export type Pointer = readonly string[];

これを選んだ理由は、単純に parse 後の評価を楽にするためです。pointer 文字列をそのまま持ち回るより、escape/unescape 済みの token 列にしてしまえば、後段の get は左から順に token を適用するだけになります。

しかもこの表現は、AI と相性が良かったです。クラスや複雑な内部オブジェクトを作るより、readonly string[] の方が責務が明快で、生成コードも暴れにくい。後から人間がレビューするときも、意味論を追いやすいです。

parsePointer と get は責務を分けた

今回の実装でかなり効いたのは、parse と traversal を最初から分けたことです。

parsePointer は、pointer 文字列を token 列に変換する責務だけを持ちます。

• "" は []
• non-empty pointer は / で始まる必要がある
• segment ごとに ~0 / ~1 を unescape する
• 不正な escape は InvalidPointer

一方の get は、すでに token 列になった pointer を JSON 値に適用する責務だけを持ちます。

• array なら index として解釈
• object なら exact key として解釈
• primitive の先は辿れない

この分離によって、「どこまでが構文」「どこからが意味論か」がかなり明確になりました。

この explicit な分岐は、実装としては少し素朴に見えるかもしれません。でも、semantic core ではこのくらい露骨に読める方が良いと感じました。

AI はしばしば「きれいに抽象化されたコード」を返してきますが、その抽象化が本当に意味論に沿っているかは別問題です。むしろこの規模では、どこで TypeMismatch が出て、どこで NotFound が出るかを、コードから直接追える方が価値があります。

とくに配列 index の扱いは厳密にした

AI 生成コードで揺れやすかったのが、array index の扱いでした。

この実装では、配列 index として受理するのは canonical な 10 進非負整数だけです。

token	判定	理由
"0"	accept	単独の 0 は可
"1"	accept	10進非負整数
"42"	accept	10進非負整数
"01"	reject	leading zero
""	reject	空 token は index ではない
"-1"	reject	digit only ではない
"1.0"	reject	digit only ではない
"foo"	reject	数字列ではない

ここで "01" を reject するのは、JavaScript 的な便利さより意味論の安定を優先しているからです。Number("01") は 1 になりますが、このライブラリではそういう暗黙の正規化はしません。

こういうところは、AI に任せるとわりと揺れます。便利な実装、自然な実装、JavaScript 的に通る実装を書いてくれますが、それが欲しい semantics と一致するとは限りません。

だから、ここも結局は「人間が先にルールを固定する」が大事でした。AI に書かせるにしても、何を reject したいかを明確にしておかないと、もっともらしいけどズレたコードが量産されます。

resolveLocalRef は薄い合成に留めた

local $ref の実装も、Phase 1 ではかなり薄くしています。

• "#" は document 全体
• "#/..." は pointer として解釈
• それ以外は未対応

ここで意識したのは、新しい意味論を増やしすぎないことです。resolveLocalRef 自体が複雑な subsystem になると、AI 生成コードの評価も難しくなります。なので、「既存の意味論を薄く組み合わせるだけの層」に留めました。

これもかなり重要な設計判断でした。AI は大きいものも書けますが、大きいものほど「どこがズレているか」の切り分けが難しくなります。だから、新機能を増やすときも、できるだけ新しい semantics を増やさずに済む設計の方が扱いやすいです。

実装コードだけでなく、検証コードもかなり AI に書かせた

今回いちばん面白かったのはここです。

AI に書かせたのは TypeScript の実装だけではありませんでした。

• unit test
• property-based testing
• Python の spec
• Z3 オラクル周辺
• Rocq proof のたたき台

まで、かなりの部分を対話しながら作れました。

最初は「実装の補助」くらいを想定していたのですが、実際には「プロジェクトのかなり広い部分を書ける」が近かったです。

ただし、ここで一気に不安も増えました。

実装コードも、検証コードも、spec も、proof のたたき台も、全部 AI がある程度書けるなら、何を基準に信用すればいいのか。

ここで必要だったのは、「それぞれを単独で信用しない」ことでした。むしろ、

• semantic contract を先に置く
• スコープを小さく保つ
• 別レイヤの成果物を相互照合できるようにする

という構造の方が重要でした。

AI に幅広く書かせるほど、「個々のコードの質」より「それらが相互にズレたときに気づける構造」の価値が上がる、というのはかなり大きな発見でした。

じゃあ、どうやって信用したのか

やったことを雑に言うと、「1 つの強い保証に賭けない」です。

1. unit test で境界条件を固定する

まず unit test で、曖昧にしたくない境界条件を固定しました。

• invalid ~ escape は InvalidPointer
• leading zero の array index は TypeMismatch
• object key 不在は NotFound
• "/" は空文字キーを指せる

unit test の役割は「正常系チェック」より、「意味論の境界を executable に固定する」ことでした。

2. PBT で get と参照モデルを大量比較する

get のような evaluator は、手書き test だけではどうしても抜けます。そこで fast-check を使って、

• 小さな JSON 値
• 嫌な token 語彙
• 長さ制限付き token 配列

を生成し、実装の get と参照モデル specGet の Result を大量比較しました。

これは「落ちないか」ではなく、「spec と exactly same result か」を見ているので、かなり効率が良いです。

3. Python spec と Z3 で差分検証する

さらに、Python の参照モデルと Z3 ベースのオラクルを置き、TypeScript 実装との差分検証を回しています。

ここでよかったのは、一度見つかった差分を regression corpus に育てられることです。AI と一緒に実装を進めていると、あとで別の生成結果に差し替えたくなることがあります。そういうとき、差分ケースが資産として残っているのは強いです。

4. Rocq は「全部証明」ではなく、pointer 周辺の不変条件を押さえる

Rocq については、現時点で主に押さえているのは次のような性質です。

• token escape/unescape の往復性
• pointer parse/format の往復性

つまり、Rocq が今カバーしているのは主に pointer 周辺の不変条件です。get 全体や resolveLocalRef 全体を end-to-end で完全証明しているわけではありません。

このあたりは、むしろ正直に書く方がよいと思っています。実際の保証はこんな layered structure です。

レイヤ	役割	限界
unit test	境界条件を固定する	網羅はしない
PBT	実装と spec のズレを大量探索する	証明ではない
Python spec	読みやすい参照モデル	実装そのものではない
Z3 oracle	concrete case の差分検証	汎用証明器ではない
Rocq	pointer 周辺の不変条件を機械証明	現時点で全 evaluator は未証明

「全部を 1 つの手法で保証する」より、「それぞれに合った検証を重ねる」方が、今の開発段階ではかなり現実的でした。

実際に効いたのは、形式検証そのものより「検証しやすい設計」だった

今回やってみて一番大きかった学びはこれです。

形式手法そのものももちろん有効でした。でも、それ以上に効いたのは「検証しやすいように設計すること」でした。

たとえば、

• Pointer を readonly string[] にする
• parse と traversal を分ける
• array index parser を internal helper に閉じる
• public API を小さく保つ
• resolveLocalRef を薄い合成に留める

といった判断は、全部「あとで検証しやすいか」に効いています。

AI コーディングでは prompt の工夫も大事ですが、それ以上に「問題をどう分解するか」が効く場面が多かったです。責務分割がはっきりしていると、AI が多少違う書き方をしてきても、人間がレビューしやすいし、差分検証にもかけやすい。

逆に、設計が曖昧だと、AI はもっともらしいコードをいくらでも返してきます。その中から「欲しかった semantics はこれだ」と見抜くのはかなりしんどいです。

なので今回の感覚としては、「AI にうまく書かせる」より「AI が書いたコードを検証しやすいサイズに切る」方が再現性が高い、でした。

「形式検証で全部安心」ではなかった

ここは誤解を避けたいところです。

今回やったことは、形式検証で全部安心になった、という話ではありません。むしろ、

• どこまで意味論を固定したか
• どこまで proof が届いているか
• どこからは差分検証や test に任せているか

を明示できるようになった、という方が正確です。

これは生成 AI を使うときには特に重要だと思っています。AI はかなり広く書けますが、「どこまで信用してよいか」を自動ではラベル付けしてくれません。だから、保証範囲を明示すること自体が、開発上の成果になります。

OSS として公開している

このプロジェクトは OSS として公開しています。

• GitHub: https://github.com/YChinen/verified-json-reference-parser
• npm: https://www.npmjs.com/package/@ychinen/verified-json-reference-parser

実装コードだけでなく、

• tests
• property-based testing
• verification/z3
• proof/rocq

まで含めて見られるので、「AI と一緒にどういう形で積み上げたか」を追いやすいと思います。

おわりに

今回やってみて面白かったのは、AI がどこまで書けるかそのものより、AI が書いた「実装と検証コードの束」をどう信用できる形にするかでした。

実装だけなら、生成 AI はかなり速く書けます。しかも今は、test も spec も差分検証コードも proof のたたき台も、かなりのところまで付き合ってくれます。

でも、だからこそ人間側に残る仕事もはっきりしてきます。

• 問題を小さく切る
• semantic contract を先に置く
• 責務境界を明確にする
• 相互照合できる検証レイヤを作る

このあたりは、少なくとも今のところ、まだ人間が握っていた方が強いと感じました。

次に進めるなら、URI 解決や external reference に広げることになります。ただ、その前に、今の Phase 1 の semantic core をもっと固める余地もあります。

少なくとも今回の題材では、「AI に書かせること」より「AI が書いたものをどう検証可能にするか」の方が、本質的で面白い問題でした。