🤖 AI

Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization

이 논문은 성공적인 자동 형식화(autoformalization)는 단순히 증명되지 않은 공백("sorries")의 부재가 아니라 정의의 품질과 API 설계에 대한 전문가 검토에 의해 평가되어야 한다고 주장하며, 그로텐디크의 소멸 정리(Grothendieck's vanishing theorem)에 대한 사례 연구를 통해 AI 에이전트가 국소적인 기계적 수정은 효과적으로 적용할 수 있지만 고차원적인 개념 설계에는 어려움을 겪는다는 점을 입증한다.

원저자: Vasily Ilin, Brian Nugent

게시일 2026-06-15

📖 4 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Vasily Ilin, Brian Nugent

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

당신이 집을 지어달라고 아주 빠르고 의욕 넘치는 견습생을 고용했다고 상상해 보십시오. 당신은 그들에게 설계도(수학 정리)와 그 집을 짓는 법을 설명하는 교과서의 한 장을 건네줍니다.

견습생은 밤낮으로 일합니다. 벽돌을 쌓고, 골조를 세우고, 지붕을 얹습니다. 작업이 끝나면 집이 완성됩니다. 집은 무너지지 않고 똑바로 서 있습니다. 검사관(컴퓨터)이 말합니다. "훌륭합니다! 구조적으로 안정적이군요."

이 논문은 그 다음에 일어나는 일에 관한 것입니다.

이 논문의 저자들은 이렇게 물었습니다. "단순히 집이 서 있다고 해서, 그것이 정말 '좋은' 집일까? 다른 사람이 살 수 있을까? 나중에 2층을 쉽게 증축할 수 있을까, 아니면 벽을 다 허물어야 할까?"

이들의 실험 과정을 쉬운 비유를 들어 설명하면 다음과 같습니다.

실험: "수학적 집" 짓기

연구팀은 AI(대규모 언어 모델)에게 **그로텐디크의 소멸 정리(Grothendieck's Vanishing Theorem)**라는 복잡한 수학 정리를 형식화하도록 요청했습니다. 이 정리는 매우 구체적이고 수준 높은 건축적 도전 과제라고 생각하면 됩니다.

그들은 AI에게 다음을 제공했습니다:

목표 (정리의 문장)
교과서에 나온 증명 (지침)
규칙: "이미 우리가 가진 기존의 표준 도구들(수학 라이브러리)만을 사용해야 한다."

1단계: "통과" (상태 A)
AI는 열심히 작업하여 오류 없이 컴파일되는 코드를 만들어냈습니다. 수학 소프트웨어의 세계에서 오류는 "sorry"(아직 이것을 증명할 수 없다는 뜻)라고 불립니다. AI는 이 "sorry"의 개수를 0으로 줄이는 데 성공했습니다.

결과: 집이 서 있습니다. 컴퓨터는 만족합니다.
문제: 인간 전문가(수학자)가 그 집을 보고 말했습니다. "이건 재앙입니다."

전문가 리뷰: 왜 "서 있는 집"이 실패했는가

인간 전문가는 집이 무너지지는 않았지만, 형편없이 지어졌다는 것을 발견했습니다. 이를 일상적인 용어로 번landı면 다음과 같습니다.

1. "커스텀 도구" 문제 (정의/Definitions)

AI가 한 일: AI는 매번 아주 작은 작업을 수행할 때마다 자신만의 커스텀 도구를 계속해서 만들어냈습니다. 만약 벽 하나를 측정해야 한다면, 그 벽만을 위한 이상하고 새로운 줄자를 새로 만든 것입니다.
왜 나쁜가: 실제 라이브러리에서는 모든 사람이 사용할 줄 아는 표준 도구를 갖추길 원합니다. 만약 AI가 매 작업마다 커스텀 도구를 만든다면, 미래의 건축가들은 AI의 이상한 발명품들을 어떻게 사용하는지 모르기 때문에 그 집을 사용할 수 없게 됩니다.
판결: AI는 도구를 '사용'하는 데는 뛰어났지만, 도구를 '설계'하는 데는 형편없었습니다. AI는 62개의 커스텀 정의를 만들었지만, 그중 61개는 쓸모없거나 혼란스러웠습니다.

2. "어지러운 설계도" 문제 (API 디자인)

AI가 한 일: AI는 깔끔한 인터페이스(사용 설명서)를 구축하지 않았습니다. 대신, 누군가 무언가를 하고 싶을 때마다 벽을 열어 생벽돌을 그대로 보여주었습니다.
해결책: 전문가는 AI에게 사람들이 내부의 지저분한 속사정을 보지 않고도 수학과 상호작용할 수 있도록 "사용자 인터페이스(API)"를 구축하라고 요청했습니다.
결과: AI는 인터페이스를 구축하긴 했지만, 지저분했습니다. AI는 현재의 증명을 위해서만 존재하는 24개의 특수한 "규칙"을 추가했을 뿐, 몇 가지 우아하고 일반적인 규칙을 만들지는 못했습니다. 이는 마치 표준 전등 스위치를 설치하는 대신, 집 안의 모든 전등마다 각각 고유하고 복잡한 스위치를 설치한 것과 같습니다.

3. "근시안적" 문제 (정리 문장/Theorem Statements)

AI가 한 일: AI는 당장 주어진 일을 완수하는 데 필요한 것만 딱 맞춰서 증명했습니다. 이는 마치 지금 있는 틈새에만 딱 맞게 판자를 자르는 목수와 같습니다. 나중에 다른 틈새에도 쓰일 수 있도록 자르는 것이 아니라 말이죠.
판결: AI는 당면한 퍼즐을 푸는 데는 탁월하지만, "5년 뒤에 이 결과물을 사용할 사람에게 어떻게 유용하게 만들 수 있을까?"라고 생각하는 능력은 부족합니다.

"전과 후" 테스트

연구팀은 포기하지 않았습니다. 그들은 전문가의 피드백을 받아 AI에게 수정하도록 요청했습니다.

AI가 잘 고친 부분: 로컬 수정에는 뛰어났습니다. 전문가가 "이 파일의 이름을 바꿔라"라거나 "이 특정 숫자를 변경하라"고 하면 완벽하게 해냈습니다. 엉망인 부분을 정리할 수는 있었습니다.
AI가 고치지 못한 부분: AI는 여전히 처음부터 좋은 집을 설계하는 방법을 알아내지 못했습니다. 피드백을 받은 후에도 정의들은 여전히 투박했고, "사용자 인터페이스"는 여전히 비대했습니다.

핵심 교훈

논문은 다음과 같은 단순하고 강력한 아이디어로 결론을 맺습니다.

"간극을 메우는 것(코드가 컴파일되게 하는 것)은 쉬운 부분입니다."

어려운 부분은 설계입니다.

AI는 뛰어난 벽돌공과 같습니다: 어디에 벽돌을 놓아야 할지 정확히 알려준다면 벽돌을 완벽하게 쌓을 수 있습니다.
하지만 AI는 건축가가 아닙니다: 집이 어떤 모습이어야 하는지, 방들이 어떻게 흘러가야 하는지, 혹은 미래의 거주자들에게 어떤 도구가 필요할지를 결정할 수는 없습니다.

요점:
우리는 단순히 "AI가 수학 문제를 풀었는가?"를 물어서는 안 됩니다. "AI가 다른 사람들이 실제로 사용할 수 있는 것을 만들었는가?"를 물어야 합니다.

현재 AI는 퍼즐을 풀 수는 있지만, 라이브러리를 구축할 수는 없습니다. 진정으로 유용한 결과를 얻으려면, 인간 전문가가 나서서 설계와 조직화라는 핵심적인 작업을 수행해야 합니다. "어려운 부분"은 정리를 증명하는 것이 아니라, 그 증명이 미래를 위한 선물이 될지 아니면 짐이 될지를 결정하는 것입니다.

기술 요약: 'sorries'를 해결하는 것이 어려운 부분이 아니다

문제 정의

반자율적 형식화(semi-autonomous formalization)의 지배적인 서사는 증명 완성(proof completion), 즉 에이전트가 증명 보조기(예: Lean)가 검증된 정리로 받아들이는 코드를 생성할 수 있는 능력에 집중되어 있습니다. 그러나 저자들은 검증된 정리가 **재사용 가능한 라이브러리 기여(reusable library contribution)**와는 별개의 개념이라고 주장합니다. 현대 수학은 정의가 결합되어야 하고, 정리 문장이 적절한 일반성을 갖추어야 하며, 사용자가 구현을 직접 펼쳐보지(unfold) 않고도 미래의 추론을 용이하게 할 수 있는 API를 갖추어야 하는 상호 연결된 라이브러리에 의존하고 있습니다.

식별된 핵심 문제는, LLM이 로컬 증명 간극(미해결된 목표인 "sorries")을 메우는 데는 점점 더 능숙해지고 있지만, 고품질의 유지보수 가능한 형식화를 위해 필요한 **글로벌 설계 결정(global design decisions)**에는 어려움을 겪고 있다는 점입니다. 구체적으로, 에이전트는 적절한 정의를 선택하거나, 일반화 가능한 정리 문장을 설계하거나, 깔끔한 API를 구축하는 데 실패하곤 합니다. 그 결과, 코드가 커널(kernel)은 통과할지언정 전문가 리뷰 단계에서는 라이브러리 기여로서의 가치를 인정받지 못하는 결과물을 만들어냅니다.

방법론

본 논문은 Lean 4를 사용하여 그로텐디크 소멸 정리(Grothendieck's vanishing theorem; Hartshorne, 1977, Ch. III, Thm. 2.7)를 반자율적으로 형식화한 상세한 사례 연구를 제시합니다. 이 정리는 노터(Noetherian) 위상 공간 $X$ 와 $X$ 의 위상적 크룰 차원(topological Krull dimension)보다 큰 정수 $n$ 에 대하여, $X$ 위의 임의의 아벨 군 층(sheaf of abelian groups)의 $n$ 차 층 코호몰로지(sheaf cohomology)가 소멸한다는 내용을 담고 있습니다.

본 연구는 **전후 실험 설계(before-and-after experimental design)**를 따릅니다:

상태 A (초기 형식화): 인간이 제공한 정리 문장과 Hartshorne의 증명이 담긴 PDF 발췌본을 바탕으로, 에이전트(Claude Code)가 "sorries"(증명되지 않은 목표)가 하나도 없는 상태로 컴파일되는 형식화를 생성했습니다.
전문가 리뷰: Lean/mathlib 전문가가 상태 A를 검토하여 정의, 정리의 일반성, 파일 구조 및 API 설계에서의 문제점을 식별했습니다.
상태 B (리팩토링된 형식화): 에이전트에게 전문가의 체크리스트를 해결하도록 과제가 부여되었습니다. 여기에는 mathlib 컨벤션에 맞추기 위한 "리뷰 기반 리팩토링"과 후속 "압축 및 연마(compression and polish)" 단계가 포함되었습니다.
2차 리뷰: 동일한 전문가가 상태 B를 검토했습니다.

분석은 정의, 정리 문장, 증명, 그리고 파일/API 구조라는 네 가지 차원에서 두 상태를 비교합니다. 프로젝트 타임라인, 토큰 사용량, 도구 상호작용은 커밋 로그와 텔레메트리를 통해 재구성되어 에이전트의 행동 패턴을 파악하는 데 사용되었습니다.

주요 결과 및 발견

1. 정의: 주요 실패 지점

정의는 가장 취약한 구성 요소로 식별되었으며, 에이전트가 상태 A에서 상태 B로 넘어가면서 개선을 거의 보여주지 못한 영역이었습니다.

상태 A: 에이전트는 62개의 커스텀 정의를 생성했습니다. 그중 단 하나(TopCat.closedIncl)만이 올바르고 재사용 가능하다고 판단되었습니다. 나머지는 "임시방편적(ad hoc)"이었으며, 기존의 표준 라이브러리 구성을 현재의 증명 맥락에 특화된 이름(예: sheafSections 대신 sheafH_filtered_colimit_h1_sectionsFunctor)으로 감싸는 형태였습니다.
결과: 이러한 정의들은 "미래의 전송 비용(future transport costs)"을 발생시켜, 이후의 사용자들이 객체를 사용하기 위해 사소한 동치 관계를 증명해야 하는 상황을 강요했습니다. 또한, 기저의 구문을 가림으로써 타틱(tactic) 성능(예: simp)을 저해했습니다.
상태 B: 에이전트는 일반적이고 재사용 가능한 정의를 만드는 능력에서 유의미한 개선을 보이지 못했습니다. 에이전트는 편리한 특수화를 가진 일반적인 구조를 설계하는 대신, 계속해서 특수하고 불필요한 객체를 만들어냈습니다.

2. API 설계: 부분적 개선

상태 A: 에이전트는 층 코호몰로지(Sheaf.H)를 위한 API를 구축하지 못하고, 하위 파일들에서 해당 정의를 반복적으로 펼쳐서(unfolding) 사용했습니다.
상태 B: 에이전트는 전용 API 파일을 생성하여 하위 증명들을 정리했습니다. 그러나 이 API 자체는 약 800줄에 달하며 24개의 매우 특수한 렘마(lemma)를 포함하는 등 "노이즈가 많고 비대(bloated)"했습니다.
대조: 에이전트는 topologicalKrullDim(더 단순한 정의)에 대한 API 설계에서는 더 나은 성능을 보였는데, 이는 에이전트가 특정되고 제한된 작업이 주어졌을 때는 좋은 API를 설계할 수 있지만, 개방형 설계에는 어려움을 겪음을 시사합니다.

3. 정리 문장: 로컬 vs 글로벌

상태 A: 에이전트는 당장의 증명에 필요한 것만을 정확히 증명했으며, 이 과정에서 지나치게 구체적인 가설(예: 일반적인 단축 완전열(short exact sequence)로 충분함에도 불구하고 "단사 프레젠테이션(injective presentation)"을 요구함)을 사용하는 경우가 많았습니다.
상태 B: 에이전트는 리뷰 체크리스트에서 명시적으로 요청받았을 때 정리 문장을 성공적으로 일반화했습니다. 그러나 스스로 필요한 일반화를 식별하지는 못했습니다. 에이전트는 로컬한 구문적 수정에는 뛰어나지만, 미래의 재사용 필요성을 예측하는 글로벌한 판단력은 부족합니다.

4. 증명: 불균형한 개선

상태 A: 증명들은 "have 문장의 벽"을 포함하고 있었고, 정의적 동등성(definitional equality)을 빈번하게 오용하며 정의를 직접 펼치는 양상을 보였습니다.
상태 B: 증명들이 개선되었으며, 특히 기존 mathlib 객체를 사용하는 파일들에서 그러했습니다. 에이전트는 복잡한 증명을 분해하기 위해 이름이 붙은 하위 렘마를 채택하는 패턴을 보였는데, 이는 "심박수(heartbeat, 성능)" 제약에 의해 강화된 패턴이었습니다.
한계: 에이전트 자신의 부실한 정의에 의존하는 증명(예: 필터드 콜리밋 파일들)은 여전히 읽기 어렵고 유지보수가 까다로운 상태로 남았습니다.

5. 프로세스 역학

피드백 적응: 에이전트는 명확한 완료 술어(예: "이 파일을 이름을 바꿔라", "이 가설을 일반화하라")에는 잘 적응했습니다. 하지만 역사실적 판단(예: "미래에 유용할 API를 설계하라")을 요구하는 피드백에는 어려움을 겪었습니다.
탈출구(Escape Hatches): 에이전트는 어려운 설계 결정에 직면했을 때 작업을 "차단됨(blocked)"으로 선언하거나 인프라(예: "mathlib gap")를 탓하는 경향이 있었습니다. 이를 강제하기 위해 이러한 표현을 금지하는 명시적인 프롬프트가 필요했습니다.
지표: "sorries를 닫는 것"은 품질을 측정하기에 불충분한 지표입니다. 프로젝트는 sorry 수가 0에 도달한 후에도 코드 라인 수와 구조 측면에서 계속해서 크게 진화했습니다.

의의 및 주장

본 논문은 자동 형식화 평가가 이진적인 증명 완성을 넘어서야 한다고 주장합니다. 저자들의 주장은 다음과 같습니다:

커널 수락은 불완전하다: 정리가 커널에 의해 검증될 수는 있으나, 그 과정에서 미래의 사용자들에게 어색한 형변환(coercion), 중복된 정의, 관리 불가능한 API를 강요할 수 있습니다.
"재사용성 격차(Reusability Gap)": 에이전트의 로컬 목표를 닫는 능력과 정의를 선택하고 API를 설계하는 능력 사이에는 뚜렷한 차이가 존재합니다. 후자는 현재의 LLM이 결여하고 있는 미래의 재사용성에 대한 판단력을 요구합니다.
평가 표준: 저자들은 AI-for-math 시스템이 결과물로 나온 형식화가 전문가 리뷰를 견뎌낼 수 있는지에 의해 평가되어야 한다고 제안합니다. 구체적으로, 증명이 완료된 후, 전문가가 공용 정의, 정리 문장, 네임스페이스, API 표면을 검토하여 시스템의 설계 피드백 대응 능력을 측정해야 합니다.

본 연구는 글로벌 설계를 위한 정교한 장치가 없다면, LLM은 "검증된 산출물"은 만들 수 있어도 아직 "재사용 가능한 라이브러리 기여"는 할 수 없다고 결론짓습니다. 향 $\는 방향은 인간 전문가가 품질 규격(정의, 인터페이스)을 정의하고, 에이전트는 좁고 기계적으로 체크 가능한 리팩토링을 처리하도록 하는 것입니다.