인공지능(AI)가 쓸 만한 정리를 찾으면 증명도 끝난 걸까?

그림에서 무엇을 볼까요?

최종 목표 '라벨이 있고 날짜가 있다'가 '라벨이 있다: 전제로 해결'과 '날짜가 있다: 근거 필요'라는 두 하위 목표로 분기한다.

LTCT의 가상 명제 증명입니다. 전제로 ‘표본 라벨이 있다’를 알고 있고, 목표는 ‘표본 라벨이 있고 측정 날짜가 기록되어 있다’입니다. ‘그리고’를 도입하는 규칙을 찾았다고 해도 목표 전체가 해결되지는 않습니다. 라벨이 있다는 하위 목표와 날짜가 있다는 하위 목표를 각각 충족해야 합니다.

첫 하위 목표는 주어진 전제로 해결됩니다. 둘째 하위 목표에는 아직 근거가 없습니다. 날짜가 기록되어 있다는 새 전제를 추가로 받거나, 다른 정당한 규칙과 전제에서 날짜 기록을 이끌어내야 합니다. ‘라벨이 있으니 날짜도 있겠지’는 원래 문제에 없는 조건을 추가하는 것입니다.