82.5% 성공률 낸 정리 증명 AI h1, 6개 전체에선 68.75%

AI 정리 증명 시스템 h1은 공통으로 평가된 에르되시 문제 5개에서 단일 실행 성공률 82.5%와 성공한 증명당 평균 121달러(약 16만원)의 API 환산 비용을 기록했다. 같은 문제 집합에서 AlphaProof Nexus는 성공률 76%, 성공한 증명당 비용 317달러(약 42만원)를 기록했지만, 여섯 번째 문제까지 포함하면 h1의 성공률은 더 낮았다.

메타($META)의 FAIR 연구 조직과 뉴욕대(NYU) 연구진 등이 참여한 연구팀은 10월 25일 논문 ‘h1: A Taste of the Bitter Lesson in Automated Theorem Proving’을 공개했다. 연구진은 h1과 다른 정리 증명 시스템의 성능·비용을 비교하고, 여러 벤치마크에서 언어 모델의 증명 능력을 평가했다.

AlphaProof Nexus와의 비교에는 세 시스템이 모두 한 번 이상 해결한 에르되시 문제 5개가 포함됐다. h1과 AlphaProof Nexus에는 같은 Gemini 3.1 Pro 모델을 적용해 시스템 구성에 따른 차이를 비교했다.

이 5개 문제에서 h1의 단일 실행 성공률은 82.5%로 AlphaProof Nexus의 76%를 웃돌았다. 성공한 증명만 따진 평균 비용은 h1이 121달러, AlphaProof Nexus가 317달러였다.

h1은 언어 모델이 Lean 4 증명 파일을 작성하고 수정하는 방식으로 작동한다. 검증기가 오류와 아직 증명해야 할 목표를 돌려주면 모델이 이를 참고해 다시 시도한다.

Lean 4는 수학 명제와 증명을 정해진 형식으로 표현하고 기계적으로 검사하는 도구다. 따라서 검증 결과는 입력된 형식 명제의 증명이 받아들여졌는지를 보여준다.

연구진은 문제를 미리 여러 단계로 나누거나 전문 증명기를 정해진 순서로 동원하도록 강제하지 않았다. 모델이 작업 파일을 유지하면서 검증 피드백과 자기 점검을 활용해 다음 단계를 정하도록 했다.

다른 벤치마크에서는 GPT-5.5를 연결한 h1이 PutnamBench 672개 문제 중 670개를 해결했다. 다만 PutnamBench 공식 리더보드에는 672개 전체를 해결한 시스템도 올라 있어, 670개를 최고 기록으로 볼 수는 없다.

GPT-5.6 Sol을 적용한 실험에서는 FATE-X 100개 중 90개, FormalConjectures100-Solved 100개 중 78개를 해결했다. 이 벤치마크 결과는 문제마다 한 번씩 실행한 실험에서 나왔다.

논문에 적힌 달러 비용은 기록된 토큰 사용량에 요금표를 적용한 API 환산 비용이다. 실제 지출액을 뜻하지 않으며, 121달러와 317달러는 실패한 과제를 제외하고 성공한 증명만을 기준으로 계산했다.

실패 비용까지 포함한 h1 내부 비교에서는 한 번의 긴 실행으로 성공률 82.5%에 도달할 때 평균 138달러(약 18만원)가 들었다. 같은 성공률을 세 번 실행 방식으로 달성하는 데는 202달러(약 27만원)가 들었으며, 이 수치는 AlphaProof Nexus와의 비용 비교와 산식이 다르다.

비교에서 빠진 에르되시 125에서는 h1의 16차례 시도가 모두 Lean 실행 시간 초과로 끝났다. 이 문제에서는 AlphaProof Nexus가 앞섰다.

여섯 문제 전체를 포함하면 h1의 단일 실행 성공률은 68.75%로 AlphaProof Nexus의 71.67%보다 낮았다. 따라서 다섯 문제에서 나온 성공률과 비용 우위를 전체 정리 증명 과제에 그대로 적용하기는 어렵다.

연구진은 FormalConjectures에서 미해결로 분류된 명제 8개를 증명했다고 보고했다. 논문 부록은 이 가운데 Written on the Wall II의 두 문제는 명제 자체를 수정한 뒤 증명한 사례라고 설명했다.

저장소에 병합된 관련 변경 요청은 이 가운데 다섯 문제를 해결로 표시하고 Lean 증명을 연결했다. 논문이 보고한 8개와 저장소 변경 요청에 표시된 5개는 범위가 다르다.

기계 검증이 증명을 받아들였는지와 입력된 명제가 원래 의도한 수학 문제를 정확히 표현하는지는 구분해야 한다. 논문 부록도 형식화된 명제에 문제가 있을 수 있다고 설명했다.

이번 논문은 수학 정리 증명 실험을 다뤘으며, 블록체인이나 스마트 계약의 검증 성능은 평가하지 않았다.