Benchmarking Testing in Automated Theorem Proving

"Automated Theorem Proving" 분야에서의 벤치마킹 테스트에 관한 Jongyoon Kim, Hojae Han, Seung-won Hwang 의 논문 "Benchmarking Testing in Automated Theorem Proving"에 대한 상세한 기술 요약입니다.

1. 문제 제기

대규모 언어 모델 (LLM) 의 급속한 발전은 Lean 과 같은 시스템에서 형식적 증명 생성 능력을 향상시켰습니다. 그러나 현재 평가 방법들은 문법적 유효성과 의미론적 정확성을 혼동한다는 치명적인 결함을 안고 있습니다.

• 컴파일의 한계: 기존 벤치마크 (예: MiniF2F, ProofNet) 는 주로 생성된 정리가 컴파일되는지 여부를 확인하여 모델을 평가합니다. 컴파일은 코드가 문법적으로 유효하고 고립된 상태에서 논리적으로 일관된 것을 검증하지만, 해당 정리가 의도된 수학적 의미를 포착했는지는 보장하지 않습니다.
• "동어반복 (Tautology)" 문제: 모델은 성공적으로 컴파일되지만 의도된 비동어반복적 명제 (예: 교환법칙 $a + b = b + a$) 를 증명하지 못하는 단순한 동어반복 (예: $a + b = a + b$) 을 생성할 수 있습니다.
• 대리 지표의 부적절성: 의미론적 정확성을 측정하려는 기존 시도는 인간이 주석한 참조문에 대한 어휘적 중첩 (BLEU 점수) 이나 수동 검사 같은 신뢰할 수 없는 대리 지표에 의존합니다. 이러한 방법들은 노이즈가 많거나, 비싼 인건비가 필요하거나, 올바른 의미와 잘못된 의미를 구분하지 못합니다.

2. 방법론

저자들은 **소프트웨어 공학의 통합 테스트 (integration testing)**에서 영감을 받아 패러다임의 전환을 제안합니다. 정리를 고립된 상태로 평가하는 대신, 코드베이스의 나머지 부분과 어떻게 상호작용하는지에 따라 평가합니다.

핵심 개념: 정리 테스트 (T2)

**커리 - 하워드 대응 (proofs correspond to programs)**을 바탕으로, 저자들은 생성된 정리를 함수로, 그리고 이에 의존하는 정리들을 "테스트 케이스"로 간주합니다.

• 의존성 그래프: 대상 정리 ($t_{GT}$) 가 사용하는 정의/보조정리인 **선행자 (predecessors)**와 이를 호출하거나 기반으로 삼는 정리인 **후행자 (successors)**를 포함하는 의존성 그래프를 구성합니다.
• 통합 테스트 논리: 생성된 정리 ($t_{fl}$) 가 의미론적으로 잘못되었을 경우 (예: 의도된 속성 대신 동어반복을 정의하는 경우), 이를 의존하는 후행 정리들은 컴파일에 실패합니다.
• 컷 제거 (Cut Elimination) 비유: 이 과정은 논리적 원리인 컷 제거에 형식적으로 기반합니다. 중간 보조정리 ($Y$) 를 생성된 후보로 대체했을 때 증명 체인 ($X \to Y \to Z \to W$) 이 실패한다면, 해당 후보는 의미론적으로 잘못되었음을 의미합니다.

T2 벤치마크

저자들은 이러한 평가를 용이하게 하기 위해 대규모 벤치마크인 T2를 구축했습니다.

• 출처: 대수학, 위상수학, 정수론 등을 포괄하는 5 개의 실제 Lean 4 저장소에서 추출되었습니다.
• 규모: 2,206 개의 문제이며, 각 문제는 평균 41 개의 후행 정리와 짝을 이룹니다.
• 하드 (Hard) 하위 집합: 주어진 명제에 대한 증명만 채워 넣는 것이 아니라, 명제 (진술) 와 증명 모두를 생성해야 하는 389 개의 "Hard" 문제 하위 집합입니다.
• 자동화: 추출 파이프라인은 완전히 자동화되어 의존성 구조에 대한 인간 주석이 필요하지 않습니다. 자연어 (NL) 설명은 강력한 LLM (Claude Sonnet 4.5) 에 의해 생성되었으며, 일부 샘플은 수동으로 검증되었습니다.

지표: 테스트 정확도 (Testing Accuracy, TA)

이 논문은 주요 평가 지표로 **테스트 정확도 (TA)**를 도입합니다:
$$TA = E_{P \sim D} \left[ \prod_{i=1}^{k} \text{compiles}(t^{(i)}_{succ} \mid t_{fl}) \right]$$
생성된 정리는 원래 정리를 생성된 것으로 대체했을 때 모든 의존하는 후행 정리가 성공적으로 컴파일될 때만 통과합니다.

