OpenAI의 수학 관련 포스트는 사실 감사 추적(Audit Trails)에 관한 것이다

OpenAI는 8월 1일, 수학 및 이론 컴퓨터 과학(theoretical computer science) 분야에서 달성했다고 주장하는 10가지 진전을 발표했습니다. 이 결과물들은 차세대 주요 모델인 Astra의 내부 버전에 의해 생성되었으며, 이후 인간의 도움을 받아 원고(manuscripts)로 변환되고 Lean 인증서(Lean certificates)로 공식화되었습니다.

마지막 문장이 가장 핵심적인 역할을 하고 있습니다.

유혹적인 헤드라인은 모델이 "수학을 했다"는 것입니다. 좋습니다, 하지만 그 문구는 유용하게 쓰이기에는 너무 모호합니다. 더 흥미로운 변화는 운영 방식에 있습니다. OpenAI는 단순히 벤치마크 수치나 증명처럼 보이는 답변의 스크린샷을 보낸 것이 아닙니다. 외부에서 검토할 수 있도록 원고(manuscripts), Lean 파일, 그리고 설명이 포함된 추론 흔적(reasoning traces)을 함께 보냈습니다.

이것이 진지한 AI 연구 보조 도구가 작동해야 하는 방식에 훨씬 더 가깝습니다.

주장은 거창하지만, 패키징이 더 중요하다

OpenAI는 Astra가 non-sofic groups, sphere packing, coding theory, lower bounds, Ramsey numbers, quantum parallel repetition 및 해당 분야의 기타 전문적인 영역을 포함하여 수학 및 이론 CS 문제 전반에 걸쳐 새로운 결과를 생성했다고 밝히고 있습니다. 동반된 GitHub 저장소에는 10가지 결과에 대한 Lean 공식화(formalizations)가 포함되어 있습니다.

저는 해당 세부 분야에서 활동하는 수학자가 아니므로, 각 증명의 참신함이나 중요성을 판결하는 척하지는 않겠습니다. 바로 그 점이 핵심입니다. 우리 대부분은 어려운 미해결 문제에 대한 주장된 해결책을 보고, 대상 문장이 올바른지, 결과가 의미 있게 새로운지, 혹은 숨겨진 조건이 목표 지점을 옮겨놓은 것은 아닌지 알 수 없습니다.

Lean 인증서(Lean certificate)가 도움이 되기는 하지만, 증명 검토(proof review)의 사회적 측면을 마법처럼 해결해주지는 않습니다. 그것은 증명 보조 도구(proof assistant) 내부의 정의로부터 공식적인 문장이 도출되는지는 확인할 수 있습니다. 하지만 그 공식적인 문장이 모두가 관심을 가졌던 비공식적인 문제와 동일한지, 혹은 그 결과가 헤드라인을 장식할 가치가 있는지는 스스로 알려줄 수 없습니다.

따라서 여기서 유용한 단위는 "AI의 답변"이 아닙니다. 그것은 검토 패키지(review package)입니다.

이 패키지는 여러 계층으로 구성되어 있습니다.

후보 논거(candidate argument)를 찾아낸 모델 생성 검색(model-generated search)이 있습니다. 전문가가 읽을 수 있도록 사람이 준비한 원고(manuscript)가 있습니다. 기계적으로 정밀한 버전을 검증하는 Lean 정식화(Lean formalization)가 있습니다. 모델의 검색 과정에 대한 서술(narration)이 있는데, 이것이 유용할 수도 있고 그렇지 않을 수도 있지만, 적어도 검토자들에게 최종적으로 다듬어진 증명(proof)과 비교할 수 있는 무언가를 제공합니다.

이는 "따라서 해결되었습니다"로 끝나는 챗봇 대화 기록(chatbot transcript)보다 훨씬 낫습니다.

이것은 에이전트가 수학 이외의 분야에서도 필요로 하는 패턴입니다

개발자들은 이미 덜 화려한 형태로 동일한 문제를 겪고 있습니다.

에이전트가 PR(Pull Request)을 올립니다. 코드가 컴파일됩니다. 설명은 그럴듯하게 들립니다. 운이 좋다면 테스트도 통과합니다. 하지만 진짜 질문은 에이전트가 작업물과 유사한 텍스트를 생성했느냐가 아닙니다. 진짜 질문은 에이전트가 인간이 처음부터 모든 것을 다시 하지 않고도 그 작업을 검토할 수 있을 만큼 충분한 증거(evidence)를 남겼느냐 하는 것입니다.

유용한 코딩 에이전트(coding agent)는 단순히 "수정함"이라고 말해서는 안 됩니다. 변경 사항(diff)을 남겨야 하며, 변경 전의 실패한 테스트, 변경 후의 통과한 테스트, 에이전트가 세운 가정(assumptions), 의도적으로 건드리지 않은 파일들, 그리고 추측이 틀렸을 경우를 대비한 롤백 경로(rollback path)를 남겨야 합니다.

