리드 칼리지에서 수학과 컴퓨터과학을 전공하고 인텔과 텐스토렌트에서 CPU 형식 검증을 맡았던 제이 크루어가 9월 15일 올린 글은 나비에-스토크스 같은 수학 결과를 LLM 에 가장 유리한 경우로 인정하면서도, 그것은 엄밀한 명세와 린(Lean) 같은 검증기가 이미 있는 분야였기 때문이라고 적어요. 실제 소프트웨어 회사들은 모델 점수보다 훨씬 낮은 하위 사분위 엔지니어를 계속 고용하고 있고, 보상 조작을 막으려면 도메인 전문가가 쓴 명세가 필요한데 CPU 프로젝트에서는 검증 엔지니어가 설계 엔지니어의 3배에서 5배에 이르며, 사람 검토도 xz 백도어와 미네소타대 위선자 커밋처럼 뚫린 전례가 있어 결국 사람 조율자에게 병목이 걸린 값싼 에이전트 무리가 현실이 되고 그 일은 딥시크 V4.1 플래시 같은 저가 모델로도 충분할 수 있다는 것이 논지예요. 해커뉴스 595개 댓글에서는 게임과 웹 개발자들이 최전선 모델로 단위 테스트를 대량 생성해 버그율이 역대 최저라고 반박했고, 그 테스트가 맞는 속성을 검사하는지는 어떻게 아느냐는 재반박과 함께 판단은 자동화되지 않는다는 말이 AI 역사에서 늘 깨져 왔다는 지적, 실패 비용이 낮은 곳도 실패를 싸게 감지하지는 못한다는 지적이 맞섰어요.
- LLM
- 대규모 언어 모델. 챗GPT·클로드처럼 글을 읽고 쓰는 AI 모델
- CPU
- 컴퓨터의 중앙 처리 장치. 여기서는 그 칩을 설계하고 검증하는 프로젝트
- 린(Lean)
- 수학 증명이 논리적으로 맞는지 기계로 확인하는 정리 증명 도구
이 글의 실무적 함의는 에이전트가 코드를 쓸수록 비용이 명세와 검증 쪽으로 옮겨 간다는 점이라, 에이전트가 스스로 만든 테스트를 통과했다는 사실을 검증으로 치지 말고 어떤 속성을 검사할지 정하는 일과 그 테스트를 읽는 일을 시니어의 핵심 업무로 두는 편이 안전해요.
- 글쓴이의 논지 수학 결과는 명세와 검증기가 이미 있는 최선의 경우이고, 실제 소프트웨어 회사는 모델보다 낮은 점수를 받을 엔지니어를 계속 고용하며, CPU 프로젝트처럼 검증 인력이 설계 인력의 3배에서 5배가 드는 비용이 병목이라고 적었어요. dank.systems (Jay Kruer)
- 해커뉴스 반론 게임과 웹 개발자들은 최전선 모델로 단위 테스트를 대량 생성해 버그율이 역대 최저라고 반박했고, 다른 쪽에서는 그 테스트가 맞는 속성을 검사하는지 어떻게 아느냐고 되물었어요. Hacker News