[Paper] 추론 중심 LLM 기반 자동 정리 증명

Source: arXiv - 2604.19558v1

Overview

이 논문은 대형 언어 모델(LLM)과 Coq 정리 증명기를 결합한 새로운 증명 보조 에이전트인 ReCent‑Prover를 소개한다. LLM에게 보다 “추론‑중심” 역할을 부여하여—증명 단계를 명시적으로 계획하고 자체 출력을 비판하도록 함으로써—이 시스템은 동일한 LLM 호출 예산 내에서 CoqStoq 벤치마크의 자동 정리 증명을 크게 향상시킨다.

주요 기여

• Reflection을 통한 검증 – LLM이 생성한 전술을 확인하고, 전술이 잘못될 가능성이 있을 때 간결한 실패 요약을 생성하며, Coq에 도달하기 전에 이를 폐기하는 피드백 루프.
• 계획을 통한 검색 – 부분 목표 유사도만으로 보조정리를 검색하는 대신, LLM이 먼저 고수준 증명 계획을 스케치하고 그 계획에 맞는 보조정리를 가져와 검색을 전략적 의도와 일치시킴.
• 예산 인식 설계 – 두 새로운 구성 요소가 LLM 호출 횟수를 증가시키지만, 저자들은 전체 추론 예산을 일정하게 유지하여 호출을 보다 스마트하게 사용하면 무차별 생성보다 효율적임을 보여줌.
• 실증적 향상 – CoqStoq 벤치마크에서 ReCent‑Prover는 이전 최고 시스템에 비해 증명된 정리 수를 22.58 % 상대적으로 증가시킴.

방법론

1. 계획을 위한 프롬프트 엔지니어링 – LLM은 정리의 설명을 받고 짧고 높은 수준의 증명 개요를 출력하도록 요청받습니다 (예: apply induction on n, then use lemma X).
2. 계획 기반 검색 – 개요를 레마 데이터베이스에 대한 질의로 사용합니다. 의도된 전술(예: 귀납 레마, 산술 레마)과 일치하는 레마만 검색되어 잡음이 감소합니다.
3. 전술 생성 – LLM은 검색된 레마와 계획을 바탕으로 구체적인 Coq 전술을 합성합니다.
4. 반사 루프 – 전술을 Coq에 보내기 전에 시스템은 가벼운 정적 검사(형식 검사, 목표 매칭)를 수행하고 LLM에게 반사하도록 요청합니다. LLM은 전술이 실패할 수 있는 이유를 설명하는 짧은 “실패 요약”을 반환하여, 시스템이 비용이 많이 드는 Coq 호출 없이 전술을 폐기하거나 수정할 수 있게 합니다.
5. 반복 실행 – 증명이 완료되거나 LLM 예산이 소진될 때까지 이 과정을 반복합니다.

모든 단계는 Python으로 작성된 얇은 컨트롤러에 의해 조정되며, 무거운 작업(언어 이해, 계획, 반사)은 API 호출을 통해 표준 LLM(예: GPT‑4 또는 Claude)에 위임됩니다.

결과 및 발견

• 증명된 정리: ReCent‑Prover는 동일한 LLM 호출 횟수 하에서 CoqStoq에서 기존 최첨단보다 22.58 % 더 많은 정리를 해결합니다.
• 효율성: 반사 단계는 초기 단계에서 ~30 %의 잘못된 전술을 걸러내어 비용이 많이 드는 Coq 상호작용 횟수를 줄입니다.
• 전략적 검색: 계획 기반 검색은 순수 하위 목표 유사도 검색에 비해 레마 관련성을 ~45 % 향상시켜 증명 스크립트를 더 짧게 만듭니다.
• 소거 연구: 반사 또는 계획 중 하나를 제거하면 성능이 기준 수준으로 떨어져 두 구성 요소가 모두 필수임을 확인합니다.

실용적 함의

• 개발자용 증명 보조 도구: 추론 중심 LLM을 통합하면 인터랙티브 정리 증명기가 보다 자율적으로 동작하게 되어, 개발자들이 현재 겪고 있는 수동적인 “검색‑및‑적용” 사이클을 줄일 수 있습니다.
• 형식 검증을 위한 CI/CD: 보다 빠르고 신뢰할 수 있는 자동 증명 생성은 형식 검증 단계를 비용이 많이 드는 연산 없이 연속 통합 파이프라인에 통합할 수 있음을 의미합니다.
• 형식 방법 교육을 위한 도구: 학생들은 전술을 제안할 뿐만 아니라 제안이 실패한 이유를 설명해 주는 보조 도구를 통해 오류를 학습 기회로 전환할 수 있습니다.
• 크로스 도메인 검색: 계획 기반 검색 아이디어는 고수준 계획이 재사용 가능한 구성 요소 선택을 안내해야 하는 다른 분야(예: 코드 합성, 데이터 파이프라인 구축)에도 적용할 수 있습니다.

제한 사항 및 향후 연구

• LLM 의존성: 이 접근 방식은 기본 LLM의 품질에 의존합니다; 저렴한 모델은 신뢰할 수 있는 반성이나 계획을 제공하지 못할 수 있습니다.
• 정리 데이터베이스의 확장성: 정리 라이브러리가 커짐에 따라 검색 속도가 병목이 될 수 있습니다; 인덱싱 전략에 대한 추가 연구가 필요합니다.
• Coq 외 일반화: 시스템은 Coq의 전술 언어에 밀접하게 결합되어 있습니다; 이를 다른 증명 도우미(예: Isabelle, Lean)에 적용하려면 비단순한 엔지니어링이 필요합니다.
• 예산 민감도: 저자들은 LLM 호출 예산을 고정했지만, 실제 배포에서는 더 엄격한 지연 시간이나 비용 제약이 있을 수 있어 보다 공격적인 가지치기 또는 캐싱 기법을 탐구해야 합니다.

전반적으로 ReCent‑Prover는 LLM에 보다 전략적이고 자기 비판적인 역할을 부여하면 자동 정리 증명에서 상당한 향상을 이끌어낼 수 있음을 보여줍니다—이 통찰은 개발자들이 형식 검증을 위해 AI를 활용하는 방식을 재구성할 수 있습니다.

저자

• Yican Sun
• Chengwei Shi
• Hangzhou Lyu
• Yingfei Xiong

논문 정보

• arXiv ID: 2604.19558v1
• 분류: cs.SE
• 발행일: 2026년 4월 21일
• PDF: PDF 다운로드