유용한 데이터 에이전트(data agent)는 단순히 "데이터셋을 정제함"이라고 말해서는 안 됩니다. 스키마 차이(schema diff), 삭제된 행 수(dropped-row counts), 이상치 규칙(outlier rules), 변경 전후의 샘플 행, 그리고 최종 테이블을 생성한 쿼리(query)를 남겨야 합니다.

유용한 연구 에이전트(research agent)는 단순히 요약만 해서는 안 됩니다. 출처 링크, 인용 구간(quote spans), 의견 불일치 지점, 그리고 검증할 수 없었던 주장들을 남겨야 합니다.

수학은 증명의 기준이 매우 높기 때문에 이러한 문제를 고통스러울 정도로 명확하게 보여줍니다. 소프트웨어 분야에서 이 문제가 덜 느껴지는 이유는 우리가 형편없는 감사 추적(audit trails)에 익숙해져 있기 때문입니다.

2,000달러라는 숫자에 매몰되는 것은 잘못된 방향입니다

OpenAI는 이러한 문제들의 해결책을 찾는 데 필요한 총 토큰 수가 Sol API 요율로 계산했을 때 대략 2,000달러 정도의 비용이 들 것이라고 말합니다. 이 숫자는 깔끔하고, 주장하는 결과물에 비해 이상할 정도로 작기 때문에 어디에서나 인용될 것입니다.

저는 이 숫자를 주의해서 바라볼 것입니다.

토큰 비용(Token cost)이 프로젝트 비용은 아닙니다. 여기에는 어떤 문제를 시도할지 선택하는 과정, 보고된 경로에 포함되지 않은 실패한 시도들, 인간의 검토(human review), 원고 준비, 정식화(formalization) 작업, 또는 무엇을 발표하는 것이 안전할지 결정하는 기관의 메커니즘 등이 포함되지 않습니다. 내부 회계 방식이 완벽하게 공정할 수도 있고, 그렇지 않을 수도 있습니다. 어느 쪽이든, 숫자는 방향성보다 덜 중요합니다.

방향성은 프런티어 모델(frontier models)이 충분히 유능해짐에 따라, 병목 현상이 생성(generation)에서 검증(verification)으로 이동하고 있다는 것입니다.

이것은 작은 변화가 아닙니다. 이는 희소한 기술이 "모델이 인상적인 것을 만들어내게 할 수 있는가?"에서 "인상적으로 보이는 결과물에 대한 영수증(receipts, 증거)이 있는 워크플로우를 구축할 수 있는가?"로 옮겨감을 의미합니다.

지루한 미래가 유용한 미래다

많은 AI 데모는 공개(reveal) 순간에 최적화되어 있습니다. 모델이 프로그램을 작성합니다. 모델이 퍼즐을 풉니다. 모델이 증명을 찾아냅니다. 모두가 최종 결과물(artifact)을 응시합니다.

제가 신뢰하는 부분은 대개 더 지루합니다. 실행 과정을 조사할 수 있는가? 검증을 다시 실행할 수 있는가? 회의적인 사람이 가장 취약한 연결 고리를 공격할 수 있는가? 시스템이 자신이 아는 것과 단순히 추측한 것을 분리할 수 있는가?

이것이 Lean 파일이 중요한 이유입니다. 형식 방법론(formal methods)이 갑자기 마법이 되었기 때문도 아니고, 모든 영역이 Lean이 될 수 있기 때문도 아닙니다. 그것들이 중요한 이유는 진지한 워크플로우의 형태를 가리키기 때문입니다. 모델이 제안합니다. 시스템이 기록합니다. 인간이 검토합니다. 기계 검증(Machine checks)이 일련의 실수들을 잡아냅니다. 남은 판단은 해당 분야를 이해하는 사람들의 몫으로 남습니다.

이것은 "AI가 수학을 해결했다"라는 말보다 덜 흥미롭게 들립니다.

좋습니다. 흥분은 값싼 것입니다. 감사 추적(Audit trails)이야말로 실제 업무와 접촉했을 때 실제로 살아남을 수 있는 부분입니다.

에이전트(agents)를 위한 교훈이라면, 저는 이것을 가져가고 싶습니다. 모델이 답을 낼 수 있는지 묻지 마십시오. 모델이 답처럼 보이는 무언가를 만들어낼 수 있다고 가정하십시오. 그다음, 그것이 어떤 증거를 남기는지 물으십시오.

그 지점이 바로 유용한 시스템이 마술 같은 속임수와 차별화되는 지점입니다.