Djinnlangは、証明可能なほど曖昧さのない仕様の背後でLLMをコンパイラに組み込んだ

プログラマーはますます形式仕様を書き、その実装をLLMに任せ、各実装が仕様に一致することを証明するようになっている。そこまで極端に進むと、仕様言語が新しいプログラミング言語になる——しかしその置き換えを妨げる問題が一つある。二つのプログラムが同じ仕様を満たしながら異なる振る舞いをすることがあり得るため、どちらの振る舞いを得たのかを知るには、依然として誰かが生成コードを読まなければならない。

Djinnlangの答えは非曖昧性制約である。LLMは、その実装が仕様を満たすことを証明するだけでなく、同じ仕様を満たす他のあらゆる実装が同一の入力に対して同一の出力を生み出すことも証明しなければならない。これが抜け穴を塞ぐ。生成されたコードは読む必要がなくなり、いつでも仕様から再生成でき、信頼できないモデルがコードを書いても検証器がその仕事を厳密に検査できる。

この仕組みにより、LLMは事実上コンパイラツールチェーンの一部となる。Djinnlangのプログラムは仕様のみで構成され、プログラマーは実行可能なコードを一切書かない。従来のコンパイラの代わりに、シンボリックトランスレータが各仕様をDafnyのスタブと証明義務に変換し、ドライバハーネスがLLMを統制して実装と証明を埋めさせ、そのすべてをDafny検証器が検査する。

このパラダイムが実現可能である証拠として、著者らはDjinnlangがセルフホスティングであることを示す。LLMがDjinnlangトランスレータをそれ自身の仕様から実装し、その再実装が自らを検証した。

仕様が曖昧でないことを証明し、その後、信頼できないLLMをコンパイラのバックエンドとして使えるようにする

ある仕様のすべての実装が同一に振る舞うなら、生成されたコードを読んでも、プログラマーが行動に移せる情報は何も増えない。

決定性を証明することでモデルが変更できる範囲が制限されるため、信頼できないモデルがコードを書いても、信頼は検証器が担うことができる。

検証済みのコードはいつでも仕様から再生成できるため、維持とレビューを要する資産ではなくなる。

正しさの証明と並んで非曖昧性の証明を要求することは、モデルに余分な作業を課すが、「正しく見える」を機械的に検査された主張へと変える。

生成が安価で信頼が乏しい場合には、人間の成果物を一段上のレベルへ移す。仕様をプログラムとし、決定性を証明義務とし、コードを使い捨てのビルド成果物として扱う。

2026年9月21日にarXivへ投稿された本論文は、このパラダイムを複数の例で実証し、セルフホスティングを報告している。LLMがDjinnlangトランスレータをその仕様から実装し、その再実装が自らを検証した。著者らはこの結果を、AI制御の強い形態——信頼できないモデルが書き、検証器が決定する——として位置づけている。