AI가 수학 난제까지 푼다고? Aletheia 논문 분석과 현업 엔지니어의 시선

IMO 금메달, 그 다음은 무엇일까?

불과 몇 년 전만 해도 우리는 AI가 코딩을 ‘도와주는’ 수준에 감탄했습니다. 그런데 이제는 상황이 조금 다르게 흘러가고 있습니다. 최근 구글 딥마인드와 협력 연구진이 발표한 Towards Autonomous Mathematics Research 논문은 단순히 수학 올림피아드(IMO) 문제를 푸는 것을 넘어, 실제 ‘연구(Research)’ 레벨의 문제를 해결하는 AI 에이전트, Aletheia 를 소개하고 있습니다.

저는 15년 넘게 시스템을 설계하고 운영해온 엔지니어로서, 솔직히 ‘Autonomous(자율)‘라는 단어가 붙으면 일단 의심부터 하고 봅니다. 하지만 이번 논문과 이에 대한 Hacker News의 반응을 뜯어보니, 우리가 주목해야 할 기술적 변곡점이 분명히 존재합니다.

오늘은 이 논문이 주장하는 바와, 시니어 엔지니어 입장에서 바라본 현실적인 한계, 그리고 업계의 반응을 가감 없이 분석해 보겠습니다.

1. Aletheia: 단순한 LLM이 아닙니다

이 시스템의 핵심은 단순히 거대 언어 모델(LLM)에게 “이거 증명해줘”라고 던지는 것이 아닙니다. 엔지니어링 관점에서 보면 Agentic Workflow 의 정수를 보여줍니다.

  • Gemini Deep Think: 복잡한 추론을 위해 강화된 모델을 사용합니다.
  • Inference-time Scaling: 단순히 학습 데이터를 늘리는 게 아니라, 추론 단계에서 더 많은 연산 자원을 투입하여 ‘오랫동안 깊게’ 생각하게 만듭니다.
  • Tool Use: 이게 정말 중요합니다. AI가 혼자 뇌피셜로 증명하는 게 아니라, Python이나 Lean 같은 증명 보조 도구(Proof Assistant)를 적극적으로 활용합니다.

논문에서는 이 시스템을 통해 세 가지 주요 마일스톤을 달성했다고 주장합니다.

  1. Feng26: 인간의 개입 없이 AI가 단독으로 작성한 리서치 페이퍼.
  2. LeeSeo26: 인간과 AI가 협업하여 작성한 페이퍼.
  3. Bloom’s Erdos Conjectures: 700개의 난제 중 4개를 자율적으로 해결.

숫자 4가 작아 보이나요? 수십 년간 풀리지 않던 문제 4개를 해결했다는 건, 레거시 코드에서 아무도 원인을 모르던 크리티컬 버그 4개를 AI가 혼자 고친 것과 맞먹는 임팩트입니다.

2. Hacker News의 반응: “기적” vs “진흙탕 싸움”

기술 커뮤니티의 반응은 언제나처럼 냉철합니다. Hacker News의 토론을 보면 현업 엔지니어들이 무엇을 우려하는지 명확히 알 수 있습니다.

“성공 사례는 극히 드물다” 한 유저는 이 논문의 결과가 AI가 모든 리서치 문제를 풀 수 있다는 뜻으로 해석되어서는 안 된다고 경고합니다. 실제로 성공 케이스는 수많은 시도 끝에 얻어걸린(spontaneous positive outcomes) 경우에 가깝다는 것이죠. 마치 우리가 수천 번의 단위 테스트를 돌려 겨우 통과하는 코드를 만들어내는 과정과 비슷합니다.

“Proof Space vs Gibberish” 흥미로운 논쟁 중 하나는 AI가 탐색하는 공간이 진정한 의미의 ‘증명 공간(Proof Space)‘인가 하는 점입니다. 한 유저는 신랄하게 비판합니다.

“LLM은 증명 공간을 탐색하는 게 아니다. 그저 문법적으로 말이 되는 헛소리(grammatically coherent gibberish)를 생성할 뿐이고, 진짜 증명 공간이라면 틀린 증명에 도달해서는 안 된다.”

하지만 반론도 만만치 않습니다. 인간 역시 직관에 의존해 수많은 헛발질을 하다가 정답을 찾습니다. AI가 Lean 같은 형식 언어(Formal Language)를 통해 검증(Verify) 과정을 거친다면, 그 과정이 확률적이든 아니든 결과물은 유효하다는 것입니다.

3. 엔지니어 관점에서의 Deep Dive: 검증의 힘

제가 이 논문에서 가장 주목한 기술적 포인트는 Verification Loop 입니다.

우리가 주니어 개발자의 코드를 리뷰할 때, 그 친구가 얼마나 똑똑한지보다 그 코드가 컴파일되고 테스트를 통과하는지가 더 중요합니다. 수학에서도 마찬가지입니다. Aletheia는 자연어로 사고하지만, 결정적인 순간에는 코드를 실행하거나 증명 검증기를 돌립니다.

  • Formal Verification (Lean): 이것은 수학계의 ‘컴파일러’이자 ‘CI/CD 파이프라인’입니다.
  • Feedback Loop: 검증기가 에러를 뱉으면, AI는 다시 수정해서 제출합니다.

결국, LLM의 환각(Hallucination) 문제를 해결하는 유일한 방법은 외부의 확실한 검증 도구(Ground Truth Tools) 와 결합하는 것입니다. 이 패턴은 앞으로 엔터프라이즈 AI 아키텍처의 표준이 될 것입니다.

4. 확장성(Scaling)과 에너지의 문제

HN 댓글 중 “AI가 인간 수준의 에러율을 달성하려면 은하계 전체의 에너지가 필요할 것”이라는 다소 과격한 주장이 있었습니다. 물론 과장이 섞여 있지만, 시사하는 바가 큽니다.

현재의 방식(Inference-time compute)은 엄청난 비용이 듭니다. 논문의 성과는 인정하지만, 이것이 경제적으로 지속 가능한 모델인지는 별개의 문제입니다. 구글이 제 Gemini 사용량을 제한하는 것만 봐도 알 수 있죠. 하드웨어 투자가 계속되고 있지만, 알고리즘 효율성의 획기적인 개선 없이는 ‘무지성 스케일링’은 한계에 부딪힐 수 있습니다.

5. 결론: 도구인가, 경쟁자인가?

이 논문은 AI가 이제 ‘정답이 있는 문제’를 푸는 단계를 지나, ‘정답을 모르는 문제’를 탐구하는 영역으로 진입했음을 보여줍니다. 하지만 여전히 Human-in-the-loop 가 가장 강력한 성능을 냅니다. LeeSeo26 페이퍼(협업 모델)가 그 증거입니다.

제 개인적인 평가는 이렇습니다:

아직 AI가 우리를 대체하여 ‘자율적으로’ 연구하고 개발하는 단계는 아닙니다. 96%의 정확도는 훌륭해 보이지만, 엔지니어링과 수학의 세계에서 나머지 4%의 오류는 치명적입니다. 하지만 형식 검증(Formal Verification) 도구와 결합된 AI는, 인간이 혼자서는 절대 도달할 수 없는 생산성의 영역을 열어주고 있습니다.

우리는 지금 ‘어셈블리어’에서 ‘C언어’로 넘어가는 듯한 과도기에 서 있습니다. 도구를 거부할 것이 아니라, 이 강력한 레버리지를 어떻게 당길지 고민해야 할 때입니다.

References: