Google DeepMind 연구진은 AlphaProof Nexus 시스템이 에르되시 문제 9개를 해결했다고 보고했으며, 수학자들이 증명 여러 개를 검토했습니다. 동료 심사를 거친 연구판은 OpenAI가 미공개 AI 모델로 만든 수학 원고 722편을 게시한 지 이틀 뒤 공개됐습니다. 연구는 10월 8일 사이언스에 보도됐습니다.

시스템은 Google의 Gemini 언어 모델을 기반으로 한 여러 에이전트를 사용해 미해결 에르되시 문제 353개에 도전했습니다. 어려운 단계에서는 수학 학습 모델인 AlphaProof를 호출할 수 있었고, 형식화한 명제에 증명 단계가 부합하는지 확인하는 소프트웨어 Lean도 이용했습니다. 에이전트들은 유망한 풀이 시도를 공유하고 진전이 없는 시도는 버렸습니다.

연구진은 전체 시스템이 해결한 9개 문제에 더 단순한 구성도 시험했습니다. 서로 독립적으로 작동하는 Gemini 에이전트들은 Lean의 피드백을 활용했지만 풀이 시도를 공유하거나 AlphaProof에 문의하지 않고 9개를 모두 해결했습니다. 단순 구성은 쉬운 문제에서 연산 자원을 덜 썼고 가장 어려운 두 문제에서는 더 많이 사용했습니다. 전체 시스템이 풀지 못한 문제도 해결할 수 있는지는 확인되지 않았습니다. 공동 저자 스와라트 차우두리는 이 결과가 놀라웠다며, 역량 있는 언어 모델이 비교적 단순한 검증 도구로 연구 수학 문제에 도전할 수 있음을 시사한다고 말했습니다.

Lean은 입력된 명제만 검사하며, 수학적 명제를 Lean 안팎으로 옮기는 과정에서 잘못 번역될 수 있습니다. 10월 6일 공개된 사전 논문은 OpenAI가 작성한 나비에-스토크스 증명의 일부와 이에 대응하는 Lean 증명 사이의 불일치를 지적했습니다. 저자들은 그 불일치가 글로 쓴 증명이 틀렸다는 뜻은 아니라고 밝혔지만, 유효한 Lean 증명이 AI 생성 논문을 자동으로 검증하지는 않는다고 설명했습니다. 차우두리는 수학자들이 문제를 직접 생각하고 시스템의 목표를 정해야 한다며, 증명이 미완성일 때도 검증된 단계가 빈틈을 찾는 데 도움을 줄 수 있다고 말했습니다.

맨체스터대학교 수학자이자 폴 에르되시가 제기하거나 수집한 문제 1,000개 이상을 추적하는 사이트 운영자인 토머스 블룸은 방문자들이 자신도 이해하지 못하는 경우가 많은 AI 증명으로 문제를 먼저 해결하려 경쟁하는 일이 늘었다고 말했습니다. 블룸은 기자와 대화한 뒤 문제의 공개·해결 표시를 중단하고 댓글을 닫았으며, 이는 OpenAI의 결과를 알기 전이었습니다. 그는 AlphaProof Nexus의 성과가 중요도 면에서 최고 수준은 아니라고 평가하면서 Google DeepMind가 더 신중한 접근을 하고 있다고 말했습니다. OpenAI는 공개 관행을 두고 독립 자문단과 협력했다고 밝혔지만, 자문단은 미공개 AI 모델을 고급 수학에 시험하지 말라고 조언했으며 OpenAI는 이를 실행했습니다.

노스웨스턴대학교 수학자 브라이나 크라는 OpenAI가 과거 연구 인용을 개선했다고 말했습니다. 그러나 연구자들은 AI 모델이 미공개 연구에 접근했을 가능성을 널리 우려하며, 아이디어 공유를 꺼리고 있습니다. Plasma AI 최고기술책임자 앤드루 터너는 AI가 수학을 더 쉽게 접하게 하고 이전에는 상상하기 어려웠던 질문에 답하는 데 도움을 줄 수 있다고 말했습니다. 블룸이 사이트 운영 방식을 바꾼 지 며칠 뒤 Plasma AI는 AI 결과를 환영하는 에르되시 문제 추적 사이트를 발표했습니다. 블룸은 호기심을 유지하고 AI를 보조 수단으로 활용하되 수학 문제를 스스로 계속 풀어야 한다고 당부했습니다.

