번역가의 딜레마: 코드가 인간의 언어를 만날 때

당신이 거대한 디지털 도시를 건설하고 있다고 상상해 보십시오. 교통 흐름을 유지하고 건물을 바로 세우기 위해서는 모든 길모퉁이와 마천루에 규칙서가 필요합니다. 소프트웨어의 세계에서 이 규칙서를 "형식적 명세(formal specifications)"라고 부릅니다. 이것은 컴퓨터가 특정 코드 조각이 무엇을 해야 하는지, 그리고 절대 해서는 안 되는 일이 무엇인지를 정확하게 알려주는 정밀하고 수학적인 지침입니다. 이를 디지털 세계의 깨지지 않는 물리 법칙이라고 생각하십시오. 문제는, 이러한 법칙을 쓰는 것이 매우 어렵다는 점입니다. 이는 대부분의 인간 프로그래머가 지루하고 오류가 발생하기 쉽다고 느끼는, 완전히 다른 언어를 말하는 것과 같은 수준의 정밀함을 요구합니다.

"자동 형식화(Autoformalization)" 문제가 등장합니다. 이것은 "리스트가 너무 커지지 않게 해줘"와 같은 인간의 모호한 자연어 아이디어를 엄격한 수학적 코드로 자동 변환하려는 탐구입니다. 수년 동안 과학자들은 인공지능(AI), 특히 대규모 언어 모델(LLM)을 번역가 역할을 하도록 사용하려고 시도해 왔습니다. 이 AI 모델들은 거의 모든 글을 읽은 초지능적인 다국어 능력자와 같습니다. 이들은 문장의 의미를 추측하는 데 탁월합니다. 하지만 여기 함정이 있습니다. AI에게 모호한 인간의 생각을 엄격한 법률 계약서로 번역하라고 요청하면, 종종 환각(hallucination)을 일으킨다는 것입니다. 존재하지 않는 규칙을 만들어내거나, 전체 시스템을 망가뜨릴 수 있는 아주 작은 디테일을 놓치거나, 혹은 "아마도"라는 말을 확신에 찬 "반드시"로 번역하기도 합니다. 이 논문이 다루는 핵심 질문은 이것입니다: "리스크가 높고 인간의 지침이 모호할 때, 우리는 어떻게 AI 번역가를 신뢰할 수 있는가?"

몬티(Monty)를 만나보세요: AI의 숙제를 검사하는 탐정

이 논문은 Monty라고 불리는 새로운 프레임워크를 소개합니다. 이 시스템은 AI가 생성한 코드 규칙을 위한 회의적이고 세심한 편집자가 되도록 설계되었습니다. 연구진(위스콘신 대학교 매디슨 캠퍼스와 일리노이 대학교 연구진)은 단순히 AI에게 문장을 코드로 번서달라고 요청하는 것만으로는 충분하지 않다는 것을 깨달았습니다. 만약 당신이 AI에게 "리스트가 비어 있어야 한다"를 번역하라고 하면, AI는 그것이 "리스트에 항목이 0개 있다"는 뜻인지, 아니면 "리스트에 아무런 항목도 없다"는 뜻인지 추측할 수 있습니다. 둘 다 맞는 말처럼 들리지만, 컴퓨터 코드에서는 매우 다른 의미를 가질 수 있습니다.

Monty는 AI가 내놓은 첫 번째 답을 그냥 믿지 않습니다. 대신, 일련의 테스트를 수행하는 탐정처럼 행동합니다. 이야기는 다음과 같이 진행됩니다.

1. AI가 용의자 무리를 생성합니다
먼저, Monty는 대규모 언어 모델에게 자연어 단언(human sentence)을 형식적 코드로 번역하도록 요청합니다. AI는 단 하나의 답만 주는 것이 아니라, 한 무리의 "후보(candidate)" 번역본들을 생성합니다. 어떤 것은 완벽할 것이고, 어떤 것은 약간 어긋날 것이며, 어떤 것은 완전히 틀릴 수도 있습니다.

2. "퍼즈(Fuzz)" 테스트: 코드를 부수기
다음으로, Monty는 이 후보 번역본들을 "퍼징(fuzzing)"이라 불리는 스트레스 테스트에 통과시킵령합니다. 로봇이 코드가 충돌하거나 이상하게 작동하는지 확인하기 위해 무작위적이고 거친 입력값을 던지는 상황을 상상해 보십시오.

• 만약 후보 번역본이 컴퓨터를 충돌시키거나 에러를 발생시키면, Monty는 즉시 이를 폐기합니다.
• 만약 번역본이 작동은 하지만 원래의 인간 문장 논리와 일치하지 않는다면, 낮은 점수를 받습니다.
• 결정적으로, Monty는 인간의 문장이 옳다고 가정하지 않습니다. 때때로 프로그래머는 실제로 틀린 규칙(버그가 있는 규칙)을 작성하기도 합니다. Monty는 "유효한" 번역이 "버그가 있는" 규칙의 번역일 수도 있다는 점을 인지할 만큼 똑똑합니다. Monty는 문맥에 가장 잘 맞는 가장 가능성 높은 정확한 번역과 가장 가능성 높은 틀린 번역을 모두 찾아내어 비교합니다.

3. "절(Clause) 커버리지" 체크: 역번역
이것이 Monty의 비밀 무기입니다. AI 번역이 정말로 충실한지 확인하기 위해, Monty는 **절 커버리지(clausal coverage)**라는 영리한 기술을 사용합니다. Monty는 AI의 형식적 코드를 가져와서 AI에게 그것을 다시 평이한 영어로 번역하도록 요청합니다. 그런 다음, 이 새로운 영어 문장을 원래의 인간 문장과 비교합니다.

• AI가 원래 문장의 일부를 놓쳤는가?
• AI가 없던 내용을 추가했는가?
• AI가 의미를 변경했는가?
  AI는 두 문장의 조각(절)들이 얼마나 잘 일치하는지에 따라 점수를 부여하는 판사 역할을 합니다. 만약 역번역된 문장이 핵심적인 디테일을 놓쳤다면, 점수는 떨어지고 해당 후보는 걸러집니다.

4. 최종 결전: 능동 학습(Active Learning)
때때로 AI가 겉보기에 완벽해 보이고 모든 테스트를 통과하는 두 개의 후보를 생성하지만, 그 둘이 미세하게 다른 의미를 가질 때가 있습니다. 이것이 바로 인간 언어의 "모호함"이 발목을 잡는 순간입니다. 이런 드문 경우에 Monty는 추측하지 않습니다. 대신 능동 학습을 사용합니다. Monty는 두 후보가 서로 다르게 행동하게 만드는 특정 시나리오("구별되는 평가값", distinguishing valuation)를 찾아냅니다. 그런 다음 인간(또는 시뮬레이션된 오라클)에게 간단한 질문을 던집니다: "이 구체적인 경우에, 당신이 실제로 의도한 규칙은 무엇입니까?" 인간이 승자를 선택하면, Monty는 올바른 번역을 확정합니다.

Monty가 발견한 것

연구진은 Java 코드(대중적인 프로그래ミング 언어)와 관련된 541개의 서로 다른 작업을 대상으로 Monty를 테스트했습니다. 그들은 실제 삶의 복잡함을 처리할 수 있는지 확인하기 위해 완벽하게 작성된 규칙과 의도적으로 망가진 규칙이 모두 포함된 데이터셋을 사용했습니다.

결과는 유망했습니다. Monty의 도움 없이 AI가 자연스럽게 번역하게 두었을 때, 정확도는 괜찮았지만 완벽하지는 않았습니다. 예를 들어, Qwen2.5-Coder라는 특정 모델을 사용할 때, 가공되지 않은 AI는 한 데이터셋에서 약 **75%**의 확률로 번역을 맞혔습니다. 하지만 Monty가 개입하여 답변을 필터링하고 검증했을 때, 그 정확도는 **91.6%**로 뛰어올랐습니다. 또 다른 데이터셋에서는 **64%**에서 **85%**로 상승했습니다.

이 논문은 Monty가 특히 "정밀도(precision)" 문제를 해결하는 데 탁-월하다고 제안합니다. 이는 Monty가 "여기에 올바른 규칙이 있습니다"라고 말할 때, 단순히 AI에게 묻고 첫 번째 답을 받아들일 때보다 훨씬 더 신뢰할 수 있음을 의미합니다. Monty는 올바른 답을 너무 많이 버리지 않으면서(높은 "재현율(recall)"을 유지하면서) 이 일을 해냈습니다.

Monty가 하지 않는 것

이 논문이 주장하는 바가 아니라는 점을 아는 것도 중요합니다. Monty는 모든 프로그래밍 문제를 해결하는 마법 지팡이가 아닙니다.

• Monty는 전체 소프트웨어 프로젝트의 고차원적인 "의도"(예: "소셜 미디어 앱을 만들어줘")를 파악하려 하지 않습니다. 대신 개별 코드 조각에 대한 특정되고 국소적인 규칙을 번역하는 데 집중합니다.
• Monty가 모호함의 문제를 영원히 해결했다고 주장하지 않습니다. 때때로 인간의 입력이 너무 모호해서 Monty조차 인간의 개입을 통해 명확히 해야 할 때가 있습니다.
• 저자들은 프로그래머가 작성한 모든 규칙이 옳다고 가정해서는 안 된다는 점을 명시적으로 주장합니다. 많은 기존 도구들은 규칙이 작성되었다면 그것이 반드시 참이라고 가정했습니다. Monty는 이를 거부하며, 때로는 규칙이 실패하는 것을 찾아내는 것이 버그를 증명하는 목표가 될 수 있음을 보여줍니다.

결론

결국, Monty는 미래의 코드 작성이 단순히 AI에게 일을 시키는 것만이 아님을 시사합니다. 그것은 AI가 아이디어를 생성하되, 스마트하고 엄격한 프로세스가 그 아이디어를 현실과 대조하여 검증하는 시스템을 구축하는 것에 관한 것입니다. AI의 창의성과 테스트의 회의주의, 그리고 "역번역"의 정밀함을 결합함으로써, Monty는 인간 개발자의 모호하고 복잡한 생각을 디지털 세계의 깨끗하고 깨지지 않는 법칙으로 바꾸는 경로를 보여줍니다. 이 논문은 우리가 아직 그 단계에 완전히 도달하지는 못했을지라도, 이러한 "자기 검토(check-your-work)" 접근 방식이 AI를 소프트웨어 개발의 신뢰할 수 있는 파트너로 만드는 데 있어 중요한 진전임을 시사합니다.