증명 보조기의 실패 메시지는 인공지능(AI) 탐색을 어떻게 바꿀까?
DeepSeek-Prover-V1.5는 Lean 4 검증 피드백을 강화학습과 트리 탐색에 이용해 형식증명 성능을 평가했습니다.
그림에서 무엇을 볼까요?
후보 증명, Lean 피드백, 탐색 갱신을 연결해 조건과 범위를 확인하는 교육용 도식.
한 정리에서 실패한 증명 경로와 검증된 중간 상태를 가지처럼 나누고, 보조기 피드백이 어느 가지를 닫는지 표시합니다.
그림은 후보 증명 → Lean 피드백 → 탐색 갱신 순서로 읽고 마지막 합류점에서 조건·범위·반례를 함께 확인합니다. 원 논문의 표나 그림을 복사하지 않고 LTCT가 개념 관계만 새로 그렸습니다.
함께 확인할 점
수치는 2024년 공개 모델·특정 샘플링 예산과 벤치마크 설정에 한정됩니다. Lean이 통과시킨 증명의 형식적 정확성과 자연어 설명의 교육적 품질은 다른 문제이며 데이터 중복 가능성도 계속 점검해야 합니다.
이 연구만으로 LTCT 교육·시험의 효과를 확인할 수 없습니다. 적용안은 별도 비교 조건과 측정 계획이 필요한 제안입니다.
생각해 볼 질문
통과율 63.5%면 한 번 질문할 때 63.5% 확률로 맞는다는 뜻인가요?
사전등록은 적어 두기만 하면 충분할까?
유의확률(p값) 하나가 증거의 판결문이 될 수 있을까?
같은 연구를 다시 하면 결과는 얼마나 돌아올까?