Google DeepMind 연구진은 AlphaProof Nexus 시스템이 에르되시 문제 9개를 해결했다고 보고했으며, 수학자들이 증명 여러 개를 검토했습니다. 동료 심사를 거친 연구판은 OpenAI가 미공개 AI 모델로 만든 수학 원고 722편을 게시한 지 이틀 뒤 공개됐습니다. 연구는 10월 8일 사이언스에 보도됐습니다.

시스템은 Google의 Gemini 언어 모델을 기반으로 한 여러 에이전트를 사용해 미해결 에르되시 문제 353개에 도전했습니다. 어려운 단계에서는 수학 학습 모델인 AlphaProof를 호출할 수 있었고, 형식화한 명제에 증명 단계가 부합하는지 확인하는 소프트웨어 Lean도 이용했습니다. 에이전트들은 유망한 풀이 시도를 공유하고 진전이 없는 시도는 버렸습니다.

연구진은 전체 시스템이 해결한 9개 문제에 더 단순한 구성도 시험했습니다. 서로 독립적으로 작동하는 Gemini 에이전트들은 Lean의 피드백을 활용했지만 풀이 시도를 공유하거나 AlphaProof에 문의하지 않고 9개를 모두 해결했습니다. 단순 구성은 쉬운 문제에서 연산 자원을 덜 썼고 가장 어려운 두 문제에서는 더 많이 사용했습니다. 전체 시스템이 풀지 못한 문제도 해결할 수 있는지는 확인되지 않았습니다. 공동 저자 스와라트 차우두리는 이 결과가 놀라웠다며, 역량 있는 언어 모델이 비교적 단순한 검증 도구로 연구 수학 문제에 도전할 수 있음을 시사한다고 말했습니다.

Lean은 입력된 명제만 검사하며, 수학적 명제를 Lean 안팎으로 옮기는 과정에서 잘못 번역될 수 있습니다. 10월 6일 공개된 사전 논문은 OpenAI가 작성한 나비에-스토크스 증명의 일부와 이에 대응하는 Lean 증명 사이의 불일치를 지적했습니다. 저자들은 그 불일치가 글로 쓴 증명이 틀렸다는 뜻은 아니라고 밝혔지만, 유효한 Lean 증명이 AI 생성 논문을 자동으로 검증하지는 않는다고 설명했습니다. 차우두리는 수학자들이 문제를 직접 생각하고 시스템의 목표를 정해야 한다며, 증명이 미완성일 때도 검증된 단계가 빈틈을 찾는 데 도움을 줄 수 있다고 말했습니다.

맨체스터대학교 수학자이자 폴 에르되시가 제기하거나 수집한 문제 1,000개 이상을 추적하는 사이트 운영자인 토머스 블룸은 방문자들이 자신도 이해하지 못하는 경우가 많은 AI 증명으로 문제를 먼저 해결하려 경쟁하는 일이 늘었다고 말했습니다. 블룸은 기자와 대화한 뒤 문제의 공개·해결 표시를 중단하고 댓글을 닫았으며, 이는 OpenAI의 결과를 알기 전이었습니다. 그는 AlphaProof Nexus의 성과가 중요도 면에서 최고 수준은 아니라고 평가하면서 Google DeepMind가 더 신중한 접근을 하고 있다고 말했습니다. OpenAI는 공개 관행을 두고 독립 자문단과 협력했다고 밝혔지만, 자문단은 미공개 AI 모델을 고급 수학에 시험하지 말라고 조언했으며 OpenAI는 이를 실행했습니다.

노스웨스턴대학교 수학자 브라이나 크라는 OpenAI가 과거 연구 인용을 개선했다고 말했습니다. 그러나 연구자들은 AI 모델이 미공개 연구에 접근했을 가능성을 널리 우려하며, 아이디어 공유를 꺼리고 있습니다. Plasma AI 최고기술책임자 앤드루 터너는 AI가 수학을 더 쉽게 접하게 하고 이전에는 상상하기 어려웠던 질문에 답하는 데 도움을 줄 수 있다고 말했습니다. 블룸이 사이트 운영 방식을 바꾼 지 며칠 뒤 Plasma AI는 AI 결과를 환영하는 에르되시 문제 추적 사이트를 발표했습니다. 블룸은 호기심을 유지하고 AI를 보조 수단으로 활용하되 수학 문제를 스스로 계속 풀어야 한다고 당부했습니다.