h1은 단순한 반복 루프만으로 Lean 정리 증명 최고 성능에 도달한다

무엇인가

이 논문은 형식 정리 증명(formal theorem proving)에서 "인간이 설계한 워크플로"가 정말 필요한지를 묻는다. 비형식 수학은 프런티어 모델의 사고 사슬과 에이전트 추론을 키우는 것만으로 발전해 왔지만, Lean 같은 증명 보조기 위에서는 계획 수립, 정리 분해, 전문화된 증명기 오케스트레이션이라는 손으로 짠 구조가 계속 늘어났다. 문제는 새 워크플로의 성능 향상이 더 강한 모델이나 더 많은 연산과 뒤섞여 있어, 순수하게 워크플로 덕분인지 판별이 어렵다는 점이다. 저자들은 검증된 형식 증명이 연구 수학의 속도를 따라가야 한다는 실무적 필요를 배경으로, 단순 루프가 같은 예산에서 이 워크플로들을 따라잡을 수 있는지 계산 비용까지 맞춰 비교한다.

어떻게 동작하나

제안 시스템 h1의 구조는 의도적으로 빈약하다. 모델은 지속되는 작업 파일 하나를 여러 턴에 걸쳐 조금씩 편집하고, 편집할 때마다 Lean 컴파일러가 오류와 남은 목표(open goals)를 즉시 돌려준다. 한 번의 이터레이션은 ReAct 방식의 추론·도구 호출 블록(최대 T턴)으로 시작해, 모델이 파일을 제출하면 외부 검증기(SafeVerify)가 원 명제와 대조해 통과 여부를 판정하는 식으로 끝난다. 검증기가 거부하면 리플렉션 LLM이 그동안의 대화록과 피드백을 "검증된 진전, 실패한 시도의 교훈, 유용한 보조정리 이름"으로 압축하고 포기하지 말 것을 주문하며, 모델은 그 요약을 들고 현재 파일에서 다시 작업을 이어간다. 분해도, 계획도, 탐색 트리도 강제하지 않는다. 대신 Mathlib 검색, 정의 확인, 증명 조각 테스트 같은 선택 도구를 제공하고 언제 쓸지는 모델이 정한다. 저자들은 이 반복이 s1의 "Wait" 기법처럼 테스트타임 연산을 늘리는 장치이며, APN basic과 AxProverBase, 소프트웨어 엔지니어링의 Ralph 루프를 계승한 것이라고 밝힌다.

무엇과 다른가

벤치마크 결과는 GPT-5.6 Sol 기준 FATE-X 90/100, FC100-solved 78/100, FormalQualBench 14/23, IMO 2026 6문제 전부 해결이다. PutnamBench는 GPT-5.5로 672문제 중 670문제를 풀었다. 모두 문제당 한 번의 실행, 반복이나 병렬화 없이 얻은 값이다. 개별 수용된 시도 중에는 리플렉션 1,123회, 활성 95시간, 증명 7,124줄에 이른 사례도 있었다. 값싼 오픈웨이트 모델도 전문화 증명기를 앞선다. DeepSeek V4 Flash를 h1에 넣으면 문제당 14.35달러 상한에서 FATE-X 43문제를 풀어 Leanstral 1.5의 공개 기록 34를 넘고, FC100-solved에서는 0.30달러 미만 상한에서 AlphaProof의 50문제와 동률을 이룬 뒤 4.89달러에서 64문제까지 간다. Gemini 3.1 Pro로는 DM prover agent의 66문제를 문제당 100달러가 아닌 25달러 상한에서 맞추고, 150달러에서 73문제에 도달한다.

어떻게 쓰나

가장 눈에 띄는 부분은 열린 문제다. Formal Conjectures에서 미해결로 분류한 236개 표적에 실행해 여덟 개를 실제로 해결했다. Erdős 138과 337의 변형, OEIS 수열 추측 세 개(A108081, A211417, A022030), AME(9,10) 상태의 존재(Open Quantum Problem 35), Written on the Wall II의 추측 두 개다. 이와 함께 시스템은 형식화 오류를 잡아내는 데도 쓸모가 있었다. 원 명제를 제대로 옮기지 못한 형식 진술을 짧은 반증으로 찾아냈고, 예로 푸앵카레 추측 형식화에 빠진 가설을 지적했다. 저자들은 증명을 찾은 것만큼이나 이런 오류 탐지가 중요하다고 말한다.

전제와 한계

