증명 인공지능(AI)를 비교하려면 같은 문제를 여러 형식체계로 옮겨야 할까?
miniF2F는 올림피아드 수준 문제를 여러 증명 보조기 형식으로 맞춰 신경 정리증명기의 비교 기반을 만들었습니다.
그림에서 무엇을 볼까요?
공통 문제, 체계별 형식화, 검증 성공를 연결해 조건과 범위를 확인하는 교육용 도식.
하나의 수론 문제를 자연어·Lean·Metamath 세 열에 놓고 진술 정렬, 라이브러리, 증명 성공을 각각 분리해 표시합니다.
그림은 공통 문제 → 체계별 형식화 → 검증 성공 순서로 읽고 마지막 합류점에서 조건·범위·반례를 함께 확인합니다. 원 논문의 표나 그림을 복사하지 않고 LTCT가 개념 관계만 새로 그렸습니다.
함께 확인할 점
488개 경쟁수학 문제는 전체 수학 추론을 대표하지 않으며 형식체계별 라이브러리와 완성도도 동일하지 않습니다. 성공률은 허용한 탐색 예산과 샘플 수에 따라 달라져 버전과 평가 설정을 함께 기록해야 합니다.
이 연구만으로 LTCT 교육·시험의 효과를 확인할 수 없습니다. 적용안은 별도 비교 조건과 측정 계획이 필요한 제안입니다.
생각해 볼 질문
한 증명 보조기에서 성공하면 다른 체계에서도 같은 AI가 성공한다고 볼 수 있나요?
사전등록은 적어 두기만 하면 충분할까?
유의확률(p값) 하나가 증거의 판결문이 될 수 있을까?
같은 연구를 다시 하면 결과는 얼마나 돌아올까?