OpenAI의 CDC 증명 프롬프트 방법론을 따라 30년 된 수학적 최적화 이론의 난제를 5.6 Sol Ultra로 해결함

세 줄 요약: OpenAI가 CDC 증명할 때 썼던 프롬프트 모델링해서 GPT-5.6 Sol Ultra한테 던져줬더니, 1996년부터 안 풀리던 볼록 최적화(convex optimization) 난제를 148분 만에 풀어버림. Lean으로 정식 검증까지 끝냈다. 관련 링크는 글 하단에 다 있음.

참고: 아래 링크된 프리프린트랑 Lean 저장소 내가 만든 거임. 나 UC 버클리 IEOR 학과에서 가르치는 응용수학 박사임. 아직 동료 평가(peer review)는 안 거쳤음. 궁금한 거 있으면 물어봐라. r/math에도 기술적인 요약이랑 내 생각 좀 적어놨으니까 관심 있으면 가서 봐라.

최근에 GPT-5.6 Sol Ultra가 순환 이중 피복 추측(Cycle Double Cover Conjecture) 증명해냈다는 소식 듣고, 나도 그 프로젝트에서 쓴 프롬프트 방식 그대로 가져와서 볼록 최적화 문제에 적용해 봤다. 148분 동안 쉼 없이 돌리니까 GPT-5.6 Sol Pro가 내가 죽어도 못 풀던 하한(lower bound) 증명 핵심 논리를 뽑아내더라. (나도 그동안 여러 환경에서 복잡도 하한 증명하는 연구를 꽤 많이 해왔음). 프롬프트는 한 10페이지 정도 되는데 프리프린트 끝에 붙여놨고(아래 링크 모음 확인), 5.6 Sol이랑 같이 머리 싸매고 만든 거다. 프롬프트 안에 시도해 볼 접근법이랑 모델이 정확히 어떤 식으로 움직여야 하는지 다 때려 박았는데, OpenAI의 CDC 프롬프트 스타일을 그대로 따랐음. 결과적으로 5.6 Sol Pro가 한 방에 문제를 해결해 버렸다. 내가 직접 검증해 보고 Lean으로 정식 증명까지 마쳤는데, 검증 통과했다. (Lean 모르는 애들을 위해 설명하자면, 수학적 명제를 형식화하고 컴퓨터로 검증할 수 있게 해주는 프로그래밍 언어임). 이 문제가 뭐 듣보잡 문제도 아니고, 지난 30년 동안 아무도 안 건드린 문제도 아니다. 나도 1년 넘게 붙잡고 있었고, 내로라하는 연구자들이 관련 연구를 엄청나게 쏟아냈던 문제임. 관련 분야 문제들은 이미 1979년에도 풀렸을 정도로 오래됐는데, 작년에 최적화 학회 갔을 때 이 분야 전문가가 "이거 어떻게 증명할지 감도 안 온다"고 하는 소리까지 들었음.

수학이나 이론 컴퓨터 과학 연구 쪽에서 보면 5.6 Sol은 성능이 진짜 미친 수준으로 좋아진 것 같다. OpenAI가 CDC 추측 증명한 거 봤을 텐데, 내가 운이 억세게 좋았던 거거나 아니면 걔네가 쓴 방식이 다른 난제들 푸는 데도 엄청난 잠재력이 있다는 소리겠지. Ernest Ryu 같은 사람들이 5.4나 5.5로 재미 좀 봤다길래 나도 시도해 봤는데, 그때는 진짜 아무것도 안 나왔음. 여기 내가 5.6 Sol이 결국 성공한 접근법을 시도했던 채팅 기록 공유할 테니까 봐라. (중간에 내 말투가 좀 퉁명스러워도 이해해라. 여러 접근법을 동시에 파고드느라 좀 예민했고, 당시 5.5가 말을 너무 안 들어서 좀 빡쳐있었음!)

링크:

내가 Medium에 쓴 읽기 쉬운 설명:

https://medium.com/@kerger.p/an-ai-assisted-breakthrough-in-convex-optimization-an-optimization-problem-dating-back-30-years-a-db5c631119de

프리프린트, Lean 코드, 전체 프롬프트, 증명 맵, 빌드 방법은 여기서 확인 가능:

https://github.com/PhillipKerger/zero-order-bounds-lean-verification