[서론] 단 하나의 불꽃이 초원에 불을 붙일 수 있습니다! 증명의 존엄성은 검증 가능성에 있습니다. 이번 GPT-5는 수학적 증거를 코드에 적용합니다.
ChatGPT는 OpenAI의 명성을 회복하여 그 명성을 되찾았습니다!
하사비스가 너무 당혹스럽다고 비판한 후, GPT-5는 실제로 새로운 수학적 결론을 도출해냈습니다.
OpenAI 과학자 세바스찬 부벡은 GPT-5가 에르되시 문제 10개를 해결한 것으로 화제를 모았습니다.
그러나 GPT는 에르되시의 문제를 해결하지 못했지만, 이미 이러한 문제를 해결한 문헌을 찾았다는 점이 지적되었습니다.
그는 나중에 해당 트윗을 삭제하고 누구도 오도할 의도가 없었다고 밝혔다.
얀 르쿤은 이를 "뿌린 대로 거두는 것"이라고 비난했습니다. OpenAI는 자체 GPTard로 인해 피해를 입었습니다.
그 후로 LinkedIn에 올린 그의 게시물은 눈에 띄게 더 단순해졌습니다.
이제 상황은 더 나아졌습니다.
세바스찬 부벡은 "잘못된 비난"을 받았습니다. AI는 실제로 과학적 진보를 가속화하고 있습니다.
놀라운 사건의 전개: ChatGPT가 OpenAI를 "옹호"하다.
어제 이야기는 전환점을 맞았습니다.
프린스턴 대학에서 수학 박사 학위를 받은 보리스 알렉세예프(왼쪽 사진)와 오하이오 주립 대학에서 준교수로 있는 더스틴 G. 믹슨(오른쪽 사진) 은 1,000달러의 보상금을 내건 에르되시 문제 707호가 제안되기 30년 전에 이미 해결되었다는 사실을 발견했습니다.
논문 링크: https://borisalexeev.com/pdf/erdos707.pdf
이 문제는 수학자의 "공허한 탐색"에 가까울 정도로 다소 터무니없는 일입니다.
이 질문에 대한 답은 30년이나 앞선 것이지만, 최근까지 이 문제는 해결되지 않은 것으로 널리 믿어졌습니다!
현재 에르되시 문제 707은 "반증됨"으로 표시되었습니다.
링크: https://www.erdosproblems.com/go_to/707
이번에는 세바스찬 부베크가 상황을 역전시켜 트윗을 올렸습니다.
문헌 검색은 결국 간단한 작업이 아닌 것 같습니다 😅.
숨은 의미는 과거 GPT-5로 10가지 기존 솔루션을 찾는 것이 결코 쉬운 일이 아니었다는 것입니다.
하지만 그보다 더 흥미로운 내용은 다음과 같습니다.
ChatGPT 지원 수학적 증명 - Terence Tao가 엄지손가락을 치켜세웠습니다.
두 수학자 역시 결과에 회의적이었기에, GPT5를 사용하여 Lean에서 정형화된 증명을 생성하기로 결정했습니다. 결국, 그들은 실제로 성공했습니다!
참고⚠️: ChatGPT와 Lean이 공동 연구자로 나열되어 있지만, 논문의 내용은 여전히 저자들이 직접 작성했습니다.
그러나 인간은 이 과정에 많은 노력을 기울여 GPT5에 지속적으로 피드백을 제공하여 공식적인 주장을 개선해 왔습니다.
최근 "에르되시 문제" 웹사이트에서 많은 성공적인 사례가 소개되었는데, 연구자들은 대규모 언어 모델을 사용하여 기존 문헌에서 에르되시 문제에 대한 해결책을 찾았습니다.
테렌스 타오가 이전에 AI를 사용하여 에르되시의 문제에 대한 "기존 답변"을 찾아 개념 증명을 성공적으로 시연했다는 점을 언급할 가치가 있습니다.
테렌스 타오 역시 이 새로운 증명을 주목하며, 이를 컴퓨터 지원 증명의 흥미로운 사례로 여겼습니다.
연구 과정에서 두 수학자는 린이 기존 논문의 진위 여부를 검증하는 데 도움이 될 것이라고 확신했지만, 당시에는 린에 익숙하지 않았고 사용자 인터페이스도 사용자 친화적이지 않다고 생각했습니다.
하지만 ChatGPT는 Lean 코드를 작성할 수 있기 때문에 전체 증명을 바이브 코딩을 통해 공식화하기로 결정했습니다.
이 과정은 약 일주일이 걸렸고 매우 힘들었지만, 예상치 못하게 마지막에는 성공했습니다.
형식적 시스템에서 ChatGPT는 에르되시 추측의 부정을 엄격하게 증명했습니다 .
최종 증명은 26개의 정의, 169개의 보조정리, 그리고 4개의 정리(최종 반례 검증 부분)를 포함하여 6,000줄이 넘는 코드로 구성되었습니다. 일반적인 노트북에서 코드 검증은 30초도 채 걸리지 않았습니다.
여러 차례의 상호작용을 거친 후, 보리스와 더스틴은 대규모 언어 모델의 인터페이스를 린과 깊이 통합하고 이 상호작용 방법에 맞게 적절히 미세 조정할 수 있다면 많은 문제가 크게 완화될 것이라는 결론을 내렸습니다.
사소하고 집중적인 최적화만으로도 "인간과 기계의 협업적 증명" 경험을 더욱 원활하고 자연스럽게 만들 수 있습니다.
테렌스 타오는 이 AI 지원 증명을 높이 평가했습니다. 그는 이것이 연구 논문에서 LLM 산출물을 책임감 있게 활용한 몇 안 되는 사례 중 하나라고 말했습니다.
중요한 점은 LLM에서 생성된 출력이 텍스트에 직접 포함되지 않는다는 것입니다 (설명 목적으로 LLM에서 생성된 Lean 코드 조각을 참조하는 경우 제외).
대신, 이 출력은 완전히 검증 가능한 컨텍스트(이 경우 Lean에서 유형 검사가 가능한 코드를 생성하는 경우)에서만 사용됩니다.
하지만 테렌스 타오는 "린 공식화는 인간 증명을 보완하는 것일 뿐, 인간 증명을 대체할 수 없다"고 강조했습니다.
게다가 그는 과장된 보도도 예상할 수 있었습니다. "이번에 LLM은 정말로 에르되시 문제를 해결했습니다!"
하지만 진실은 훨씬 더 복잡하고 미묘합니다. 결론을 내리려면 전체 이야기를 면밀히 살펴봐야 합니다.
GPT-5는 연구를 주도하고 있으며, 초기 징후가 나타나고 있습니다.
캘리포니아 대학교 어바인 캠퍼스의 수학 교수인 파타 이바니스빌리도 ChatGPT를 해당 논문의 공동 저자로 명시했습니다.
이 새로운 논문은 수학 교수 파아타 이바니스빌리와 중국과학기술대학교(USTC) 2022년 학부 졸업생 신위안 시에가 공동 집필했습니다. ChatGPT가 제1 저자입니다.
이 탐구는 두 사람이 GPT-5 Pro에 공개적으로 이용 가능한 미해결 문제에서 반례를 찾아달라고 요청하면서 시작되었습니다(아래 참조 👇).
- 링크: https://simons.berkeley.edu/sites/default/files/openprobsmerged.pdf
- 제목: 컴퓨터 과학의 실제 분석: 미해결 문제 모음
여러 수치 실험을 거친 후, 지우기와 관련된 비대화 상관 증류(NICD) 문제 에 대한 반례를 제안합니다.
5비트로 정의된 부울 함수는 지우기 매개변수 p = 0.40일 때 5비트 다수 함수의 해당 값보다 엄격하게 큰 E|f(z)| 값을 갖습니다.
그들은 발견 내용을 기록하고 전체 계산 과정을 검증했습니다.
이 결과는 선형 임계값 함수에서 "다수가 가장 불안정하다"는 고전적인 반례를 반영합니다. AI가 알려진 반례 패턴을 새로운 시나리오에 적용하고 검증하는 것만 해도 그 기여도는 여전히 인정할 가치가 있습니다.
링크: https://arxiv.org/abs/1703.07657
이것이 이론 컴퓨터 과학에서 AI의 "불꽃" 입니다. 이전에는 대규모 언어 모델(LLM)이 주로 문헌 검색이나 수치 지원에 사용되었지만 이번에는 구체적이고 제한적이며 검증 가능한 반례가 생성되었습니다 .
또한 UCLA 수학 교수인 어니스트 류는 GPT-5 Pro를 사용하여 볼록 최적화 분야의 미해결 문제를 해결했습니다.
이 모델에 대한 증명 시도의 약 80%가 틀렸지만, 이 모델은 몇 가지 새로운 아이디어를 제안했습니다.
GPT-5 Pro의 구체적인 기여:
- 최종적으로 실현 가능한 증명 접근 방식과 논증 프레임 제시됩니다.
- 잘못된 경로를 신속하게 제거함으로써 탐사 과정이 상당히 가속화되었습니다.
이 작업은 약 12시간이 걸렸고 3일 만에 완료되었습니다. 돌이켜보니, 어니스트 류는 증명이 사실 꽤 간단하다는 것을 깨달았습니다.
ChatGPT에서 생성된 증명의 주요 단계:
어니스트 류는 자신의 기여를 다음과 같이 요약했습니다.
- 잘못된 주장을 걸러내고 올바른 사실들을 모아보세요.
- 유망한 새로운 추론 아이디어를 파악하고 ChatGPT가 이러한 아이디어를 더욱 탐구하도록 안내합니다.
- 전략이 완전히 탐색되었는지 인식하고 언제 다른 방향으로 전환할지 결정하세요.
그는 이 프로젝트를 계속 개발하고, 전문 최적화 이론 저널에 결과를 발표하고, 업데이트와 향후 개발 내용을 공유할 것입니다.
비판을 받은 OpenAI 과학자 Sebastien Bubeck도 비슷한 시나리오를 재현했습니다.
GPT-5는 흥미로운 수학적 결론을 증명할 수 있습니다.
하지만 실제로는 인간이 GPT-5보다 먼저 성공했습니다 :-). 또 다른 저자가 그 격차를 완벽하게 메워 새로운 한계를 증명했습니다.
GPT-5가 제안한 증명:
GPT-5는 이미 연구 가치가 있는 몇 가지 새로운 아이디어를 제시했습니다. 게다가 대부분의 단서어를 스스로 생성하기도 했습니다.
링크: https://github.com/Dicklesworthstone/model_guided_research
AI 지원 연구의 문이 열리고 있습니다.
아마도 역사는 "정말 창피했다"라는 문구가 아니라, qed에 조용히 컴파일된 코드 한 줄을 기억할 것입니다.
참고문헌:
https://x.com/SebastienBubeck/status/1980804267524116569
https://x.com/PI010101/상태/1981014478969033156
https://borisalexeev.com/pdf/erdos707.pdf
https://mathstodon.xyz/@tao/115416211466664814
https://x.com/slow_developer/status/1980990021248160009
본 기사는 WeChat 공식 계정 "New Intelligence" 에서 발췌하였으며, KingHZ가 편집하고 36Kr의 허가를 받아 게시되었습니다.
