Formally Solving Answer-Construction Problems in Lean

기술 요약: Lean에서의 정답 구성 문제의 형식적 해결

문제 정의
수학 경시 문제는 일반적으로 두 가지 범주로 나뉩니다: 정리 증명(주어진 명제를 검증)과 정답 구성(특정 성질을 만족하는 특정 객체를 생성). 최근 대규모 언어 모델(LLM)의 발전은 형식적 정리 증명을 크게 향상시켰으나, 형식적 정답 구성은 여전히 미개척 영역으로 남아 있습니다. 직관적 추론 시스템(추측에는 강하지만 형식적 검증에는 약함)과 형식적 증명 LLM(증명에는 최적화되어 있으나 존재 양화사(existential quantifiers)를 제거하기 위한 필요한 증거(witness)를 발견하는 데 어려움을 겪음) 사이에 결정적인 간극이 존재합니다.

정답 구성을 형식화할 때 발생하는 구체적인 과제는 **가용성(admissibility)**입니다. 표준 Lean 증명 검사기는 증명 항(proof term)이 올바른 타입을 갖는지 검증하지만, 생성된 증거가 정형화된(canonical) 폐쇄형(closed-form) 답변인지까지는 본질적으로 강제하지 않습니다. 예를 들어, 어떤 증명은 $\exists x, P(x)$라는 존재 명제를 만족하기 위해 명시적인 자연수(예: 245) 대신 비정형적 항인 sInf PropertySet(정의된 집합의 하한값)을 반환할 수 있습니다. 이러한 "순환적"이거나 "비폐쇄형"인 증거는 논리 내에서는 수학적으로 유효하지만, 경시 대회 답안으로는 부적격합니다.

방법론: 열거-추측-증명 (Enumerate-Conjecture-Prove, ECP)
이러한 과제를 해결하기 위해 저자들은 Lean 4에서 엔드 투 엔드 정답 구성 및 형식적 증명을 수행하도록 설계된 신경-기호적(neuro-symbolic) 프레임워크인 **ECP(Enumerate-Conjecture-Prove)**를 도입합니다. ECP는 형식적 검증 루프를 유지하면서 과정을 다음과 같이 구분합니다:

1. 문제 형식화 및 가용성 검사:

   • 문제는 함수 합성 작업으로 형식화됩니다: 즉, $\forall X, P(X) \to Q(X, \Psi(X))$를 만족하는 함수 $\Psi$를 찾는 것입니다.
   • 생성된 답안이 사전 정의된 "가용 어휘"(예: 특정 상수, 산술 연산자 및 표준 생성자)만을 사용하는지 보장하기 위해 **가용성 검사기(admissibility checker)**가 구현되었습니다. 이 검사기는 Lean 항에서 의미론적 상수를 구조적으로 추출하고, 행정적 상수(예: 타입클래스 인스턴스 또는 컴파일러 생성 아티팩트)와 비정형 정의(예: sInf)를 필터링합니다.

2. 열거 단계 (도구 지원 탐색):

   • 범용 LLM(예: GPT-5.4)에 Python 도구 실행 능력을 부여합니다.
   • LLM은 작은 도메인에 대해 유계 열거(bounded enumeration)를 수행하여 제약 조건을 만족하는 튜플을 찾는 Python 코드를 작성하고 실행합니다.
   • 이러한 실행 흔적(execution traces)은 패턴, 불변량 및 함수의 형태를 식별하기 위한 경험적 근거로 활용됩니다.

3. 추측 단계 (답안 합성):

   • 열거 단계의 증거를 사용하여 동일한 범용 LLM이 후보 답안 함수 $\Psi'$를 합성합니다.
   • 후보는 진행하기 전 두 가지 필터를 거칩니다:
     • 구문 검증(Syntactic Verification): 해당 항이 올바른 타입으로 Lean에서 컴파일되어야 합니다.
     • 가용성 검증(Admissibility Verification): 해당 항은 허용된 어휘 내의 상수만을 사용해야 합니다.
     • 만약 후보가 실패하면, 시스템은 실패 메시지를 프롬프트에 포함하여 반복합니다.

4. 증명 단계 (형식적 검증):

   • 유효한 후보 $\Psi'$가 구성되면, 시스템은 인스턴스화된 정리 $Stmt(T)|_{\Psi=\Psi'}$를 증명하려고 시도합니다.
   • 반박 루프(Refutation Loop): 증명을 시도하기 전에, 시스템은 부정(negation)을 증명함으로써 후보를 반박하려고 시도합니다. 만약 반박이 성공하면, 후보는 폐기되고 시스템은 추측 단계로 돌아갑니다.
   • 증명 생성: 반박이 실패하면, 시스템은 내장된 자동화 기능(예: simp, aesop, ring, norm_num 등의 택틱)과 특화된 증명 LLM(예: Goedel-Prover-V2)을 결und하여 긍정 명제를 증명합니다. 자동화가 실패하면, 증명 LLM이 호출되어 증명을 생성하거나 수정하는 리페어 루프(repair loop)가 작동합니다.

