논리적 사고

같은 수학문제를 여러 증명 언어로 옮기면 인공지능(AI) 비교가 더 공정해질까?

PutnamBench는 640개 대학 수학문제를 Lean 4·Isabelle과 일부 Coq로 1,692회 형식화해 언어별 자동증명기의 강점과 난도를 비교했습니다.

그림에서 무엇을 볼까요?

하나의 Putnam 원문이 Lean Isabelle Coq 형식화로 갈라지고 각 커널 검사를 거쳐 비교표에 모이는 도식

원문 ‘모든 짝수 n에 대해 n²은 4의 배수다’를 Lean·Isabelle·Coq로 옮긴다고 합시다. 각 언어의 자연수 정의와 나눗셈 보조정리가 달라 같은 수학 아이디어도 다른 코드 경로를 가집니다.

평가표는 원문 의미 보존, 필요한 라이브러리, 생성한 증명, 커널 통과를 네 열로 둡니다. 커널 통과만 있고 원문 번역이 약하면 수학 문제를 제대로 푼 것으로 단정하지 않습니다.

2024년 공개 당시 자동증명기 결과이며 이후 모델·탐색예산 변화로 수치는 달라질 수 있습니다.

다언어 형식화는 비교 범위를 넓히지만 라이브러리와 구문 차이를 완전히 제거하지 않습니다.

형식 증명이 커널을 통과하면 원래 자연어 문제도 반드시 풀었다고 할 수 있나요?