Djinnlang, 증명 가능하게 모호하지 않은 명세 뒤의 컴파일러 안에 LLM을 넣다

프로그래머들은 점점 더 형식 명세를 작성하고 LLM이 이를 구현하게 하며, 각 구현이 자신의 명세와 일치함을 증명한다. 그 극단까지 가면 명세 언어가 새로운 프로그래밍 언어가 되지만, 그 교체를 가로막는 문제가 하나 있다. 두 프로그램이 모두 명세를 만족하면서도 서로 다르게 동작할 수 있으므로, 어떤 동작을 얻었는지 알기 위해서는 여전히 누군가가 생성된 코드를 읽어야 한다.

Djinnlang의 답은 모호성 없음 제약이다. LLM은 자신의 구현이 명세를 만족함을 증명하는 것에 더해, 같은 명세를 만족하는 다른 어떤 구현이라도 같은 입력에 대해 동일한 출력을 낼 것임을 증명해야 한다. 이것이 그 허점을 막는다. 생성된 코드는 결코 읽을 필요가 없고 언제든 명세로부터 재생성할 수 있으며, 신뢰할 수 없는 모델이 코드를 작성하는 동안 검증기가 그 작업을 엄격하게 검사할 수 있다.

이러한 구성은 LLM을 사실상 컴파일러 툴체인의 일부로 만든다. Djinnlang 프로그램은 오직 명세로만 구성되며, 프로그래머는 실행 가능한 코드를 결코 작성하지 않는다. 전통적인 컴파일러 대신 기호 번역기가 각 명세를 Dafny 스텁과 증명 의무로 낮추고, 드라이버 하네스가 구현과 증명을 채우는 LLM을 조율하며, 이 모든 것은 Dafny 검증기에 의해 검사된다.

이 패러다임이 실현 가능하다는 증거로, 저자들은 Djinnlang이 자기 호스팅됨을 보인다. 즉 LLM이 Djinnlang 번역기를 자신의 명세로부터 구현했고, 그 재구현이 스스로를 검증했다.

명세가 모호하지 않음을 증명한 뒤, 신뢰할 수 없는 LLM이 컴파일러 백엔드가 되게 하라

어떤 명세의 모든 구현이 동일하게 동작한다면, 생성된 코드를 읽는 것은 프로그래머가 행동에 옮길 수 있는 어떤 정보도 더해 주지 않는다.

결정성을 증명하는 것은 모델이 바꿀 수 있는 범위를 제한하므로, 신뢰할 수 없는 모델이 코드를 작성하는 동안 검증기가 신뢰를 담당할 수 있다.

검증된 코드는 언제든 명세로부터 재생성할 수 있으므로, 유지보수하고 검토해야 하는 자산이기를 그친다.

정확성 증명과 함께 모호성 없음 증명을 요구하는 것은 모델에게 추가 작업을 부과하지만, '맞아 보인다'를 기계가 검사한 주장으로 바꾼다.

생성이 저렴하고 신뢰가 귀할 때는 인간의 산출물을 한 단계 위로 올려라. 명세를 프로그램으로 만들고, 결정성을 증명 의무로 만들며, 코드를 일회용 빌드 산출물로 취급하라.

2026년 9월 21일 arXiv에 제출된 이 논문은 여러 예시에서 이 패러다임을 보여 주고 자기 호스팅을 보고한다. 즉 LLM이 Djinnlang 번역기를 자신의 명세로부터 구현했고, 그 재구현이 스스로를 검증했다. 저자들은 이 결과를 강력한 형태의 AI 통제, 즉 신뢰할 수 없는 모델이 작성하고 검증기가 결정하는 것으로 규정한다.