인공지능(AI)가 보조선을 잘 찾으면 기하 증명도 끝난 걸까?

그림에서 무엇을 볼까요?

형식화된 전제에서 신경모형의 보조점 후보, 기호 엔진의 규칙 유도, 검증된 결론으로 이어지는 네 단계 표. 각 단계의 실패 조건을 함께 표시한다.

가상의 문제에서 삼각형 ABC와 각의 이등분 조건이 주어졌다고 합시다. 신경 구성 요소가 변 BC 위에 보조점 D를 제안합니다. 기호 엔진은 D의 위치 조건을 추가한 뒤 합동·닮음·각 관계 규칙으로 목표까지 경로가 이어지는지 검사합니다. 경로가 막히면 제안을 폐기하거나 다른 구성을 탐색합니다.

그림은 ‘형식화된 전제→보조 구성 후보→기호 유도→검증된 결론’의 네 단계를 나눕니다. 첫 단계가 틀리면 뒤의 증명이 형식적으로 완벽해도 원래 문제의 답이 아닙니다. 마지막 단계에서 목표가 실제로 도출되지 않으면 중간 사실이 많아도 성공으로 세지 않습니다.