OpenAI, 수학 결과 3건 철회

Hacker News 의견들 이런 오류를 짚어낼 활발한 수학 공동체가 없었다면 잘못된 채로 남았을 것임. Tao가 짚었듯 수학 자동화는 바로 그 공동체를 위태롭게 함. 수학 공동체만의 문제가 아님. AI가 신입 소프트웨어 엔지니어의 필요성을 없애면서 거의 아무도 신입을 채용하지 않지만, 기업에는 여전히 시니어가 필요함. 신입 없이 미래의 시니어를 어떻게 길러낼 수 있을까?. 해법이 무엇일지는 모르겠지만, 소프트웨어나 수학 분야의 AI 발전을 중단하는 것이 답이라고 보지는 않음. 수학 공동체가 없거나 약했다면 OpenAI는 철회한 결과의 명성을 계속 누렸을 텐데, 논문 철회로 투자자들이 손해를 봤으니 참으로 용납할 수 없는 일임. 자동화가 그 공동체를 위협한다니 반가운 소식임. 투자자에게 방해가 되는 공동체는 없애야 하지 않겠는가? 본문에는 LLM을 검증기로 사용해 오류를 찾았다고 되어 있어서, 여기서 공동체의 역할이 얼마나 컸는지는 잘 모르겠음. OpenAI의 태도는 “모든 수학 문제의 답을 내놨으니 수학자는 이제 필요 없음. 상금과 명성은 Sam Altman에게 보내면 됨. 그런데 이 답을 확인할 수학자는 좀 필요함”이라는 식임. 누가 오류를 지적했는지 보여주는 링크가 있는지? 아직 형식 증명을 진행 중인 것 같아서, 그 과정에서 문제를 찾았을 가능성이 있어 보임. 철회된 증명 3개가 Lean 검증이 없던 증명이었는지? 그렇다면 왜 Lean으로 검증한 증명과 자연어 증명을 섞어서 공개했는지 궁금함. Aaronson의 블로그를 읽으면서도 같은 의문이 들었음. https://scottaaronson.blog/?p=10169. 글에는 “적어도 증명이라고 꽤 확신함. 다른 획기적 결과 372개 중 일부와 마찬가지로 Lean 인증서가 있음. 다만 거의 어떤 증명도 아직 인간이 이해하지 못한 것으로 보인다”는 취지로 적혀 있음. 검증된 결과와 아이디어는 좋지만 오류가 있을 수 있는 결과를 나눠 공개하는 게 당연해 보임. 후자는 사람이 검증하는 데 훨씬 많은 비용이 들 것임. 모델 작업 시간 3.5시간이라는 제약을 고려하면, Lean 증명이 있다는 사실은 오히려 일부 결과의 수준이 낮을 가능성을 보여줌. 공동체의 노력에도 mathlib에는 빈틈이 많고 기본 이론도 여럿 빠져 있어, 증명은커녕 명제를 기술할 수조차 없는 문제가 많음. 형식화는 작은 단계마다 많은 노동이 필요해서 작성 가능한 코드량이 도달 범위를 제한하기도 ...