기술 요약: Visored: LLM 생성 수학을 위한 제어된 자연어 프로버(Prover)

문제 정의

대규모 언어 모델(LLM)은 수학적 추론 능력에서 향상된 역량을 보여주었으나, 환각(hallucination) 현상에 취약하다는 한계가 있다. 결과적으로, AI가 생성한 증명은 그 검증 과정이 얼마나 신뢰할 수 있느냐에 따라 그 가치가 결정된다. 자동 정리 증명기(ATP)나 전체 증명 모델(예: Lean 또는 Rocq를 대상으로 하는 모델)은 miniF2F와 같은 벤치마크에서 높은 통과율을 달est하지만, 일반적으로 이미 정형화된 문장을 입력값으로 요구한다. 핵심적인 병목 구간은 자동 정형화(autoformalization), 즉 비정형 수학 산문(prose)을 기계가 검증 가능한 형태로 번역하는 과정에 있다.

이 번역 작업은 매우 까다로운데, 이는 비정형 수학이 공유된 배경 지식, 암묵적인 부수 조건(예: $x \neq 0$), 그리고 독자가 자동으로 채워 넣는 표기법의 남용에 의존하기 때문이다. 정형 언어로의 직접적인 번역은 특정 라이브러리의 보조 정리(lemma), 하위 타입(subtype), 예외 케이스 관례, 그리고 형변환(coercion, 예: $\mathbb{N}$ vs $\mathbb{Z}$ vs $\mathbb{R}$) 등을 결정해야 하며, 이러한 결정들은 원문에는 흔적을 남기지 않는다. 이러한 결정 과정에서의 오류는 컴파일 에러로 나타나기보다는, 문장은 컴파일되지만 원래의 의도를 반영하지 못하게 되는 "침묵하는 의미적 드리프트(silent semantic drift)"로 나타나는 경우가 많다.

방법론

Visored는 LaTeX와 Lean과 같은 저수준 프로버 사이에 위치하는 **의존 타입 중간 표현(dependently-typed intermediate representation, IR)**을 도입함으로써, 비정형 수학 글쓰기와 정형 검증 사이의 간극을 메우기 위해 설계된 연구 프로토타입이다.

핵심 아키텍처

시스템은 다음과 같은 단계로 구성된 파이프라인(논문의 그림 2 참조)으로 작동한다:

1. 제어된 자연어(CNL) 입력: Visored는 LaTeX 내에 임베딩된 수학적 영어의 제어된 부분 집합을 수용한다. 어휘(예: "Let...", "Assume...", "Then..."과 같은 문장 템플릿 및 LaTeX 명령어)는 외부 .lpcsv 사양 파일에 의해 정의되며, 이를 통해 시스템을 수정하지 않고도 표면 언어를 확장할 수 있다.
2. 구문 및 의미론(Syntax and Semantics): 입력은 구문 트리로 파싱된 후 **타입이 지정된 AST(sem AST)**로 정교화(elaboration)된다. 이 단계에서는 이름을 해결하고, 타입과 종류(kind)를 할당하며, **잘 정의됨(well-definedness)**을 타입 체크 시점에 강제한다. PVS의 전통을 따라, 부분 함수(예: $1/x$, $\sqrt{x}$, $\log x$)는 암묵적인 가설 인자(예: $x \neq 0$, $x \ge 0$)를 가지며, 이들은 식이 수용되기 전에 반드시 해소되어야 한다.
3. 중간 단계 IR (MIR): 타입이 지정된 AST는 솔버의 기질(substrate)인 Visored MIR로 낮아진다(lowered).
4. 비용 제한 솔버(Cost-Bounded Solver): 솔버는 "Then..." 의무 사항과 잘 정의됨 조건을 규칙 기반의 비용 제한 엔진(이름: "Miracle")을 사용하여 해소한다. 이 엔진은 ProofGrader에서 영감을 받은 순방향 및 역방향 규칙 데이터베이스와 특화된 택틱(tactic, 예: 대수적 정규화 도구, 체인 솔버)을 사용하여 수학자들이 보통 생략하는 일상적인 단계들을 닫는다(close).
5. 선택적 Lean 방출(Emission): 수락된 증명은 Lean 4로 트랜스파일될 수 있다. 이는 외부 커널 검증을 위한 선택적인 다운스트림 단계이다. 트랜스파일 과정은 정규화 이력을 재현하고 숫자 체계 간의 형변환 증거(coercion witnesses)를 관리하는 과정을 포함한다.

설계 철학

Visored는 두 가지 주요 관찰을 바탕으로 구축되었다:

1. LLM 유창성: LLM은 압도적으로 비정형 수학 데이터로 학습된다. CNL 표면 언어는 LLM이 이미 유창한 영역에 가깝게 유지되므로, 모델이 저수준 프로버의 구문(택틱, 라이브러리 보조 정리 이름 등)을 처음부터 배울 필요가 없다.
2. 다루기 쉬운 복잡도: 자연적 추론과 정형적 추론 사이를 잇는 것은 완전 자동 정리 증명보다 더 다루기 쉽다. LLM이 CNL로 증명 개요를 제공하게 함으로써, 솔버는 작은 단위의 명백한 단계들을 닫는 데 집중할 수 있으며, 이는 현대적인 에이전트 엔지니어링의 범위 내에 있는 작업이다.

