Hacker News

OpenAI Withdraws 3 Math Papers

OpenAI, 수학 논문 3편 철회하고 14편 수정

OpenAI는 부호 오류로 핵심 논증이 무너진 논문과 그 결과에 의존한 논문 두 편을 철회했습니다. 다른 논문 14편도 증명과 가정 등을 수정했으며, 추가 수정본 인용과 형식화 결과를 반영해 주요 결과의 Lean 형식화 비율은 300/719, 약 42%가 됐습니다.

AI 요약

OpenAI가 수학 원고의 철회·수정 내역을 공개했습니다. 철회한 세 편 가운데 ‘Algebraicity of Weil classes on split abelian eightfolds’에서 부호 오류가 발견됐습니다. 이 오류는 안정화-추적 상쇄 논증과 그 논증에 쓰인 구성을 무효로 만들었습니다. 해당 결과에 의존한 논문 두 편도 함께 철회했습니다. 철회한 원고의 README에는 오류가 난 부분과 보관된 원고 링크를 안내합니다.

철회와 수정

철회 대상은 ‘Algebraicity of Weil classes on split abelian eightfolds’, ‘Algebraicity of Kuga–Satake Correspondences for K3 Surfaces’, ‘The rational Hodge conjecture for products of K3 surfaces’입니다.

OpenAI는 별도의 원고 14편도 고쳤습니다. 수정에는 증명 보완, 명제 정정, 가정과 의존 관계 명료화, 오래된 인용 하나 삭제가 포함됩니다. Lipschitz 높이와 Ashkin–Teller 전류 관련 원고 4편에서는 교차, 경계 부착, 조건화, 수렴 논증을 손봤고 real-Lipschitz 경계면 증명도 보강했습니다. Kähler 최소 모델 프로그램과 풍부성 관련 원고 6편은 양성 및 수축 논증을 확장하고, 입력으로 사용하는 결과와 필요한 가정을 명확히 했습니다.

Taming과 hypersymplectic 변형 관련 원고 2편에서는 ‘Taming implies compatibility’의 원뿔 집합 동치 주장을 정정하고 엄격한 포함 관계의 예를 추가했습니다. hypersymplectic 원고에서는 불필요한 원뿔 비교 의존성을 제거했습니다. ‘Incompressible Box Transport and Finite Computation’은 토러스 사영과 공통 시계 추정치를 수정했습니다. ‘Exact Birch–Swinnerton-Dyer Formula from Low Selmer Corank’에서는 삭제된 보조 원고를 가리키던 오래된 서론 인용을 없앴습니다.

이 수정에 맞춰 동료 원고 13편도 인용한 판본과 버전 날짜를 갱신했습니다. 형식화(formalization)는 6건 추가했고, 뒷받침 결과 5건도 더했습니다. 주요 결과 가운데 Lean으로 형식화한 비율은 719개 중 300개, 약 42%입니다.

Hacker News 반응

  • @breezybottom — “Lean으로 검증했으니 괜찮다”는 변명은 이제 못 하겠네요.
    • @n2d4 — 철회한 논문은 Lean으로 검증되지 않았고, 검증됐다고 주장한 적도 없습니다.
  • @qoez — 이런 문제를 지적할 활발한 수학 공동체가 없었다면 오류가 그대로 남았을 겁니다. 자동화 수학이 발전하면 그 공동체가 위험해진다고 Tao가 지적했죠.
    • @viraptor — 누가 오류를 지적했는지 링크가 있나요? 형식 증명을 진행하다가 발견한 문제일 가능성이 커 보입니다.
    • @afavour — 그건 증명이 아니지 않나요? 원래 LLM 출력이 틀릴 수 있다면, 그 출력을 검토하는 LLM도 틀릴 수 있습니다.
    • @rsfern — 무엇을 증명한다는 뜻인가요? 증명 하나에서 부호 오류가 나왔고 OpenAI는 이를 인정해 논문 세 편을 철회했습니다. LLM 검토도 사람 검토도 틀릴 수 있지만, 흥미로운 점은 OpenAI가 자기 모델로 오류를 찾기 전에 확인했어야 한다는 겁니다.
  • @hmate9 — 지금까지 약 400편 중 3편의 오류라면 그래도 꽤 좋은 적중률 아닌가요?
    • @matsemann — 사람이 따라가기 힘들 만큼 원고가 엉성하다면 나머지를 반증할 수는 있나요? OpenAI가 맞다는 걸 입증해야 하는 것 아닌가요?
    • @true_religion — 컴퓨터가 생성한 결과라면 형식 검증을 책임져야 합니다. 지금까지 형식화된 논문은 22%뿐입니다.
    • @malux85 — 철회를 보고 안심했습니다. 가설을 세우고, 주장하고, 시험하고, 반박하거나 확장하고, 철회하는 과정은 건강한 과학 생태계의 일부입니다.
  • @margorczynski — 이 정도로 한꺼번에 공개한다면 전부 형식화해야 합니다. 사람이 일일이 검토하기엔 자료가 너무 많고, AI가 쓴 글은 사람이 쓴 글보다 읽기도 어렵습니다.
    • @margorczynski — 글을 읽기 어렵다는 점도 문제지만, 더 급한 문제는 Lean 형식화가 부족하다는 겁니다. 형식화되지 않으면 증명됐는지 반증됐는지 말하기 어렵습니다.
  • @mtlmtlmtlmtl — 논문을 철회하는 것 자체는 무책임한 일이 아닙니다. 다만 검증되지 않은 미완성 결과를 두고 대대적인 홍보를 하는 일은 무책임합니다.

원문: Hacker News / 번역·요약: Trawling