같은 모델·비슷한 비용 조건의 비교에서도 단순 루프가 밀리지 않는다. PutnamBench에서 DeepSeek V4 Flash를 쓴 h1은 Goedel-Architect의 pass@1 점수를 비슷한 비용에 맞춘 뒤, pass@4(비형식 증명 시딩 포함)에서 597대 598로 앞서며 문제당 1.47달러 대 1.08달러를 기록했다. Goedel-Architect의 도구 통합 추론 베이스라인은 200문제 부분집합에서 pass@32로 54.5%인 반면, 같은 모델의 h1은 전체 벤치마크 pass@1에서 89.0%다. Putnam 2025의 최난도 문제 A5는 Numina가 하위 에이전트를 동원한 전용 워크플로와 1,000달러 예산으로 처리한 것인데, h1에서는 GPT-5.2 단독 실행이 81.52달러로 12문제 전부를 풀었다. 단일 시도를 더 길게 늘리는 것이 반복보다 효율적이라는 관찰도 나온다. Gemini 3.1 Pro로 APN이 개별 보고한 열린 Erdős 문제 다섯 개에서 h1의 pass@1은 121달러에 82.5%로, APN basic의 pass@3(191달러에 75.4%)와 전체 APN(317달러에 76%)을 비용까지 포함해 앞선다. 실패 비용까지 평균에 넣어도 pass@1이 138달러에 82.5%, pass@3은 같은 비율에 202달러가 든다. 다만 Erdős 125는 h1 시도 16회가 모두 Lean 타임아웃으로 끝나 전체 APN이 우위를 지킨다.

하네스 설계 자체도 성능을 크게 가른다. 같은 Gemini 3 Flash와 20달러 예산에서 AxProverBase는 Putnam100 18문제를 푸는 데 그쳤고 h1은 69문제를 풀었다. AxProverBase의 컴파일 실패 중 42.2%가 잘못된 라이브러리 임포트에서 멈추는데, h1은 파일이 Mathlib 전체를 임포트하고 있어 이런 실패가 구조적으로 불가능하다. 검색 도구·REPL·언어 서버를 모두 빼면 h1은 Putnam100 49문제, FATE-X 49문제로 떨어지고(전체 도구 사용 시 69, 63), 어떤 단일 도구를 빼도 손실은 최대 4문제다. 즉 특정 도구보다 "조회하고 확인할 수 있는 능력"이 중요하다. 리플렉션은 DeepSeek V4 Flash의 PutnamBench 해결 수를 554에서 598로 올렸다. 리플렉션 사이 턴 수를 1턴으로 두면 Putnam100 50문제·FATE-X 39문제, 10턴이면 72·65문제지만 해결당 비용은 약 두 배가 되고, 200턴으로 늘리면 캐시 재사용률이 0.2%에서 86%로 오르는데도 해결 수는 60·52로 떨어진다. 추론 노력을 높이는 편이 낫다. Gemini 3.1 Pro에서 낮은 노력은 Putnam100 89문제를 문제당 20.63달러에, 높은 노력은 99문제를 5.34달러에 풀었다.

개발자 관점의 메시지는 명확하다. 검증기 피드백이 있는 환경(정리 증명, 소프트웨어 검증, 대형 코드베이스 작업)에서 에이전트를 만들 때, 먼저 값싼 인터페이스와 충분한 테스트타임 예산으로 프런티어 모델을 그냥 돌려 보고 그다음에 워크플로를 설계하라는 것이다. 구체적으로는 작은 단위 편집이 가능한 지속 작업 공간, 편집 직후의 즉시 컴파일 피드백, 필요한 것을 조회·확인하는 도구, 예측 가능한 실패(API 오류, 타임아웃)에 대한 견고한 처리, 캐시 재사용이 가능한 긴 컨텍스트와 품질이 떨어지기 전의 압축이 핵심으로 꼽힌다. 저자들은 또 pass@1이라는 지표가 시스템마다 전혀 다른 연산량을 뜻한다는 점을 지적한다. Goedel-Architect의 한 시도는 계획 수정 16회, AxProverBase의 한 시도는 에이전트 50회 반복을 허용하며, 출력 토큰은 캐시된 입력보다 최대 100배 비쌀 수 있다. 하네스 비교는 모델을 고정하고 비용을 함께 보고해야 한다는 것이 이 논문의 방법론적 요구다.

한계도 분명히 밝힌다. 프런티어 모델이 블랙박스라 학습 중 벤치마크 노출이 격차를 얼마나 좁혔는지는 측정할 수 없다는 점을 인정하면서, 가능한 곳에서는 문제나 해법보다 먼저 출시된 모델(Opus 4.5, GPT-5.2, GPT-5.6 Sol)을 썼다. 단순 루프와 전용 워크플로를 비교한 707개 벤치마크 문제 중 전용 하네스만 푼 예외는 두 개뿐이라고 보고한다. 규모 측면에서는 h1이 단일 파일만 다루므로, 페르마의 마지막 정리나 교과서 전체처럼 컨텍스트 윈도를 넘는 형식화에는 파일 간 의존성 관리, 코드베이스 수준 검증, 중간 결과를 공유하는 병렬 에이전트가 필요하다. 도구도 Lean에 한정되어 수치 계산, 시뮬레이션, 시각화, 웹 검색은 없다. 저자들은 h1의 인터페이스와 도구 역시 인간이 설계한 것이며, 결국 인간 설계와 연산 활용은 대립하지 않는다는 입장을 남긴다.