본 시스템은 "상향식(upward)" 의미론적 파싱(LaTeX $\to$ Visored)을 LLM이 처리해야 할 어려운 문제로 보고, "하향식(downward)" 투영(Visored $\to$ Lean)을 결정론적이고 기계적인 프로세스로 취급한다.

주요 기여

• 자동 정형화를 위한 의존 타입 IR: Visored는 LaTeX에 표면적인 흔적이 없는 모든 결정(하위 타입, 라이브러리 보조 정리, 예외 케이스 관례, 형변환 등)이 명시적으로 드러나는 의미론적으로 풍부한 IR을 도입한다.
• 사양 기반 확장성: CNL 표면은 하드코딩된 파서가 아닌 외부 설정 파일에 의해 정의되므로, 시스템을 재컴파일하지 않고도 특정 수학적 관례(교과서, 경시 대회, 연구 등)에 맞춰 어휘를 조정할 수 있다.
• 국소적 진단(Localized Diagnostics): 전체 Lean 컴파일 후에 단일 accept/reject 판정을 내리는 시스템과 달리, Visored는 정교화(elaboration) 또는 솔빙 단계에서 국소적인 진단을 제공한다. 이를 통해 LLM이 특정 오류를 찾아내고 수정할 수 있는 "검증 및 수정(verify-and-revise)" 루프를 가능하게 한다.
• 잘 정의됨(Well-Definedness) 강제: 시스템은 대상 프로버의 총체화(totalization) 관례에 의존하는 대신, 솔버에 의해 해소되는 암묵적 가설 인자를 통해 잘 정의됨(예: $1/x$ 이전에 $x \neq 0$ 보장)을 강제한다.
• 기존 학파의 통합: Visored는 Mizar/Naproche(CNL 표면), PVS(타입 체크 시점의 잘 정의됨), Lean/Rocq(의존 타입), 그리고 ProofGrader(비용 제한 규칙 기반 솔빙)의 요소들을 하나의 LLM 친화적인 파이프라인으로 합성한다.

실험 결과

저자들은 개발 및 평가 세트로 사용된 miniF2F-valid 분할(244문제)에 대한 커버리지 연구를 보고하였다.

• 성능: CNL 표면을 설명하는 스킬 문서를 가이드로 삼은 LLM 코딩 에이전트(Claude)는 244문제 중 222문제(91%)에 대해 Visored로 검증된 증명을 생성했다.
• 세부 내역:
  • 귀납법(Induction): 100% (8/8)
  • 대수(Algebra): 98% (86/88)
  • 정수론(Number Theory): 97% (66/68)
  • AMC/AIME: 93% / 87%
  • IMO (올림피아드): 35% (7/20)
• 실패 분석: 해결되지 않은 문제들은 LLM의 증명 전략 수립 능력 부족이 아니라, Visored의 규칙 데이터베이스의 공백(예: 산술-기하 평균 부등식 누락, 유한체 타입 부재, 삼각 항등식 등) 또는 프로토타입의 퇴보(regression) 때문인 것으로 분석되었다. 저자들은 필요한 "기제(machinery)"가 아직 시스템에 구현되지 않았기 때문에 에이전트가 문제를 풀지 못한 것이라고 명시했다.
• 트랜스파일 비용: 현재의 희소한 방출 방식은 매우 장황한 Lean 출력을 생성하며, 수동으로 작성된 Lean 증명 대비 중앙값 라인 수 비율은 약 $250\times$이며, 최댓값은 $\approx 25,000\times$에 달한다. 이는 정규화 단계와 형변환 증거를 재현하기 때문이다.

의의 및 주장

본 논문은 Visored를 경쟁적인 자동 정리 증명기가 아니라, **AI가 생성한 비정형 수학을 검증하고 조직하기 위한 새로운 인프라의 개념 증명(PoC)**으로 포지셔닝한다.

• 겸허한 주장: 저자들은 자동 정리 증명 분야에서 경쟁적인 성능을 주장하지 않으며, 홀드아웃(held-out) 테스트 분할으로 결과를 일반화하지도 않는다. 91%의 커버리지는 튜닝된 통과율이 아니라, 설계가 표현할 수 있는 능력의 하한선으로 제시된다.
• 병목 구간의 변화: 본 연구는 AI 수학의 제약 조건이 "아이디어 생성"에서 "생성된 아이디어를 규모 있게 검증하고 조직하는 것"으로 이동하고 있다는 견해를 뒷받침한다.
• 활용 모드: Visored는 네 가지 모드로 작동하도록 설계되었다:
  1. 추론 시 검증기(Inference-time verifier): LLM 출력에 대한 실시간 체커.
  2. 자동 정형화 루프(Autoformalizer loop): 국소적 진단을 바탕으로 증명을 재작성하는 LLM 메커니즘.
  3. 밀집된 보상 신호(Dense reward signal): 강화 학습(RL)을 위한 단계별 피드백 제공.
  4. CNL 데이터 생성기(CNL data generator): 자연스럽게 읽히면서도 정형적으로 검증된 증명 코퍼스를 재생산 가능하게 생성.

결론적으로, CNL 표면, 의존 타입 IR, 그리고 규칙 기반 솔버의 결 조합은 실패 지점이 국소화되고 실행 가능하게 만들어, 현재의 직접적인 자동 정형화 방식보다 비정형 산문으로부터 커널 검증된 증명으로 가는 더 신뢰할 수 있는 경로를 제공한다. 해결되지 않은 문제들은 설계의 근본적인 한계가 아니라, 누락된 규칙과 기제의 백로그(backlog)를 나타낸다.