해설에 그럴듯한 정리 이름이 나옵니다. 그 정리를 알고 있다는 사실과 지금 문제에 적용할 수 있다는 사실은 같을까요? 자동 증명에서도 필요한 재료를 찾는 작업, 실제 증명 단계를 만드는 작업, 그 단계가 규칙에 맞는지 검사하는 작업은 서로 다릅니다.
연구를 읽는 두 가지 질문
어떤 연구를 읽었나요?
린도조는 칼텍·엔비디아·MIT 등 소속 연구진이 공개한 정리 증명 환경입니다. 여기서는 NeurIPS 2023 논문의 arXiv v2, 2023-10-27 개정본을 확인했습니다. 전제를 검색하는 리프로버와 린 증명 환경의 상호작용을 소개하며, 본문의 기본 설명은 린 3이고 린 4는 부록에서 별도로 다룹니다. [1]
찾은 전제가 지금 사용 가능한지도 검사합니다
연구는 현재 증명 위치에서 접근 가능한 전제를 찾아 다음 전술 생성에 사용합니다. 또한 훈련 때 사용되지 않은 전제가 필요한 평가 분할을 마련해 단순한 무작위 분할의 한계를 살핍니다. 후보를 생성한 뒤에는 환경에서 오류나 남은 목표를 확인합니다. 검색 결과의 관련성과 증명 완성은 별개의 단계입니다. [1]
‘그리고’를 증명하려면 두 목표가 남습니다
LTCT의 가상 명제 증명입니다. 전제로 ‘표본 라벨이 있다’를 알고 있고, 목표는 ‘표본 라벨이 있고 측정 날짜가 기록되어 있다’입니다. ‘그리고’를 도입하는 규칙을 찾았다고 해도 목표 전체가 해결되지는 않습니다. 라벨이 있다는 하위 목표와 날짜가 있다는 하위 목표를 각각 충족해야 합니다.
첫 하위 목표는 주어진 전제로 해결됩니다. 둘째 하위 목표에는 아직 근거가 없습니다. 날짜가 기록되어 있다는 새 전제를 추가로 받거나, 다른 정당한 규칙과 전제에서 날짜 기록을 이끌어내야 합니다. ‘라벨이 있으니 날짜도 있겠지’는 원래 문제에 없는 조건을 추가하는 것입니다.
그림은 최종 목표를 위에, 필요한 두 하위 목표를 아래에 둡니다. 이 도식의 화살표는 목표가 하위 목표로 나뉘는 방향이며, 사실에서 결론으로 향하는 논증맵의 화살표와 구별해 캡션에 밝혔습니다. 해결된 목표와 미해결 목표도 색과 글자로 함께 표시합니다. 이 예시는 린 코드를 실행한 증명 결과가 아니라 규칙의 요구를 설명하는 자체 제작 도식입니다.
어디까지 말할 수 있을까요?
- 형식 검증은 주어진 정의·공리·전제와 표현된 명제에 관한 검증입니다. 현실의 표본에 실제 라벨이나 날짜가 있는지까지 보장하지 않습니다.
- 자동 증명의 성공률은 검색 범위·시간 예산·자료 분할에 영향을 받습니다. 이 글에서는 시스템을 설치하거나 논문 실험을 재현하지 않았습니다.
원문에 근거한 한계와 LTCT의 적용 범위 검토입니다. [1]
교육 현장과 연결해 보면
수업의 조작형 증명 활동에서는 ‘사용할 규칙 고르기’와 ‘규칙이 요구하는 조건 채우기’를 분리할 수 있습니다. 알맞은 규칙을 골랐지만 근거가 부족한 경우에 부분 수행을 기록하면 오류의 위치가 선명해집니다.
문항은행 검수에서도 비슷한 문항이 학습용과 평가용에 나뉘어 들어가면 낯선 구조를 평가한다고 보기 어려울 수 있습니다. 공통 논리 구조와 필요한 전제를 기준으로 묶어 중복 노출을 점검하는 방안을 제안합니다.
목표 둘 중 하나를 증명하지 못했으면 최종 문장은 거짓인가요?
생각을 비교할 해설 펼치기
그렇게 결론 내릴 수 없습니다. 현재 가진 전제와 수행한 단계만으로 증명이 완성되지 않았다는 뜻입니다. 새 근거로 해결될 수도 있고 실제로 거짓일 수도 있습니다. 증명 실패, 반증 성공, 현실에서의 거짓은 서로 다른 상태입니다.
원문과 출처 정보
한국어 제목은 이해를 돕기 위한 LTCT 번역입니다. 한글 제목 뒤 괄호에 원제를 함께 표기했습니다. 저자·학술지·원문 버전은 원문 서지정보를 기준으로 확인할 수 있습니다.
린도조: 검색으로 보강한 언어모델의 정리 증명 (LeanDojo: Theorem Proving with Retrieval-Augmented Language Models)
Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, Anima Anandkumar (2023). NeurIPS 2023, Datasets and Benchmarks Track · arXiv:2306.15626.
- 자료 성격
- 학회 연구의 저자 공개 원고
- 읽은 버전
- arXiv v2 · 2023-10-27 개정 · 최초 v1 2023-06-27
- 확인 범위
- v2 제3~6절의 증명 환경·전제 검색·분할·평가, 제7절과 부록 F 한계. 프로그램을 설치하거나 연구 수치를 재현한 것은 아님.
- 원문 확인일
이 글은 한국어 해설이며 원문 전문 번역이 아닙니다. 도식과 활동의 제작·재구성 범위는 각 그림과 본문에 표시했습니다. 자료 선정과 출처 기준
같은 연구 흐름에서 이어 읽기
같은 원문, 저자·연구 흐름, 공통 개념 태그를 기준으로 연결한 관련 해설입니다.