자동 정리 증명에도 ‘쓴 교훈’이 왔다: 단순 에이전트의 도전

들어가며

대규모 언어 모델은 비형식 수학에서 긴 사고 과정, 에이전트형 추론, 테스트 시점 계산량 확대를 통해 성능을 높여 왔다. 그러나 형식 정리 증명은 훨씬 엄격하다. 모델이 작성한 각 단계가 Lean 4 같은 검증기를 통과해야 하기 때문이다. 이에 따라 최근 시스템은 계획 수립, 문제 분해, 탐색, 특화 증명기 오케스트레이션 등 사람이 설계한 복잡한 워크플로를 모델 주변에 구축해 왔다.

논문 **‘h1: A Taste of the Bitter Lesson in Automated Theorem Proving’**은 이 구조들이 항상 필요한지 묻는다. 모델에 효율적인 Lean 인터페이스를 제공하고, 검증 오류를 읽어 스스로 수정하며 다시 시도하게 하면 단순한 반복 루프도 전문화된 시스템과 경쟁할 수 있을까?

h1의 접근법

h1은 Lean 4를 위한 간결한 하네스다. 정리를 미리 정해진 하위 문제로 나누게 하지 않고, 고정된 탐색 트리나 여러 전문 에이전트의 협업도 요구하지 않는다. 모델은 증명 코드를 제안한 뒤 Lean의 실행 결과와 오류를 확인하고, 이를 바탕으로 수정한 다음 다시 시도한다.

논문이 제시한 주요 결과는 다음과 같다.

• PutnamBench, FATE-X, FormalConjectures100-Solved에서 최고 수준의 성능을 달성했다.
• FormalConjectures에서 기존 미해결 문제 8개를 해결했다.
• 동일한 모델을 사용한 비교에서 Goedel-Architect, AlphaProof Nexus 같은 전문 워크플로와 비슷하거나 더 나은 결과를 보였다.
• 여러 후보 중 하나를 고르는 방식이 아닌 단일 시도(pass@1)만으로도 많은 경우 미해결 문제를 풀 수 있음을 보였다.

마지막 결과는 특히 주목할 만하다. 자동 증명에서는 많은 후보를 생성한 뒤 성공한 결과를 선택하는 접근이 자연스럽게 여겨졌다. 하지만 모델이 형식 검증의 피드백을 효율적으로 활용한다면, 하나의 지속적인 상호작용 안에서 증명을 완성할 수 있다는 의미다.

‘쓴 교훈’의 핵심

여기서 말하는 쓴 교훈은 사람이 정교하게 설계한 구조보다 범용적인 계산량 확대가 더 넓은 범위에서 효과적일 수 있다는 관점을 뜻한다. 다만 증명 시스템을 비교할 때는 더 강한 모델, 더 많은 호출, 더 큰 테스트 시점 예산이 결과에 함께 반영되기 쉽다. h1은 모델과 조건을 맞춘 비교를 통해, 복잡한 오케스트레이션의 일부 이점이 일반적인 에이전트 루프에서도 나타날 수 있음을 보였다.

그렇다고 단순성만으로 충분한 것은 아니다. 소거 실험과 Claude Code, AxProverBase와의 비교는 Lean 인터페이스의 효율성이 비용과 해결률을 크게 결정한다는 점을 보여준다. 검증 과정이 느리거나 피드백이 불명확하면 단순한 루프도 많은 계산 자원을 소모하고 성능을 내기 어렵다.

연구에 주는 의미

이 연구의 실용적인 메시지는 복잡한 모듈을 추가하기 전에 효율적인 실행 피드백을 갖춘 강력한 기준선을 먼저 측정해야 한다는 것이다. 모델 능력과 테스트 시점 계산량도 통제해야 워크플로 자체의 효과를 구분할 수 있다.

h1이 모든 정리에 단일 루프가 최선이라고 증명한 것은 아니다. 문제 분해, 탐색, 특화 증명기의 가치를 부정한 것도 아니다. 대신 추가 구조가 늘리는 비용과 복잡성을 정당화할 만큼 실제 이득을 제공하는지 입증해야 한다는 기준을 제시한다. 프런티어 모델이 더 많은 수학적 추측을 만들어 내는 시대에는, 모델과 형식 검증기 사이의 마찰을 줄이는 인터페이스가 새로운 오케스트레이션 계층만큼 중요할 수 있다.

출처: Hugging Face Daily Papers