트윗
테렌스 타오 "현재 AI, 연구 수준 작업을 약간 가속화하는 수준 도달"
작성자
하이룽룽
작성일
2025-11-06 21:15
조회
2592
https://terrytao.wordpress.com/2025/11/05/mathematical-exploration-and-discovery-at-scale/
https://mathstodon.xyz/@tao/115493667607261044
최근 Lean에서 Erdos 문제에 대한 솔루션의 성공적인 "바이브 코딩"에서 영감을 얻었습니다.https://arxiv.org/abs/2510.19804, 나는 Quanyu Tang이 최근에 발굴한 Erdos의 또 다른 문제에 대한 반증(2001년 Pikhurko에 의해)을 공식화하려고 노력했습니다.https://www.erdosproblems.com/613. 이것은 간단한 유한 반례였습니다. 15개 정점에 44개의 간선이 있는 그래프로, 이분 그래프와 최대 차수가 5인 그래프로 나눌 수 없었습니다. Pikhurko의 논문은 9페이지에 불과했고 (더 다양한 매개변수 선택과 적절한 하한을 갖는 더 일반적인 반례도 구성했습니다), 최신 AI 도구에서도 충분히 구현할 수 있을 것으로 보였습니다. 그래서 저는 이 논문을 ChatGPT Pro에 업로드하고, 먼저 비공식적인 언어로 구성을 요약한 다음, 단계별로 공식화하도록 요청했습니다.https://chatgpt.com/share/690a65b3-473c-800e-afa5-e99f78610ee9 (1/4)
초기 단계는 매우 순조롭게 진행되었습니다. ChatGPT는 Pikhurko의 생성을 5차 사례에 맞게 정확하게 특화하고, 생성이 무엇이고 왜 작동하는지에 대한 매우 읽기 쉬운 설명을 제공했습니다. (이 버전의 GPT에서는 모든 질의에 답변하는 데 10분에서 20분이 걸렸기 때문에, 저는 이 작업을 비동기식으로 진행하면서 GPT를 수시로 확인하면서 다른 문제들을 처리했습니다.) 또한 그래프와 문제 진술에 대한 본질적으로 정확한 정의를 공식화하고, 요청된 각 단계에 대해 대부분 작동하는 Lean 코드를 제공했습니다. 제 Lean 저장소에 직접 접근할 수 없다는 점이 다소 제한적이었고, 약간 다른 구문을 사용하는 이전 버전의 Mathlib에서 학습한 것으로 보이므로 모든 것을 유형 검사하기 위해 어느 정도 정리가 필요했지만, 저는 이러한 문제를 해결할 만큼 Lean에 대한 전문 지식을 갖추고 있었습니다. 일부 줄은 전혀 컴파일되지 않았지만, 대부분의 경우 증명해야 할 진술이 충분히 명확해서 다른 증명을 직접 제공할 수 있었습니다. (많은 경우, GPT가 어떤 이유에서인지 사용하지 않았던 `aesop`이나 `grind`와 같은 강력한 추론 전략이 해당 진술을 즉시 처리했습니다.) (2/4)
한 가지 중요한 예외가 있었는데, 그래프에 실제로 44개의 간선이 있는지 확인해야 하는 단계였습니다. 그래프는 서로 분리된 다섯 개의 부분 그래프의 합집합이었는데, GPT는 각 그래프를 다소 정확하게 셀 수 있었습니다(사소한 기술적 수정을 통해). 하지만 합집합의 간선 수가 각 구성 요소 부분 그래프의 간선 수의 합인 이유를 제시하지는 못했습니다. 결국 저는 이 논증의 일부를 제대로 구현하기 위해 (GPT가 제안한 것과는 다른 접근 방식을 사용하여) Mathlib 도구에서 합 유형과 Finset 기수에 대한 정보를 찾는 데 한 시간 정도를 보냈습니다. (이는 제가 Lean에 대해 일반적으로 경험한 바와 일치합니다. 가장 "명백한" 명제가 제대로 공식화하는 데 가장 오랜 시간이 걸리는 경우가 많습니다.)
하지만 이것과 다른 사소한 변경 사항으로 인해 나는 다음과 같은 유형 검사 증명을 얻었습니다.https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/erdos_613.lean(풀 리퀘스트에 요약된 워크플로https://github.com/teorth/analysis/pull/384)(3/4)
이 과정은 이틀에 걸쳐 진행되었지만, 처음부터 끝까지 제 실제 집중력은 두세 시간 정도밖에 필요하지 않았던 것 같습니다. 같은 문장을 수작업으로 공식화하는 통제 실험(더 일반적인 검색 도구와 Github Copilot의 자동 완성 기능을 사용했지만, 프론티어 수준의 AI는 사용하지 않았습니다)은 시도하지 않았지만, 대략 6시간 정도 걸렸을 것으로 추정합니다. 아마도 증명은 훨씬 더 정교했을 것입니다. "바이브 코딩" 증명은 1,125줄로 구성되어 있으며, 그중 많은 부분이 `grind`와 같은 강력한 린 전략으로 이미 구현 가능한 사소한 것들을 증명하는 데 할애되어 있습니다. 하지만 이 결과는 인간의 증명이 불분명하거나 설득력이 없는 결과가 아니었고, 저는 이 실험을 통해 추가적인 린 공식화 경험을 얻었습니다.
요약하자면, 저는 이런 종류의 도구들을 린 타입체킹과 같은 엄격한 검증 방법과 결합하면 단계별로 실행할 때 시간이 많이 소요되는 여러 연구 수준의 작업을 (평균적으로) 약간 가속화하는 수준에 도달했다고 생각합니다. 하지만 여전히 무작위적인 변동과 통합 워크플로우에 대한 장벽이 있어 프로세스가 완전히 원활하지는 않으며, 사용 가능한 출력을 생성하지 못하는 쿼리의 중요하지 않은 부분을 적절히 수정할 수 있으려면 해당 작업에 대한 충분한 전문 지식이 필요합니다. (4/4)
https://mathstodon.xyz/@tao/115493667607261044
최근 Lean에서 Erdos 문제에 대한 솔루션의 성공적인 "바이브 코딩"에서 영감을 얻었습니다.https://arxiv.org/abs/2510.19804, 나는 Quanyu Tang이 최근에 발굴한 Erdos의 또 다른 문제에 대한 반증(2001년 Pikhurko에 의해)을 공식화하려고 노력했습니다.https://www.erdosproblems.com/613. 이것은 간단한 유한 반례였습니다. 15개 정점에 44개의 간선이 있는 그래프로, 이분 그래프와 최대 차수가 5인 그래프로 나눌 수 없었습니다. Pikhurko의 논문은 9페이지에 불과했고 (더 다양한 매개변수 선택과 적절한 하한을 갖는 더 일반적인 반례도 구성했습니다), 최신 AI 도구에서도 충분히 구현할 수 있을 것으로 보였습니다. 그래서 저는 이 논문을 ChatGPT Pro에 업로드하고, 먼저 비공식적인 언어로 구성을 요약한 다음, 단계별로 공식화하도록 요청했습니다.https://chatgpt.com/share/690a65b3-473c-800e-afa5-e99f78610ee9 (1/4)
초기 단계는 매우 순조롭게 진행되었습니다. ChatGPT는 Pikhurko의 생성을 5차 사례에 맞게 정확하게 특화하고, 생성이 무엇이고 왜 작동하는지에 대한 매우 읽기 쉬운 설명을 제공했습니다. (이 버전의 GPT에서는 모든 질의에 답변하는 데 10분에서 20분이 걸렸기 때문에, 저는 이 작업을 비동기식으로 진행하면서 GPT를 수시로 확인하면서 다른 문제들을 처리했습니다.) 또한 그래프와 문제 진술에 대한 본질적으로 정확한 정의를 공식화하고, 요청된 각 단계에 대해 대부분 작동하는 Lean 코드를 제공했습니다. 제 Lean 저장소에 직접 접근할 수 없다는 점이 다소 제한적이었고, 약간 다른 구문을 사용하는 이전 버전의 Mathlib에서 학습한 것으로 보이므로 모든 것을 유형 검사하기 위해 어느 정도 정리가 필요했지만, 저는 이러한 문제를 해결할 만큼 Lean에 대한 전문 지식을 갖추고 있었습니다. 일부 줄은 전혀 컴파일되지 않았지만, 대부분의 경우 증명해야 할 진술이 충분히 명확해서 다른 증명을 직접 제공할 수 있었습니다. (많은 경우, GPT가 어떤 이유에서인지 사용하지 않았던 `aesop`이나 `grind`와 같은 강력한 추론 전략이 해당 진술을 즉시 처리했습니다.) (2/4)
한 가지 중요한 예외가 있었는데, 그래프에 실제로 44개의 간선이 있는지 확인해야 하는 단계였습니다. 그래프는 서로 분리된 다섯 개의 부분 그래프의 합집합이었는데, GPT는 각 그래프를 다소 정확하게 셀 수 있었습니다(사소한 기술적 수정을 통해). 하지만 합집합의 간선 수가 각 구성 요소 부분 그래프의 간선 수의 합인 이유를 제시하지는 못했습니다. 결국 저는 이 논증의 일부를 제대로 구현하기 위해 (GPT가 제안한 것과는 다른 접근 방식을 사용하여) Mathlib 도구에서 합 유형과 Finset 기수에 대한 정보를 찾는 데 한 시간 정도를 보냈습니다. (이는 제가 Lean에 대해 일반적으로 경험한 바와 일치합니다. 가장 "명백한" 명제가 제대로 공식화하는 데 가장 오랜 시간이 걸리는 경우가 많습니다.)
하지만 이것과 다른 사소한 변경 사항으로 인해 나는 다음과 같은 유형 검사 증명을 얻었습니다.https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/erdos_613.lean(풀 리퀘스트에 요약된 워크플로https://github.com/teorth/analysis/pull/384)(3/4)
이 과정은 이틀에 걸쳐 진행되었지만, 처음부터 끝까지 제 실제 집중력은 두세 시간 정도밖에 필요하지 않았던 것 같습니다. 같은 문장을 수작업으로 공식화하는 통제 실험(더 일반적인 검색 도구와 Github Copilot의 자동 완성 기능을 사용했지만, 프론티어 수준의 AI는 사용하지 않았습니다)은 시도하지 않았지만, 대략 6시간 정도 걸렸을 것으로 추정합니다. 아마도 증명은 훨씬 더 정교했을 것입니다. "바이브 코딩" 증명은 1,125줄로 구성되어 있으며, 그중 많은 부분이 `grind`와 같은 강력한 린 전략으로 이미 구현 가능한 사소한 것들을 증명하는 데 할애되어 있습니다. 하지만 이 결과는 인간의 증명이 불분명하거나 설득력이 없는 결과가 아니었고, 저는 이 실험을 통해 추가적인 린 공식화 경험을 얻었습니다.
요약하자면, 저는 이런 종류의 도구들을 린 타입체킹과 같은 엄격한 검증 방법과 결합하면 단계별로 실행할 때 시간이 많이 소요되는 여러 연구 수준의 작업을 (평균적으로) 약간 가속화하는 수준에 도달했다고 생각합니다. 하지만 여전히 무작위적인 변동과 통합 워크플로우에 대한 장벽이 있어 프로세스가 완전히 원활하지는 않으며, 사용 가능한 출력을 생성하지 못하는 쿼리의 중요하지 않은 부분을 적절히 수정할 수 있으려면 해당 작업에 대한 충분한 전문 지식이 필요합니다. (4/4)
전체 0