에르되시 문제 #728, AI가 거의 자율적으로 해결

1 month ago 12

  • 에르되시 문제 #728이 최근 AI 도구에 의해 거의 자율적으로 해결되며 수학 연구 자동화의 새로운 이정표를 세움
  • 문제는 원래 Erdős, Graham, Ruzsa, Strauss가 1975년에 제기한 이항계수의 소인수분해 관련 질문으로, 애매한 조건 때문에 오랫동안 명확히 다뤄지지 않았음
  • ChatGPT가 조정된 제약 조건하에서 증명을 생성하고, Aristotle이 이를 Lean 형식 증명으로 공식화하며 오류를 자동 수정함
  • 이후 여러 참가자들이 ChatGPT를 이용해 자연어로 재작성하고, 문헌 연결과 서사 구조를 강화한 버전을 반복적으로 개선함
  • Terence Tao는 이 과정을 통해 AI의 신속한 증명 작성·수정 능력이 연구 논문 작성 방식 자체를 변화시킬 잠재력을 보여준다고 평가함

AI가 해결한 에르되시 문제 #728

  • 최근 AI 도구의 적용이 에르되시 문제 해결에 새로운 진전을 보였으며, 문제 #728이 거의 자율적으로 AI에 의해 해결
    • 초기 시도 후 피드백을 반영해 수정된 버전에서 성공
    • 결과는 기존 문헌에서 동일하게 재현되지 않았으며, 유사한 방법의 비슷한 결과만 존재
  • 이 사례는 최근 몇 달간 AI의 수학적 문제 해결 능력이 실제로 향상되었음을 보여줌
    • 과거에도 AI가 에르되시 문제를 해결한 사례가 있었으나, 대부분은 이후 문헌에서 이미 존재하는 해로 판명됨
  • 이번 문제는 원래 에르되시의 서술이 잘못된 형태로 제시되어 있었고, 최근에야 의도된 형태로 재구성됨
    • 이로 인해 기존 문헌에 관련 연구가 부족했던 것으로 설명됨

문제의 역사와 초기 접근

  • 1975년 Erdős, Graham, Ruzsa, Strauss이항계수 (2n choose n) 의 소인수분해를 연구하며 여러 관련 문제를 제시
    • 그중 하나가 a!b! | n!(a+b−n)! 조건과 a+b > n + C log n을 만족하는 무한한 a, b, n의 존재 여부를 묻는 문제였음
    • 그러나 C의 크기(작은지 큰지) 등 여러 부분이 불명확하게 서술됨
  • 몇 달 전 AlphaProof 팀이 문제의 단순 해를 발견했으나, 이는 의도된 문제 정신에 맞지 않아 a,b ≤ (1−ε)n 제약을 추가함
    • 이후 AI 보조 문헌 검색에서도 관련 연구는 거의 발견되지 않음

ChatGPT와 Aristotle의 협업

  • 1월 4일 ChatGPT가 조정된 제약 조건에서 작은 C의 경우에 대한 증명을 생성
    • 이 증명은 Aristotle에 의해 Lean 형식 증명으로 공식화됨
    • 이후 원문을 재검토한 결과, 원래 논문이 이미 작은 C의 경우를 다루고 있었음이 확인됨
  • 다른 참가자가 Lean 증명을 ChatGPT로 자연어로 변환하고, 추가 대화를 통해 개선된 버전을 작성
    • 이 버전은 일부 증명 공백을 메웠으나, 여전히 AI 특유의 어색한 문체문헌 인용 부족이 남음
    • 그럼에도 핵심 아이디어를 이해할 수 있을 정도로 읽기 가능한 수준에 도달함

대규모 재작성과 개선된 결과물

  • 추가 프롬프트를 통해 ChatGPT가 큰 C의 경우까지 확장된 증명을 생성
    • 일부 오류가 있었으나 Aristotle이 자동으로 수정하고 Lean 검증된 증명을 완성
  • 세 번째 참가자가 Lean 증명을 압축한 뒤, 다른 참가자가 ChatGPT와 장시간 대화를 통해
    • 문헌 연결과 서사 구조를 강화한 완성도 높은 논문 형태로 재작성
    • 결과물은 AI 생성물의 느낌이 줄어든, 연구 논문 수준에 근접한 품질로 평가됨
    • Tao는 이 텍스트를 에르되시 문제 포럼에서 검토했다고 언급

AI가 바꾸는 연구 논문 작성 방식

  • Tao는 최종 논문은 여전히 핵심 부분은 인간이 작성해야 한다고 보지만,
    • AI와 Lean의 결합증명 작성과 수정의 속도를 획기적으로 높였다고 평가
  • 기존에는 논문 한 편을 읽기 좋게 만드는 데 많은 시간이 들고,
    • 심사자 피드백에 따른 수정도 국소적 변경에 그치는 경우가 많았음
  • 그러나 이제는 AI의 텍스트 생성·수정 능력형식 증명 도구의 검증 기능이 결합되어
    • 다양한 수준의 정밀도와 서술로 빠르게 새로운 버전의 논문을 생성할 수 있음
  • 하나의 “공식 논문” 외에도, AI가 생성한 다수의 보조 버전이 존재해
    • 다양한 관점과 추가적 가치를 제공할 수 있는 가능성이 제시됨

커뮤니티 반응

  • 일부 사용자는 AI가 생성한 문서의 추가적 가치를 “다른 각도에서 볼 수 있는 능력”으로 설명
  • 다른 수학자들은 AI 결과의 독창성 측정이나 기존 문헌과의 유사성 평가의 필요성을 제기
    • 예를 들어, Lean 형식 증명 길이 비교를 통한 정량적 유사성 측정 제안
  • 또 다른 논평에서는 AI가 코드 리팩터링처럼 논문을 전역적으로 재작성할 수 있어
    • 연구자들이 더 높은 수준의 문서 구조 설계에 집중해야 한다는 의견도 제시됨
  • 일부는 AI가 수학자의 역할을 대체할 가능성에 회의적 반응을 보였으나,
    • 다른 이들은 이를 협업과 사고 확장의 새로운 기회로 평가함

Read Entire Article