요약: 단 한 번의 148분 세션 동안, OpenAI가 CDC(Cycle Double Cover) 증명을 위해 사용했던 프롬프트를 모델링한 GPT-5.6 Sol PRO는 1996년부터 존재해 온 볼록 최적화(convex optimization)의 복잡성 격차를 메우는 증명을 제공했습니다. 이 결과는 Lean에서 형식적으로 검증되었습니다. 모든 링크는 본문 하단에 있습니다. 참고: 저는 아래 연결된 프리프린트와 Lean 저장소의 저자입니다. 저는 응용 수학 박사 학위를 가지고 있으며 UC Berkeley의 IEOR 교수진으로 재직 중입니다. 이 결과는 아직 동료 심사를 거치지 않았습니다. 질문이나 의견을 기꺼이 답변해 드리겠습니다. 관심 있는 분들을 위해 r/math에도 조금 더 기술적인 요약과 생각을 올렸습니다. 수정: 제가 제목을 수정할 수는 없지만, 이것은 Ultra가 아니라 Sol PRO였습니다. 이전에는 codex에서 작업했었는데, 그곳에서는 XHigh보다 높은 레벨이 Ultra였습니다. 하지만 저는 웹 인터페이스에서 이 작업을 했고, 거기서 가장 높은 것이 Pro였으며, 이는 사실 Ultra와 완전히 같지는 않습니다. GPT-5.6 Sol Pro가 Cycle Double Cover Conjecture의 증명을 생성했다는 최근 발표에 따라, 저는 그 프로젝트에서 사용된 프롬프팅 방법론을 볼록 최적화 문제에 적용했습니다. 중단 없이 148시간 동안 작업한 후, GPT-5.6 Sol Pro는 제가 스스로 증명하지 못했던(그리고 제 과거 작업의 상당 부분은 다양한 환경에서 복잡성 하한을 증명하는 것이었습니다) 하한에 대한 주요 논거를 생성했습니다. 저의 프롬프트는 약 10페이지 분량이며 프리프린트 끝부분에 첨부되어 있습니다(아래 링크 모음 참조). 이 프롬프트에는 시도할 접근 방식과 모델이 정확히 어떻게 진행해야 하는지에 대한 내용이 많이 포함되어 있지만, OpenAI의 CDC 프롬프트 스타일 그대로 구축되었습니다. 이를 통해 5.6 Sol Pro는 한 번에 문제를 해결했습니다. 제가 직접 확인한 후, 저는 Lean에서 증명을 형식적으로 검증했으며, 이는 형식 검증 절차를 통과했습니다(낯선 분들을 위해 설명하자면, Lean은 수학적 명제를 공식화하고 계산적으로 검증할 수 있는 프로그래밍 언어입니다).

이 문제와 관련하여, 이것은 아무도 시도하지 않았거나 수년 동안 잊힌 모호한 문제가 아닙니다. 저는 이 문제를 약 1년 동안 간간이 생각해 왔고, 최고의 연구자들로부터 엄청나게 많은 관련 연구가 존재하며, 관련된 설정에서의 동등한 문제들은 오랫동안 해결되어 왔습니다(일부는 1979년까지 거슬러 올라갑니다). 그리고 지난 해 최적화 컨퍼런스에서 이 결과를 어떻게 증명할 수 있을지에 대해 해당 분야 전문가에게 '전혀 모르겠다'는 말을 들은 적도 있습니다. 수학 및 이론 컴퓨터 과학 연구에 있어서, 5.6 Sol은 그 역량 면에서 엄청난 개선처럼 보입니다. 우리는 OpenAI가 CDC 추측에 대한 증명을 본 적이 있는데, 제가 극도로 운이 좋았거나 아니면 그들이 사용한 접근 방식이 다른 많은 미해결 문제에서도 성공할 수 있는 심각한 잠재력을 가지고 있다고 생각합니다. 저는 Ernest Ryu와 같은 사람들이 그것들을 사용하여 성공하는 것을 본 후 이 문제에 5.4와 5.5를 사용하려고 시도했지만, 아무 소용이 없었습니다. 예를 들어, 제가 여기에서 공유할 채팅 기록이 있는데, 거기서 Sol 5.6이 결국 사용하게 된 접근 방식을 시도해 보았고 그것이 마침내 효과가 있었습니다(그때 저는 여러 다른 접근 방식에 대해 병렬로 심층 분석을 하려고 했기 때문에 후속 조치가 짧은 점은 용서해 주십시오, 그리고 당시에는 5.5에 약간 좌절하고 있었습니다!).

링크: Medium에 작성한 접근 가능한 설명 글: https://medium.com/@kerger.p/an-ai-assisted-breakthrough-in-convex-optimization-an-optimization-problem-dating-back-30-years-a-db5c631119de 사전 인쇄본(preprint), Lean 코드, 전체 프롬프트, 증명 지도(proof map), 빌드 지침은 여기에서 확인할 수 있습니다: https://github.com/PhillipKerger/zero-order-bounds-lean-verification ArXiv 사전 인쇄본: 미분 불필요 볼록 최적화에서의 오라클-복잡도 격차 해소: 정확한 함수 값으로부터의 근사 이차 하한(Near-Quadratic Lower Bound from Exact Function Values) 최초 증명을 생성한 원래 중단 없는 148분간의 채팅 기록: https://chatgpt.com/share/6a55aa50-b484-83ea-85c0-c7e7b4bda41c 정확도 요구 사항에 대한 d⁻¹ᐟ² 개선으로 이어진 후속 채팅 기록: https://chatgpt.com/share/6a55ad10-7644-83ea-859e-5483d2e0dff0 제가 구조화한 OpenAI의 CDC 프롬프트: https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98d31/cdc_prompt.pdf /u/pkerger가 r/OpenAI에 제출한 [링크] [댓글]