EasyProver, Lean 정리 증명을 실제 코드 검증으로 확장

들어가며

자동 정리 증명의 평가 대상이 독립적인 수학 문제에서 실제 프로그램으로 이동하고 있다. 논문 ‘Scaling Lean Theorem Proving for Real-World Code Verification’은 Lean 기반 증명 시스템 EasyProver와 구현 중심 검증 과제를 생성하는 Aegis를 소개한다. 기존 벤치마크가 포화에 가까워진 상황에서, 현실적인 소프트웨어 검증 능력을 어떻게 측정할지에 대한 시도다.

검색을 확장하는 EasyProver

EasyProver는 별도 학습을 거친 전용 모델이 아니라, 기존 프런티어 모델을 여러 역할의 에이전트로 조직한다. 핵심 구성은 다음과 같다.

• 재귀 에이전트를 활용한 증명 목표 분해와 진행
• 탐색 분기별 격리 컨텍스트
• 비동기 탐색과 전술의 병렬 시도
• Lean의 분석과 타입 검사를 처리하는 탄력적 elaboration 서비스

PutnamBench에서는 672개 중 669개 문제를 증명했다. 자료에 제시된 IMO 2026 형식화 6개도 모두 완료했다. NTP4VC에서는 600개 중 597개 검증 조건을 해결했으며, VERINA의 189개 과제에는 모두 증명 또는 반박을 제시했다. 이는 모델의 규모뿐 아니라 탐색을 나누고 실행하는 시스템 설계가 자동 증명의 성능에 큰 영향을 준다는 점을 보여준다.

Aegis가 추가한 구현 수준의 난점

연구진은 기존 수작업 벤치마크가 지나치게 포화됐다고 보고 Aegis를 설계했다. Aegis는 경쟁 프로그래밍 문제에서 안전한 Rust 구현을 작성하고, Aeneas를 통해 이를 Lean으로 변환한 뒤 후보 사양을 생성한다. 고정된 각 명제에는 Lean 커널이 검사한 증명 또는 반박 라벨이 붙는다.

이 파이프라인은 차분 검증된 Rust-Lean 프로그램 쌍 2,045개와 후보 사양 11,533개를 생성했다. 과제에는 고정 폭 정수 산술, 명시적 실패 처리, 생성된 루프, 형 변환, 가변 연산의 함수화가 들어간다. 추상적인 정리만 다루는 벤치마크와 달리, 실제 구현의 세부 동작이 검증 난이도에 직접 반영된다.

2,000개 명제의 층화 샘플에서 EasyProver는 명제당 30분 제한 안에 1,054개를 증명했다. 비율은 52.7%다. 이 결과는 실제 코드 검증이 해결됐다는 뜻은 아니지만, 포화된 수학 벤치마크보다 시스템 간 차이를 더 분명하게 드러내는 평가 환경을 제공한다. Aegis 데이터는 다른 증명기의 평가나 강화학습 보상에도 활용할 수 있다.

의미와 남은 과제

이번 연구는 자동 증명의 발전을 단순한 정답률만으로 평가하지 않는 방향을 제시한다. 탐색 구조, 사양 생성, 프로그램 변환, 커널 검증 라벨이 함께 중요해지기 때문이다. Rust 구현을 Lean 표현으로 연결하면 추상 명제가 아니라 구체적인 프로그램 동작을 검증 대상으로 삼을 수 있다.

동시에 52.7%라는 수치는 현실적인 코드가 여전히 어렵다는 사실을 보여준다. 긴 프로그램 의존성, 사양의 품질, 반박 결과의 해석 가능성은 앞으로 해결해야 할 문제다. AI가 생성한 코드는 실행되는 것만으로 충분하지 않으며, 고정된 구현에 대해 기계가 확인할 수 있는 보장을 제공하는지도 평가받게 될 가능성이 커지고 있다.

출처: Hugging Face Daily Papers