그림이 포함된 정리를 인공지능(AI)가 풀었다면 형식 검증도 통과할까?

그림에서 무엇을 볼까요?

문제 그림과 문장에서 형식 명세를 거쳐 증명 후보와 커널 검사로 이어지는 네 단계 파이프라인.

LTCT 예시입니다. 그림 모서리에 작은 사각형이 있어 ∠A=90°임을 나타냅니다. 모델이 이를 무시하고 일반 삼각형으로 형식화하면 뒤의 증명이 아무리 문법적으로 좋아도 원 문제를 푼 것이 아닙니다.

반대로 형식 명세가 정확해도 커널이 증명 코드를 거절하면 완료가 아닙니다. ‘시각 해석 통과’, ‘명세 보존 통과’, ‘커널 검사 통과’를 따로 기록해야 합니다.