주요 기여

• 답안 구성을 위한 프레임워크: ECP는 형식적 검증 루프 내에서 가용성 제약을 강제하면서 답안 구성과 증명 생성을 명시적으로 분리한 최초의 프레임워크입니다.
• 가용성 강제: 표준 Lean 검사기가 허용할 수 있는 비정형 증거(예: 순환적 정의)를 필터링하는 구조적 방법을 도입하여, 출력이 경시 대회 요구 사항과 일치하도록 보장합니다.
• 신경-기호적 통합: ECP는 Python 도구를 통한 일반 LLM의 탐색적 추론과 특화된 증명 LLM의 엄격한 증명 능력을 효과적으로 결합합니다.
• 자동 형식화 및 벤치마크: 저자들은 2026 MathArena 최종 답안 경시 대회(AIME, HMT, APEX)의 문제 75개와 PutnamBench의 답안 구성 문제 346개를 자동 형식화하여, 이 유형의 새로운 평가 표준을 만들었습니다.

실험 결과
시스템은 직접 증명 생성 기반 모델(GPT-5.4, Goedel-Prover-V2)을 대상으로 MathArena 2026(75문제) 및 PutnamBench(346문제)에서 평가되었습니다.

• 엔드 투 엔드 성능: ECP는 직접 증명 생성 기반 모델보다 우수한 성능을 보였습니다.
  • MathArena: ECP는 18/75 문제(Pass@32)를 해결하여, 가장 우수한 LLM 단독 기반 모델(GPT-5.4, 13/75)보다 높은 성적을 기록했습니다.
  • PutnamBench: ECP는 17/346 문제(Pass@32)를 해결하여, GPT-5.4(8/346) 및 Goedel-Prover-V2-32B(7/346)보다 높은 성적을 기록했습니다.
• 답안 단독 정확도: 도구 지원 답안 구성은 일반 LLM이 올바른 후보를 생성하는 정확도를 크게 향 향상시켰습니다. GPT-5.4의 경우, 도구 사용은 PutnamBench에서의 올바른 답안 구성 능력을 290/346에서 303/346으로 높였습니다.
• 가용성 영향: 분석 결과, 기반 모델들이 생성한 많은 증명은 Lean에서는 컴파일 가능했으나 부적격한 답안(예: 순환적 증거)을 포함하고 있었습니다. ECP의 명시적인 가용성 검사가 이를 필터링하는 데 결정적이었습니다.
• 절제 연구(Ablation Studies):
  • 증명 LLM 수정 단계를 제거하면 MathArena(18 $\to$ 16)와 PutnamBench(17 $\to$ 16)의 성능이 모두 감소했습니다.
  • Lean 자동화를 제거하면 MathArena에서는 심각한 영향(18 $\to$ 11)을 미쳤으나, 특정 실행 환경의 PutnamBench에서는 영향이 적었는데, 이는 MathArena 문제가 자동화 택틱에 더 의존하고 PutnamBench는 증명 능력에 더 의존함을 시사합니다.
  • 더 작은 규모의 증명 모델(8B)을 사용하면 MathArena 성능은 유지되었으나 PutnamBench 결과는 크게 하락(17 $\to$ 7)하여, Putnam 문제가 증명 탐색의 제한을 더 많이 받는다는 것을 보여주었습니다.

의의 및 주장
본 논문은 ECP가 비형식적 답안 생성과 형식적 정리 증명 사이의 간극을 성공적으로 메운다고 주장합니다. 답안 구성을 명시적으로 처리하고 가용성을 강제함으로써, ECP는 직접적인 증명 생성 방식으로는 해결하기 어려운 사례들을 해결합니다. 저자들은 이 접근 방식이 단순히 고정된 결론을 검증하는 것이 아니라, 특정 증거(존재 양화)를 구축해야 하는 문제에 특히 효과적임을 강조합니다.

이 연구는 현재의 형식적 벤치마크들이 "답안이 포함된" 버전의 문제에 집중하느라 답안 구성의 난이도를 간과하고 있음을 지적합니다. ECP는 열거를 위한 일반 LLM의 도구 실행과 특화된 증명 LLM의 검증을 결합하는 것이 복잡하고 개방적인 수학 문제를 형식 시스템에서 해결하는 유망한 경로임을 입증합니다. 저자들은 가용 어휘 레이블링의 휴리스틱한 특성과 매우 복잡한 조합론 문제에서의 열거 단계 내 조합 폭발 가능성이라는 한계점도 언급하였습니다.