82.5% 성공률 낸 정리 증명 AI h1, 6개 전체에선 68.75%
제목 연관성·주요 수치·시장 영향·향후 전망을 기준으로 핵심 문장을 선별한 요약 브리핑입니다.
핵심 포인트
- h1은 세 시스템이 공통으로 해결한 에르되시 문제 5개에서 AlphaProof Nexus보다 높은 성공률과 낮은 성공 조건부 비용을 기록했다.
- 여섯 번째 문제를 포함한 전체 비교에서는 성공률이 68.75%로 낮아졌다.
- AI 정리 증명 시스템 h1은 공통으로 평가된 에르되시 문제 5개에서 단일 실행 성공률 82.5%와 성공한 증명당 평균 121달러(약 16만원)의 API 환산 비용을 기록했다.
본문
h1은 세 시스템이 공통으로 해결한 에르되시 문제 5개에서 AlphaProof Nexus보다 높은 성공률과 낮은 성공 조건부 비용을 기록했다. 여섯 번째 문제를 포함한 전체 비교에서는 성공률이 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과 다른 정리 증명 시스템의 성능·비용을 비교하고, 여러 벤치마크에서 언어 모델의 증명 능력을 평가했다.
이 5개 문제에서 h1의 단일 실행 성공률은 82.5%로 AlphaProof Nexus의 76%를 웃돌았다. 실패 비용까지 포함한 h1 내부 비교에서는 한 번의 긴 실행으로 성공률 82.5%에 도달할 때 평균 138달러(약 18만원)가 들었다. 같은 성공률을 세 번 실행 방식으로 달성하는 데는 202달러(약 27만원)가 들었으며, 이 수치는 AlphaProof Nexus와의 비용 비교와 산식이 다르다. 여섯 문제 전체를 포함하면 h1의 단일 실행 성공률은 68.75%로 AlphaProof Nexus의 71.67%보다 낮았다. 따라서 다섯 문제에서 나온 성공률과 비용 우위를 전체 정리 증명 과제에 그대로 적용하기는 어렵다. 이번 논문은 수학 정리 증명 실험을 다뤘으며, 블록체인이나 스마트 계약의 검증 성능은 평가하지 않았다.