arXiv에 2026년 6월 13일 공개된 논문이 검증 가능한 AI 보조 추론 시스템 VGPT-RSI(Verifiable Growing Physical Transformer with Recursive Self-Improvement)를 수학의 미해결 난제인 리만 가설(Riemann Hypothesis) 인접 과제에 적용한 결과를 보고했다. 연구진은 리만 가설 자체를 증명했다고 주장하지 않는다. 대신 형식적으로 검증된 부분 진전을 생성하면서 아직 해결되지 않은 수학적 장애물을 명시적으로 식별할 수 있는지를 탐구했다.
연구진은 두 가지 인증 과제를 수행했다. 첫째, 특정 매개변수화된 안전 하한 곡선 위의 구간에 대해 유한 RH 경계 인증서를 구성하고 검증했다. 수치 경계 곡선을 인증서 기반 하한 곡선으로 변환한 뒤 외향 반올림 구간 산술과 Arb/FLINT 볼 산술을 이용해 감사한 후 Rocq/CoqInterval에서 정리를 검증했다. 둘째, 라가리아스 기준(Lagarias criterion)을 활용한 형식 인증서를 시작했다. 라가리아스 기준은 리만 가설이 전역 부등식과 동치임을 말한다. 연구진은 이 유한 수량을 형식화하고 Coq로 검증된 유한 인증서를 생성했다.
이 연구의 특징은 AI 시스템이 증명에 실패하는 정확한 지점을 식별한다는 데 있다. 논문은 아직 해결되지 않은 수학적 병목으로 라가리아스 동치 형식화, 임의의 유한 상한을 넘는 전역 꼬리 정리 증명, 반례가 있다면 특정 극단적 정수로 환원하는 문제를 지목했다. 연구진은 VGPT-RSI가 인증된 형식 진전을 생산하고 증명 의존성을 정리하면서, 남은 장애물이 진짜 수학적 문제일 때 과도한 주장을 피한다고 밝혔다.
AI를 이용한 형식 수학 증명 시도는 딥마인드의 알파프루프(AlphaProof) 등으로 주목을 받아왔다. 이 연구는 완전한 증명보다 검증 가능한 부분 진전과 실패 경계의 명시적 기록이라는 접근으로, AI 보조 수학 연구의 신뢰성 기준을 높이는 방향을 제시한다는 점에서 의미가 있다.
