Your Spec Has Bugs. Catch Them Before Your Agent Codes. - Rajath Mahendrappa Kotyal, AWS

한 줄 핵심

코딩 에이전트에 넘기기 전 명세의 모호함·충돌·누락을 먼저 검증해야 하며, LLM 재작성과 SMT/solver 검증, 인간 확인을 결합하면 잘못된 코드 생성을 크게 줄일 수 있다.

시간별 요약

1. 0:00
   명세의 작은 문장 차이가 큰 버그를 만든다 이커머스 예시처럼 각각은 그럴듯해 보이는 규칙도 함께 읽으면 서로 모순될 수 있다. 코딩 에이전트는 이런 모호함을 그대로 코드로 옮길 수 있으므로, 입력 단계에서 명세의 품질을 먼저 점검해야 한다.
2. 2:01
   코드보다 먼저 명세를 검증해야 하는 이유 불명확한 프롬프트는 정확도를 20~40% 떨어뜨리고, 유효한 코드라도 60~90%가 여전히 잘못될 수 있다. 그래서 설계 문서처럼 코드 이전 단계에서 충돌과 누락을 찾아내는 검증 과정이 필요하다.
3. 3:02
   LLM 재작성과 SMT 기반 형식 검증 먼저 LLM이 문장을 스스로 다듬고, 실패하면 영어 문장을 SMT 공식으로 바꿔 solver로 모호성 여부를 판정한다. 검증 결과가 유효하면 통과시키고, 충돌이나 이중 해석이 있으면 해당 문장을 다시 점검하게 만든다.
4. 4:01
   여러 번 번역해 해석의 분포를 본다 같은 문장을 7~10번 번역해 서로 다른 해석을 모으고, 논리적 동치 기준으로 군집화하면 LLM이 어떤 가정으로 해석했는지 드러난다. 이렇게 하면 실제 모델 한계인지, 입력이 유발한 혼란인지 구분할 수 있다.
5. 5:05
   모호성은 사람에게 되돌려야 한다 삭제처럼 애매한 문장은 시스템이 임의로 해석하면 안 되며, 보관·비노출처럼 선택지를 제시해 사용자가 결정해야 한다. 충돌은 상충 규칙, 갭은 빠진 규칙이므로 둘 다 인간의 도메인 지식으로 최종 확인이 필요하다.
6. 6:01
   도구의 역할은 대체가 아니라 검증 보조 명세의 정확성을 보증하는 최종 권한은 사용자에게 있고, 도구는 그 전에 문제를 찾는 보조 수단이다. 결국 명세를 먼저 검토하고, 번역을 군집화해 해석 차이를 확인한 뒤, 인간이 결정하거나 필요하면 구현을 보류해야 한다.

실무 인사이트

• 코딩 에이전트를 쓰기 전에는 기능 요구사항을 자연어 문장 단위가 아니라 문장 간 관계까지 포함해 검증하는 절차가 필요하다.
• 프롬프트 개선만으로 해결되지 않는 문제는 SMT/solver 같은 형식 검증을 붙여 모호성·충돌·누락을 자동 탐지하는 방식이 효과적이다.
• 애매한 규칙은 자동 결정보다 선택지 제시와 인간 승인으로 넘기는 편이 재작업과 배포 후 회귀를 줄인다.