Lean 4와 AI 에이전트를 통한 형식 검증된 멀티폴리곤 교차 연산

형식 검증된 멀티폴리곤 교차 연산 개요

verified-polygon-intersection 프로젝트는 멀티폴리곤 교차 알고리즘에 대한 최초의 알려진 형식 검증된 구현체입니다. Lean 4 증명 보조 도구를 사용하여, 두 멀티폴리곤의 교차 영역(내부 점들의 집합으로 정의됨)이 가능한 모든 입력 구성에 대해 수학적으로 정확함을 보장하며, 이를 통해 계산 기하학에서 전통적인 테스트와 관련된 위험을 제거합니다.

계산 기하학 검증의 과제

계산 기하학 알고리즘은 입력 구성의 무한한 다양성과 희귀한 엣지 케이스의 존재로 인해 전통적인 테스트를 통해 검증하기가 매우 어렵기로 유명합니다.

무한한 입력 집합

멀티폴리곤의 내부는 무한한 점들의 집합이므로, 전통적인 테스트로는 두 집합의 교차가 코드에서 올바르게 표현되는지 철저히 검증할 수 없습니다. 형식 검증을 사용하면 내부 집합을 단순한 해석이 아닌 수학적 엔티티로 다룰 수 있습니다.

복잡한 엣지 케이스

십자 모양과 구멍이 있는 사각형의 교차와 같은 특수한 구성은 까다로운 과제를 생성합니다. 이러한 경우, 알고리즘은 세그먼트를 분할하고 폐쇄된 경계 구성 요소로 순서를 정해야 합니다. 프로젝트에서는 이 과정이 오일러 회로(Eulerian cycles)와 관련이 있으며, 알고리즘이 모든 경우에 작동하도록 보장하기 위해 증명해야 하는 사소하지 않은 사실임을 언급합니다.

신뢰할 수 있는 정확성을 위한 Lean 4 활용

알고리즘의 정확성에 대한 신뢰는 코드를 생성한 AI에 대한 신뢰가 아니라, Lean 체커와 최소화된 명세(specification)에 대한 인간의 검토에서 비롯됩니다.

최소한의 인간 검토

인간 검토자의 부담을 최소화하기 위해, 프로젝트는 명세와 구현을 분리합니다. 검토자는 DataStructures.lean, Defs.lean, 그리고 MultipolygonIntersectionAlgorithmWithPreconditionCheck.lean 세 개의 파일만 검토하면 됩니다. 이 파일들은 약 87줄의 간단한 Lean 명세를 구성합니다. 실제 구현과 증명은 훨씬 더 크고 복잡하지만, Lean 체커에 의해 자동으로 검증됩니다.

공리 검증

AI 에이전트가 증명 과정에서 원치 않거나 타당하지 않은 공리를 도입하지 않도록 하기 위해, 프로젝트는 사용자가 정리가 정리의 의존성을 갖는 공리를 검사할 수 있도록 허용합니다. 현재 구현은 propext, Classical.choice, 그리고 Quot.sound와 같은 신뢰할 수 있는 공리들에만 의존합니다.

형식 증명에서의 AI 에이전트 능력의 진화

이 프로젝트의 개발은 LLM이 형식 검증 작업을 처리하는 능력, 특히 인간의 스케치를 번역하는 단계에서 자율적인 전략 수립 단계로 이동하는 중요한 도약을 보여줍니다.

모델 진화 과정

Claude Opus 4.5/4.6: 이 모델들은 사소하지 않은 Lean 증명을 처리할 수 있었지만, 인간 개발자가 완벽하게 엄격한 증명 스케치를 제공해야 했습니다. 예를 들어, 내부 집합 정의가 광선 방향에 독립적임을 증명하는 것은 인간의 안내를 받아 많은 작은 단계로 나누어 증명해야 했습니다.
Claude Opus 4.7: 이 모델은 더 큰 단계를 밟을 수 있었고 임의의 두 폴리곤의 교차 존재성을 증명할 수 있었지만, 오일러 회로와 특정 까다로운 엣지 케이스에 관한 인간의 힌트가 여전히 필요했습니다.
Claude Opus 4.8 (Ultracode mode): 이 모델은 대규모 증명 전략을 자율적으로 수립하고 실행할 수 있는 능력을 보여주었습니다. 힌트 없이도 주요 폴리곤 교차 정리를 처음부터 다시 증명하는 데 성공했으며, 겹치는 세그먼트들을 처리하도록 알고리즘을을 확장했습니다. 이는 Opus 4.7이 실패했던 작업입니다.

AI 행동 변화

Opus 4.8의 중간 출력물을 관찰하면, 모델이 잘못된 중간 정리(theorem)의 위험을을 가장 효과적으로 처리한다는 것을 알정할 수 있습니다. 잘못된 정리에 걸려 넘어지는 대신, 모델은 이제 자신의 경로에 대해 의심을 품고 자율적으로 다른 전략으로 전환하거나 여러 접근 방식을 테스트하기 위해 병렬 서브 에이전트를 배치할 수 있습니다.

구현 상의 트레이드오프와 향후 과제

형식 검증을 도입하면 정확성은 보장되지만, 특정 실무적인 단점점들이 발생합니다. 저자는 AI 에이전트에게 구현을 형식적으로 검증하도록 강제하는 것이 종종 수학적 명세에 포함되지 않은 실은 더 느리거나 실무적인 최적화가 누락된 코드를 생성하게 만든다고 언급합니다. 이는 검증의 어려움 때문에 AI가 더 단순하고 증명 가능한 코드로 유도되기 때문입니다.

향후 로드맵

성능 최적화: 구현체의 실행 속도를 측정하고 개선하기.
증명 단순화: 최신 AI 모델을 사용하여 현재 증명 과정의 불여필요한 우회 경로를 제거하기.
기능 확장: SVG 가져오기 및 내보내기 기능 추가하기.