논리적 사고

자연어 증명에 참고문헌을 붙이면 자동으로 검증된 증명이 될까?

NaturalProver는 배경 정리와 정의를 조건으로 자연어 증명 단계를 생성해 사람 평가를 개선했지만, 형식 검사기가 없는 자연어 증명은 여전히 인간 검토가 필요했습니다.

그림에서 무엇을 볼까요?

참고 정리 검색에서 자연어 증명 생성으로 이어진 뒤 인간 검토와 형식 검증 부재를 구분하는 흐름도

모델이 ‘짝수와 짝수의 합은 짝수’ 정리를 인용해 8+6이 짝수라고 설명했다고 합시다. 정리 이름뿐 아니라 8과 6이 각각 짝수라는 적용 조건과 합 14의 결론을 연결해야 합니다.

반대로 ‘짝수와 홀수의 합은 홀수’ 정리를 언급하면서 두 입력의 홀짝을 확인하지 않으면 참고문헌은 있어도 근거화가 불완전합니다.

2022년 특정 모델·데이터·사람 평가 결과이며 최신 모델이나 모든 수학 분야 성능을 뜻하지 않습니다.

제약 디코딩은 참고항목의 포함을 보장할 수 있어도 그 항목의 정확한 논리적 사용을 형식 검증하지 않습니다.

참고 정리 이름이 정확히 들어가도 증명이 틀릴 수 있는 이유는 무엇인가요?