드미트리 트레이텔(Dmitriy Traytel)은 클로드와 Isabelle 증명 보조기를 이용해 상대적 차익거래에 관한 수학 논문의 주요 정리를 형식화했다. 작업에는 3주가 걸렸고, 초기 증명은 10만 줄이 넘었으며 정리와 구조 개선을 거친 현재 형식화는 8만 5천 줄이다. Isabelle은 증명을 검사했지만, 트레이텔은 증명 과정을 충분히 이해하지 못했다고 밝혔다.
트레이텔은 르네상스 필란트로피가 지원하는 Copilots for Isabelle 프로젝트의 일환으로 AI 에이전트가 Isabelle과 연동하는 도구를 개발한다. 이번 작업에서는 케빈 카펠만(Kevin Kappelmann)의 PIDE MCP를 사용했다. 이 도구는 Isabelle의 상태와 피드백을 에이전트에 실시간으로 제공한다.
형식화 대상은 미샤 슈클로프니코프(Misha Shkolnikov), 주화 라이(Jou-Hua Lai), H. 메테 소너(H. Mete Soner)가 공동 집필한 상대적 차익거래 논문이다. 논문은 아직 출판 전이지만 출판 절차가 마무리 단계에 있다고 트레이텔은 설명했다. 논문은 arXiv에서 확인할 수 있다.
정리의 내용과 수정 과정
형식화는 Isabelle의 HOL-Analysis와 HOL-Probability에 더해 Archive of Formal Proofs(AFP)의 Disintegration, Kolmogorov_Chentsov, Levy_Prokhorov_Metric, Lower_Semicontinuous, Martingales, Standard_Borel_Spaces를 활용했다. 정리의 정의와 논문 표현을 비교해 설명하는 시각 자료도 만들었다. 정리 설명 자료는 정의에 마우스를 올려 관련 내용을 살펴볼 수 있도록 구성됐다.
트레이텔은 논문과 형식화된 정의를 대조해 정리의 진술이 올바르다고 판단했다. 공동 저자 슈클로프니코프에게 정리의 PDF 버전을 보여준 뒤에는 그 판단이 더 강해졌다고 덧붙였다. 다만 증명은 Isabelle이 검사했으므로 증명 세부를 직접 면밀히 살필 필요는 없었다고 했다.
작업 중 클로드는 정리의 가정을 논문과 다르게 설정한 부분을 스스로 찾아 고쳤다. 처음에는 초해집합의 상한 조건을 잘못 적어 무한대 값을 배제하지 못했지만, 앞서 증명한 내용을 활용해 진술을 수정했다. 또 초해결자 조건에서 논문의 L ≥ 1 대신 L > 1을 사용한 점을 발견했다. 클로드는 논문에서 L > 1이 암묵적으로 도입되는 대목을 찾아냈고, 이후 증명을 고쳐 L = 1도 포함하도록 했다. 슈클로프니코프는 이 수정이 이번 형식화에서 가장 흥미로운 결과였다고 평가했지만, 논문에 반영하려면 일주일가량이 걸릴 것이라고 말했다.
작업 규모와 제약
클로드는 약 3주 동안 거의 쉬지 않고 작업했다. 트레이텔은 당시 Claude Max 5x 구독을 이용했다. Claude Fable 5가 토큰 한도 안에서 초안을 작성하면 Claude Opus 5가 현재 증명 상태와 메모, 계획을 바탕으로 이어갔다. 트레이텔은 주로 논문을 Isabelle로 형식화하라는 지시를 주고, 진행을 독려하거나 새 개념을 형식화하기 전에 AFP를 살펴보라고 제안했다.
첫 완성본은 64개 이론 파일을 하나의 세션에 담았고 10만 줄이 넘었다. 이후 재사용 가능한 내용과 정리 전용 내용을 분리하고 구조를 바꿔 현재는 12개 세션, 약 8만 5천 줄로 줄었다. 이 가운데 약 7만 줄은 AFP에 재사용 가능한 라이브러리 자료가 될 수 있고, 1만 3천 줄은 주요 정리를 형식화하며, 1,800줄은 논문 표기로 결과를 제시한다. 다만 트레이텔은 이 자료가 현재 상태로 AFP에 적합한지 확신하지 못하며, AI가 만든 내용의 품질을 우려해 제출에 신중하다고 밝혔다.
클로드는 논문에서 사용한 확률적 적분과 이토 공식은 형식화하지 않았다. 대신 무엇을 했는지, 그 접근이 수학적으로 더 나은지 나쁜지 트레이텔은 판단하기 어렵다고 했다. 에이전트는 크랜달-이시이 정리 전체도 처음에는 미뤘다가 주요 정리에 필요한 핵심 논증만 형식화했다. 트레이텔이 그 정리의 중요성을 알게 된 뒤 전체 내용을 보완하라고 지시했다.
PIDE MCP는 Isabelle의 편집 결과에 대한 최신 피드백을 제공해 형식화 작업에 적합했다고 트레이텔은 평가했다. 에이전트가 끝나지 않는 증명을 만들 때도 문제 명령을 ‘잠재적으로 종료되지 않음’으로 표시해 알아차릴 수 있었다. 다만 당시에는 세션을 동적으로 다루는 기능이 없어 구조를 바꿀 때마다 MCP 서버와 Claude Code를 재시작해야 했다. 이 기능은 이후 PIDE MCP에 추가됐다.
트레이텔은 구독료 월 100달러와 별도로, 같은 작업에 API를 사용했다면 비용이 약 7,500달러였을 것으로 클로드가 추산했다고 전했다. 추산에는 입력 토큰 약 97억 개와 출력 토큰 2천만 개가 포함되며, 사용량은 Fable 30%, Opus 70%로 나뉜다. 최초 증명 이후의 정리와 구조 개선 비용은 계산에 포함되지 않았다.
트레이텔은 형식 증명이 만들어졌다고 해서 작업자가 증명 구조를 이해하거나 결과의 재사용 가능성을 판단할 수 있는 것은 아니라고 지적했다. 그는 비전문가도 형식 증명을 쉽게 생성하는 시대가 올 수 있지만, 결과를 살피고 품질을 평가할 도구와 이를 검토할 분야 전문가가 필요하다고 봤다. 초기 완성본은 프로젝트 저장소에서 확인할 수 있다.
PIDE MCP와 다른 Isabelle 연동 접근법을 비교한 자료는 PIDE MCP 프리프린트에서 볼 수 있다. Isabelle용 다른 MCP 도구인 I/Q도 소개됐다.
댓글 (0)
로그인하면 이 기사에 내 생각을 남길 수 있어요