https://mathstodon.xyz/@tao/113132502735585408

저는 LLM을 실행하기 전에 초기 추론 단계를 수행하는 OpenAI의 새로운 GPT 반복 기능인 GPT-o1을 조금 사용해 보았습니다. 이전 버전보다 확실히 더 유능한 도구이지만, 여전히 가장 고급 연구 수학 작업에는 어려움을 겪고 있습니다.

다음은 몇 가지 구체적인 실험입니다(액세스 권한이 부여된 모델의 프로토타입 버전으로). https://chatgpt.com/share/2ecd7b73-3607-46b3-b855-b29003333b87 에서 저는 문헌에서 적절한 정리(크레이머의 정리)를 찾아내면 풀 수 있는 모호한 단어로 된 수학적 질문에 GPT가 답하도록 요청하는 실험(https://mathstodon.xyz/@tao/109948249160170335)을 반복했습니다. 이전에는 GPT에서 몇 가지 관련 개념을 언급할 수 있었지만 세부적인 내용은 말도 안 되는 헛소리였습니다. 이번에는 크레이머의 정리가 확인되었고 완벽하게 만족스러운 답이 주어졌습니다. (1/3)

https://chatgpt.com/share/94152e76-7511-4943-9d99-1118267f4b2b 에서 저는 새로운 모델에 까다로운 복잡한 분석 문제(이전에 https://chatgpt.com/share/63c5774a-d58a-47c2-9149-362b05e268b4 에서 증명 작성에 도움을 받기 위해 GPT4에 요청했던 문제)를 제공했습니다.결과는 이전 모델보다 좋았지만 여전히 약간 실망스러웠습니다. 새 모델은 많은 힌트와 힌트를 제공하면 올바른(그리고 잘 작성된) 해답을 찾을 수 있었지만 핵심 개념 아이디어를 스스로 생성하지 못했고 사소한 실수도 몇 가지 범했습니다. 완전히 무능하지는 않지만 평범한 대학원생에게 조언을 해주는 것과 거의 비슷한 수준이었습니다.하지만 이는 실제로 무능한 대학원생에 가까웠던 이전 모델에 비해 개선된 것이었습니다.'유능한 대학원생' 수준에 도달하기까지는 한두 번의 기능 개선(그리고 컴퓨터 대수 패키지나 증명 도우미 같은 다른 도구와의 통합)이 더 필요할 수 있으며, 이 시점에서 이 도구가 연구 수준의 작업에서 상당히 유용하게 사용될 수 있을 것으로 보입니다. (2/3)

세 번째 실험으로, 저는 (https://chatgpt.com/share/bb0b1cfa-63f6-44bb-805e-8c224f8b9205 에서) 새로운 모델에게 린으로 결과를 공식화하는 작업(특히, 소수의 정리의 한 형태를 다른 소수의 결과로서 성립시키는 작업)을 시작하도록 요청했지만, 증명은 공식화하지 않고 진술은 공식화할 수 있는 하위 정리로 나누었습니다. 이 모델은 과제를 잘 이해하고 초기 문제 분석을 합리적으로 수행했다는 점에서 유망한 결과를 보였지만, 학습 과정에서 Lean과 그 수학 라이브러리에 대한 최신 정보가 부족하고 코드에 몇 가지 실수가 포함되어 있다는 점에서 한계가 있었습니다.하지만 이 기능의 모델을 Lean과 Mathlib에 맞게 세밀하게 조정하고 IDE에 통합하면 공식화 프로젝트에 매우 유용할 것이라고 상상할 수 있었습니다. (3/3)