3. 주요 기여

1. T2 벤치마크: 고립된 문제를 넘어 실제 저장소 컨텍스트로 이동하는, 의존성이 풍부한 최초의 대규모 형식적 정리 증명 벤치마크입니다.
2. 테스트 정확도 (TA): 의존 모듈의 컴파일을 통해 의미론적 정확성을 직접 검증하는 새로운 자동 참조 무관 지표입니다.
3. 실증적 격차 분석: 오픈소스와 폐쇄소 18 개의 최첨단 모델에 대한 포괄적 평가를 통해 컴파일 성공과 의미론적 정확성 사이의 거대한 단절을 드러냈습니다.
4. 맥락적 통찰: 자연어 증명만 제공하는 것보다 후행 정리를 컨텍스트로 제공하는 것이 의미론적 정확성을 크게 향상시킨다는 것을 입증했습니다.

4. 실험 결과

저자들은 T2 벤치마크에서 GPT-5, Claude-Sonnet-4.5, Llama-3.1 및 DeepSeek-Prover 와 같은 전문 수학 모델을 포함한 18 개의 모델을 평가했습니다.

• 의미론적 격차:

  • 컴파일 정확도: 모델들은 높은 컴파일률을 달성했습니다 (예: Claude-Sonnet-4.5: 전체 세트 기준 80.3%).
  • 테스트 정확도 (TA): 동일한 모델들은 TA 점수가 극적으로 낮았습니다 (예: Claude-Sonnet-4.5: 전체 세트 기준 38.9%; Hard 세트 기준 4.5%).
  • 거짓 양성: 후행자에 대해 테스트했을 때, 컴파일 가능한 정리 중 최대 **93.1%**가 의미론적으로 잘못되었음이 발견되었습니다.

• 기존 지표의 실패:

  • BLEU: 높은 어휘적 유사성 (BLEU 점수) 은 의미론적 정확성과 거의 상관관계가 없었습니다 (상관관계: 0.123). 모델들은 어휘적으로 유사하지만 논리적으로 잘못된 증명을 생성할 수 있었습니다.
  • 전문 모델: 정리 증명을 위해 특별히 파인튜닝된 모델들은 종종 더 높은 컴파일률을 달성했지만, TA 에서는 일반 목적 모델보다 낮거나 비슷한 성능을 보여, 의미론이 아닌 문법에 과적합되었음을 시사합니다.

• 컨텍스트의 영향:

  • 후행 정리를 입력 컨텍스트로 제공하는 것은 TA 를 일관되게 향상시켰습니다 (예: Claude-Sonnet-4.5 의 경우 +4.9%).
  • 후행자 없이 NL 증명만 제공하는 것은 성능을 향상시키지 못했고 때로는 저하시켰습니다.
  • Few-shot 프롬프팅과 **반복적 개선 (컴파일러 피드백 사용)**은 Hard 세트에서 미미한 개선만 가져와, 어려움이 작업 형식화가 아닌 깊은 의미론적 추론에 있음을 나타냈습니다.

5. 중요성 및 결론

이 논문은 Automated Theorem Proving (ATP) 평가의 현재 상태를 근본적으로 도전합니다.

• 성공의 재정의: "컴파일"은 정리 생성에 필수적이지만 불충분한 조건임을 증명합니다. 모델은 문법적으로 완벽할 수 있지만 의미론적으로는 쓸모없을 수 있습니다.
• 신뢰성: T2 벤치마크와 TA 지표는 LLM 이 수학적 개념을 진정으로 이해하는지, 아니면 단순히 문법적으로 유효한 코드를 환각하는지 엄격하고 자동으로 평가할 수 있는 방법을 제공합니다.
• 미래 방향: 이 연구는 향후 ATP 시스템이 고립된 퍼즐을 해결하는 능력보다 기존 코드베이스에 통합되는 능력 (의존성 인식 생성) 으로 평가받아야 함을 시사합니다. 또한 생성 과정에서 모델에게 "테스트 스위트 (후행 정리)"를 제공하는 것이 의미론적 정렬을 개선하는 데 중요한 전략임을 강조합니다.

요약하자면, 이 논문은 통합 테스트가 형식 수학 분야에서 LLM 을 평가하는 데 누락된 연결고리임을 주장하며, 현재 최첨단 모델들이 정리 증명에서 신뢰할 수 있는 의미론적 정확성을 달성하기에는 아직 멀었음을 드러냅니다.