Resolution, 에이전트로 힐로나카 특이점 해소 정리 자동 형식화…약 13.5만 달러·60만 줄 Lean 코드

Import AI 478: Math for alignment; ProgramBench; and Mirendil shows what RSI means

AI 안전 스타트업 Resolution이 통계적 학습 이론과 관련된 수학 명제 일부를 자동으로 형식화했다고 발표했다. 특이점 해소(resolution of singularities) 정리를 자동 형식화해 손실 지형 기하와 일반화의 관계를 자동 연구할 기반을 마련했다는 것이 핵심이다. 연구자는 먼저 에이전트들과 함께 고수준의 사람이 읽을 수 있는 계획과, 기존 문헌을 충실히 따르는 112페이지 분량의 원자 단계 계획 두 가지를 만들었다. 이후 오케스트레이터 에이전트에게 실행을 맡겼고, 에이전트들은 종이와 펜으로 하는 수학, Lean 작성, 계획 점검 등을 나눠 수행했다. 실행 단계에서는 초기 계획과 이전 내부 자동 형식화 작업에서 추출한 일부 에이전트 스킬 외에는 별다른 스캐폴딩이 거의 필요하지 않았다고 한다. 작업은 약 일주일이 걸렸고, 약 1000억 입력 토큰(90%가 캐시 읽기)과 약 3억 출력 토큰이 쓰였으며 추정 토큰 비용은 13만 5천 달러, 생성된 Lean 코드는 약 60만 줄이다. Resolution은 이 라이브러리를 활용해 특이 학습 이론(singular learning theory)의 일부를 확장하는 데 이미 성과를 보았다고 밝혔다. 특이점 해소를 형식화하면 샘플링을 더 잘 이해하는 등 이론의 더 많은 부분을 자동화할 수 있고, 그 이해를 바탕으로 모델이 학습하는 방식을 형성하는 것이 회사가 '패터닝'이라 부르는 목표다. 기사는 이러한 수학의 산업화가 연구 자동화에 대한 새로운 엄밀한 과학을 가능하게 할 것이라고 Resolution이 쓴 점을 전한다.