OpenAI, 수학 논문 3편 공개 철회

그러면 철회된 3개의 증명은 Lean 검증이 없는 것들이었나?

그렇다면 왜 Lean으로 검증된 증명과 자연어로 된 증명을 섞어 놓았을까?

Aaronson의 블로그를 읽으면서 궁금했던 점이다:

https://scottaaronson.blog/?p=10169

적어도 우리는 그것이 증명이라고 꽤 확신한다! 다른 372개의 획기적인 결과들 중 일부(전부는 아님)와 마찬가지로 Lean 인증서가 있다. 하지만 이 증명들 중 거의 어떤 것도 아직 인간이 이해하지 못한 것으로 보인다.

당연히 해야 할 일은 두 부분으로 나누어 공개하는 것 같다: 검증된 것들과, 좋은 아이디어가 있을 수도 있지만 실수도 있을 수 있는 것들. 후자는 아마 인간이 검증하는 데 훨씬 더 많은 비용이 들 것이다.

자세히 들여다보면, 완전히 AI가 생성한 이러한 증명들 중 많은 것이 무너질 것이라고 생각한다. Lean에서도 컴파일은 되지만 실제로 의도한 것과 다른 것을 진술하는 이론을 만들 수 있다. 다만 증명의 양이 너무나 압도적으로 많아서, abc 추측처럼 문제점을 발견하기까지 아마 수년이 걸릴 것이다.

정수 곱셈에서 O(n log n)을 능가한다는 논문도 상당히 수상하다고 본다. 확실치는 않지만 너무 좋아서 사실일 리 없어 보이고, 뭔가 미묘한 결함이 있을 것 같다. 어쩌면 내가 논문에 나오는 이런 작은 숫자들을 싫어해서 그럴 수도 있지만, 틀려 보이고 부자연스럽기까지 하다! 빛의 속도를 아주 작은 비율로 초과할 수 있다고 주장하는 물리학 논문에도 비슷하게 회의적일 것이다. 여기서 n log n이 자연스러운 한계라는 이유는 없지만, 몇 가지 좋은 직관이 보이는데도 우아한 형태로 표현될 수 없는 다른 무언가가 있다는 것은 나에게 매우 '비수학적'으로 느껴진다.

이렇게 한꺼번에 쏟아낼 거라면 전부 형식화해야 한다. 손으로 검토하기에는 자료가 너무 많고, 게다가 AI가 작성한 것이라 인간의 작업에 비해 읽기 어렵다.

이게 무슨 타임라인이냐, OpenAI의 모델이 너무 좋아서 수백 편의 수학 논문을 출판한다.

최신 모델은 심지어 이전에 출판된 수학 논문에서 오류를 찾아내기까지 한다!!!*

* 지금까지는 OpenAI의 수학 논문만 결함이 있어서 철회가 필요했다.

소프트웨어 엔지니어링 관행이 수학을 만났을 때 이렇게 된다. "openai/math 릴리스 1.3.42: 논문 139와 140 철회, 논문 47의 부호 오류 수정, 이전에 철회된 논문 85 복원, 논문 101의 논증 리팩터링".

철회가 실제 수학자가 논문을 보고 오류를 발견해서 이루어진 것인지, 아니면 모델을 돌려 교정한 것인지 궁금하다. 후자라면 아마 처음 있는 일은 아닐 텐데, 출판 전에 분명히 그렇게 했을 테니까. 두 경우 모두 흥미로운 함의가 있다.

약 400편 중 (지금까지) 3개의 실수라면 여전히 꽤 좋은 적중률이다.

그래서 수학도 '일단 판에 던져보고 붙는지 보자' 단계에 들어선 건가..

이건 그냥 OpenAI가 또 남의 작업을 훔치는 것이다.

그들이 출판하는 것 자체에는 문제가 없다. 그들의 과정과 상호작용 방식에도 문제가 없다. 그들이 실제로 이 작품들의 관리자 역할을 하고 있다는 점은 매우 기쁘다.

그건 그렇고, 그들은 문제를 검증하는 사람들에게 돈을 지불해야 한다. 정말 나를 화나게 하는 것은, 이 과정에서 출판되는 모든 것이 다음 훈련 세션에 빨려 들어갈 것이라는 점을 우리가 알고 있다는 것이다.