재귀 Lean 증명 에이전트로 실제 코드 검증 난제를 공략한다
Scaling Lean Theorem Proving for Real-World Code Verification
무엇인가
이 논문은 LLM과 Lean 4를 결합해 수학 정리와 프로그램 정합성 명제를 기계 검사 가능한 증명으로 해결하는 에이전트 시스템을 다룬다. 기존 형식 추론 벤치마크는 포화에 가깝고 검증 벤치마크는 수백 개 규모라 기억·오염 위험이 있으며, 테스트 기반 보상은 테스트 하네스를 악용할 수 있다는 문제의식에서 출발한다. 목표는 커널이 검사한 증명 또는 반증을 라벨로 삼아 난이도와 신뢰를 함께 확보하는 것이다.
어떻게 동작하나
EasyProver는 Lean 4 환경 Γ와 명제 P가 주어지면 P 또는 ¬P의 커널 검사 증명을 찾는다. 목표 정리 서명까지의 파일 앞부분은 고정되고 증명 본문만 수정할 수 있다. 완료 주장은 Lean Comparator가 lake env lean과 #print axioms를 읽기 전용 툴체인으로 다시 돌려 통과해야 하며, sorry가 있거나 공리 허용 목록을 벗어나면 거부된다. 하네스는 추가 학습 없는 Anthropic Fable-5를 쓰고, 부모 에이전트가 자식 에이전트를 만들어 대안 전략과 보조 정리를 탐색한다. 각 자식은 격리된 컨텍스트와 프로젝트 사본을 받고 완성 증명, 반례, 부분 결과를 반환하며, 부모는 그 내용을 읽어 계속·수정·확장을 결정한다. UCT처럼 방문 횟수나 롤아웃 평균으로 노드 값을 매기지 않는다.
무엇과 다른가
병렬 전술 탐색은 현재 증명 상태에서 여러 전술과 자동화 도구를 동시에 시도하고 성공한 것만 남긴다. InfiniLean은 Lean 소스를 JSON-RPC로 받는 무상태 서비스로, 고정된 Lean/Mathlib 버전의 복제본 풀과 워커 재사용으로 가져오기 비용을 줄인다. 원문에 따르면 워커의 가져오기는 수십 초, 데워진 워커의 정교화는 약 0.2초이며 Kubernetes 오토스케일링을 쓴다. 하네스 프로세스별로 활성 하위 에이전트 64개, 동시 고비용 Lean 질의 16개로 제한한다. 후보 증명은 잠금 아래 해법 파일로 승격되고 빌드·수용 기준 재검사를 통과해야 하며 실패하면 되돌리고, 첫 수용 후보에서 탐색을 끝낸다.
어떻게 쓰나
Aegis는 경쟁 프로그래밍 문제를 실제 구현 위의 Lean 검증 과제로 바꾼다. 코딩 에이전트가 안전한 Rust 풀이를 작성하고, cargo test로 참조 사례를 통과시킨 뒤 Charon으로 추출하고 Aeneas로 실행 가능한 Lean 모델로 번역한다. 같은 입력에서 Rust 출력과 Lean 출력이 모두 일치해야 하며, 2,356문제 중 2,045개(86.8%)가 Rust 테스트, 추출, 번역, Lean 정교화, 차등 평가 전 단계를 통과했다. 이후 명세 에이전트가 원 문제, 추출된 Lean 프로그램, 서명, 차등 검증 예제를 보고 sorry 본문을 가진 정교화되는 정리문과 자연어 설명을 작성하고, 중복·자명·공허한 명세와 정교화 오류를 걸러 고정한다.
전제와 한계
번역된 프로그램은 수학 함수가 아니라 기계어 폭 산술과 실패를 드러내는 구현이라 Result α와 모나드 시퀀싱, Std.U32/Std.I64의 .val 투영, 캐스트 범위 의무가 붙는다. 루프는 ControlFlow를 반환하는 본문과 루프 결합자, 가변 변수 튜플로 바뀌고 중첩 루프는 보조 정리로 아래에서 위로 다뤄야 한다. 읽기 전용 입력은 Slice, 가변 작업 저장소는 Vec이며 index_mut는 갱신된 벡터를 재구성하는 역방향 함수를 함께 반환해 리스트 갱신·길이 보존·불변식 증명을 요구한다. 선택적으로 Plausible 속성 기반 테스트로 반례를 먼저 찾지만, 반례도 Lean 검사 뒤에만 반증 라벨이 되고 양성 라벨은 만들지 않는다. 증명 또는 반증 결과는 명세가 요청한 극성과 맞으면 확인, 반대면 불일치로 표시되고 미해결은 신호를 주지 않으며 RLVR 보상으로도 쓸 수 있다.
수학 벤치마크에서 EasyProver는 PutnamBench 672개 중 669개(99.6%)를 풀었고, 이는 Chung 등이 보고한 가장 강한 구성 597/672보다 72개 많다. IMO 2026 형식화 6개와 Putnam 2025 12개도 모두 풀었다. 저자들은 IMO 2025와 USAMO 2026은 평가하지 않았고 다른 시스템의 공개 결과만 비교했다고 밝힌다. 코드 검증에서는 VERINA 189/189, AlgoVeri 77/77, NTP4VC 600개 중 597개(99.5%, 증명 588·반증 9)를 해결했고, Lean 4.32 툴체인으로 번역되는 CLEVER 143개 중 113개(79.0%)를 해결했다.
Aegis는 11,533개 후보 명세를 만들었고, LeetCode 난이도와 명세 범주로 층화한 1,257개 프로그램의 2,000개 명세 표본을 평가했다. 이 표본은 Plausible로 이미 반증된 명세와 실패를 요청한 범주를 제외했고, 명세당 30분 예산에서 1,997개를 시도해 1,054개(표본의 52.7%)를 증명했으며 943개는 미해결로 남겼다. 증명률은 경계 사례 명세 84.1%에서 명시적 계약 31.0%까지, Easy 66.7%에서 Hard 37.6%까지 걸쳤다. 기존 벤치마크를 거의 포화시킨 동일 증명기가 여기서는 절반 가까이 해결하지 못했다.
개발자 관점에서 이 시스템은 Lean 기반 코드 검증 자동화를 서비스로 붙일 때 참고할 만한 수용 설계를 보여준다. 에이전트의 성공 보고가 아니라 고정된 명제, 허용 공리, 커널 검사, 독립 재검사를 통과해야 채택하므로 검증 파이프라인의 신뢰 경계를 어디에 둘지 판단할 수 있다. 또한 Rust에서 Lean으로 번역한 구현 자체에 명세를 걸기 때문에 손으로 쓴 수학 함수가 아니라 기계어 폭 산술·실패·루프·가변성을 포함한 실제 구현 의무를 다룬다. 다만 Aegis는 상태 기반·클래스 인터페이스, 해시 테이블, 클로저, 중첩 참조, 제한 없는 별칭 같은 미지원 기능을 제외했고 입력 크기와 정수 범위를 제한하며 소수 부동소수점 문제만 허용 오차 비교를 쓴다. 하네스 구성 요소별 절제 실험은 각 설정마다 벤치마크 전체 실행이 필요해 하지 않았고, 같은 모델을 Lean 도구만 주고 하네스 없이 비교한 결과도 없다. Aegis를 다른 증명기로 평가하거나 강화학습·다중 교사 온폴리시 증류에 쓰는 일, 변이 프로그램으로 추가 과제를 평가하는 일은 향후 과제로 남겼다. 수학 벤치마크는 모델 학습 컷오프가 공개되지 않아 오염 가능성을 배제할 수 없지만, 저자들은 해석에는 영향을 주어도 커널 검사된 증명의 정확성에는 영향을 주지 않는다고 본다.