Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation

당신이 매우 똑똑하고 박식한 로봇에게 복잡한 기계를 위한 엄격하고 수학적인 레시피를 가르치려 한다고 상상해 보세요. 이 기계는 "분산 시스템"(Amazon이나 Microsoft를 실행하는 클라우드 서버와 같은 것)이며, 레시피는 **TLA+**라고 불리는 특별한 언어로 작성됩니다.

이 언어는 고도의 집중력을 요하는 퍼즐과 같습니다. 만약 기호 하나를 놓치거나 논리가 아주 조금이라도 틀리면, 레시피 상에서는 제대로 작동할지 몰라도 실제 상황에서는 시스템이 붕괴할 수 있습니다. 문제는 이 레시피를 손으로 직접 쓰는 것이 어렵고 느리다는 점입니다. 그래서 연구자들은 질문했습니다: "현대적인 AI(거대 언어 모델, LLM)에게 우리 대신 이 레시피를 쓰게 할 수 있을까?"

이 논문은 그 질문에 대한 첫 번째 대규모 성적표입니다. 연구 결과는 다음과 같으며, 이해하기 쉽게 설명되어 있습니다:

1. "문법 vs 의미"의 격차

연구자들은 30개의 서로 다른 AI에게 평이한 영어 설명을 바탕으로 TLA+ 레시피를 작성하도록 요청했습니다.

• 좋은 소식 (문법): 약 **26%**의 경우, AI가 겉보기에 올바른 레시피를 작성했습니다. "철자 검사기"(SANY라고 불림)는 "좋습니다, 단어와 기호가 올바른 순서로 배치되어 있습니다"라고 말했습니다.
• 나쁜 소식 (의미): 하지만 실제로 레시피를 "논리 테스터"(TLC라고 불림)에 통과시켜 실제로 작동하는지 확인했을 때, 이를 통과한 비율은 **8.6%**에 불과했습니다.

비유: 어떤 학생에게 법률 계약서를 쓰라고 시켰다고 상상해 보세요. 학생은 완벽한 철자와 문법을 사용하지만(26% 성공), 그 학생이 쓴 계약서는 원래 의도와 정반대의 내용을 담고 있거나 중요한 조항을 빠뜨려 법적으로 무용지물이 된 상태입니다(8.6% 성공). AI는 언어의 '외형'을 흉내 내는 데는 뛰어나지만, 그 언어 뒤에 숨겨진 '논리'를 이해하는 데는 자주 실패합니다.

2. 크다고 항상 좋은 것은 아니다

보통 우리는 더 크고 강력한 AI가 더 잘할 것이라고 가정합니다. 하지만 이 연구에서 그것은 사실이 아니었습니다.

• 놀라운 사실: 더 작은 AI 모델(DeepSeek r1:8b)이 거대한 "형님" 모델(DeepSeek r1:70b)보다 훨씬 더 잘 수행했습니다.
• 이유: 작은 모델은 "단계별로 생각하기"(수학 문제를 풀 때 풀이 과정을 보여주는 학생처럼)를 하도록 특화되어 훈련된 반면, 큰 모델은 너무 방대한 일반 인터넷 데이터로 훈련되어 TLA+의 엄격한 규칙에 혼란을 느꼈습니다. 이는 정확하게 수플레를 굽는 법을 아는 전문 요리사와, 모든 요리를 할 줄 알지만 특정 레시피를 지나치게 복잡하게 생각하는 일반 요리사의 차이와 같습니다.

3. "코드 전문가"들의 실패

연구자들은 Python이나 Java와 같은 컴퓨터 코드를 작성하는 것으로 유명한 AI들을 테스트했습니다. 놀랍게도, 이 "코드 전문가"들은 일반 목적의 AI들보다 성적이 좋지 않았습니다.

• 이유: 이 모델들은 세미콜론(;)이나 중괄호({})를 사용하는 코드 작성에 너무 익숙해져 있어서, TLA+ 레시피에 실수로 이러한 기호들을 집어넣었습니다. TLA+에는 이런 기호들이 사용되지 않기 때문에 레시피는 즉시 깨졌습니다. 이는 목수가 시계를 고치려고 하는데, 평소 쓰던 망치를 실수로 가져다 쓰는 것과 같습니다.

4. "단계별(Step-by-Step)" 기법이 가장 효과적이었다

연구자들은 AI에게 도움을 요청하는 네 가지 다른 방법을 시도했습니다. 가장 성공적인 방법은 **"점진적 프롬프팅(Progressive Prompting)"**이라 불리는 방식이었습니다.

• 작동 방식: AI에게 한 번에 전체 레시피를 쓰라고 하는 대신, 조각조각 나누어 요청했습니다: "먼저 제목을 써라. 이제 변수를 써라. 이제 규칙을 써라."
• 결과: 이것이 실제로 작동하는 레시피를 만들어낸 유일한 방법이었습니다(8.6%의 성공률). 이는 집을 짓는 것과 같습니다: 지붕, 벽, 기초를 한 번에 거대하게 만들려고 하면 실패할 가능성이 높지만, 방을 하나씩 만들어 나가면 성공할 확률이 더 높습니다.

5. AI의 "환각(Hallucinations)" 현상

논문은 AI가 반복적으로 저지르는 다섯 가지 구체적인 실수 유형, 즉 "환각"을 발견했습니다:

1. 잘못된 기호 사용: TLA+가 요구하는 일반 텍스트 기호(예: /\) 대신 화려한 수학 기호(예: ∧)를 사용함.
2. 언어 혼합: 다른 프로그래밍 언어에서 쓰이는 세미콜론(;)이나 백틱(`)을 실수로 추가함.
3. 생각 노출: AI가 자신의 "사고 과정"(예: ...)을 최종 레시피에 그대로 붙여넣어 레시피를 망가뜨림.
4. 잘못된 길이: 어떤 경우에는 레시피가 9배나 길게 작성되기도 하고, 어떤 경우에는 거의 아무것도 쓰지 않기도 함.
5. 구조 파괴: 레시피의 "끝" 표시를 누락하여 문서가 완성되지 않은 채로 남겨둠.

결론

이 논문은 현재의 AI는 아직 스스로 신뢰할 수 있는 TLA+ 명세(specification)를 작성할 수 없다고 결론짓습니다. AI는 언어의 외형을 흉내 낼 수는 있지만, 인간 전문가가 모든 줄을 일일이 확인하지 않고는 믿기 어려울 정도로 논리적 오류를 많이 범합니다.

연구자들은 이를 해결하기 위해 다음과 같은 조치가 필요하다고 제언합니다:

• "단계별" 프롬프팅 방식을 사용할 것.
• 거대한 일반 모델보다는 추론에 특화된 작은 모델을 사용할 것.
• AI가 레시피를 실행하기 전에 잘못된 기호(틀린 기호 등)를 자동으로 수정하는 도구를 구축할 것.

그때까지, 이러한 중요한 시스템 레시피를 작성하는 일은 여전히 인간 전문가의 몫이며, AI는 유용하지만 오류가 잦은 보조자의 역할에 머물 것입니다.