사람의 풀이에는 큰 단계가 있지만 형식증명에는 모든 작은 정당화가 필요합니다. DSP는 자연어 풀이를 빈칸이 있는 형식 스케치로 옮기고 자동 증명기가 빈칸을 채우게 합니다.
연구를 읽는 두 가지 질문
연구 질문과 확인한 자료
Albert Q. Jiang 등 9명의 arXiv v3(2023-02-20) 공개 전문과 ICLR 2023 발표 기록을 확인했습니다. miniF2F의 488개 문제를 검증 244개와 시험 244개로 나누고, Isabelle 형식 문장에 맞춘 비형식 문장·풀이 자료를 정렬했습니다. 성공은 sorry·oops 없이 Isabelle 커널이 전체 증명을 확인할 때만 인정했습니다. [1]
방법과 핵심 결과
Draft 단계는 사람 풀이 또는 언어모델 풀이를 준비하고, Sketch 단계는 큰 추론을 Isabelle 중간 명제로 옮기되 작은 증명을 빈칸으로 남깁니다. Prove 단계는 Sledgehammer와 11개 휴리스틱 전술로 빈칸을 닫습니다. 시험셋 기준 직접 자동화 기준선은 20.9%, 언어모델 풀이 개요 사용은 최대 38.9%, 사람 풀이 개요 사용은 39.3%였습니다. 사람 개요를 써도 60% 넘게 실패했습니다. [1]
구체적 예시와 해석의 범위
‘a에 대해 10a≤28a²+1’을 보일 때 사람은 제곱 완성을 말하지만 형식기는 각 부등식 변환을 확인해야 합니다. 스케치는 중간식 c1…c5를 세우고 자동기가 각 빈칸을 증명합니다. 수치는 이 데이터·Isabelle2021·모델·100회 질의 예산의 성공률이며 오늘의 다른 모델이나 일반 수학 전체 성능이 아닙니다. [1]
학술적 의미와 최근 쟁점
DSP는 사람의 고수준 설명과 기계의 저수준 검증 사이에 ‘스케치’라는 중간 표현을 둡니다. 이 층이 있으면 어느 단계에서 자연어 의미를 잘못 옮겼고 어느 하위목표에서 자동 탐색이 막혔는지 분리해 진단할 수 있습니다. 성공률이 약 두 배가 됐어도 절반 이하라는 사실은 중간 표현의 가치와 현재 한계를 함께 보여 줍니다. 교육에서는 실패한 빈칸도 사고 과정 자료로 보존하는 편이 유익합니다. 독자는 연구의 결론을 받아들이기 전에 원자료가 다룬 대상과 과제, 비교 기준, 측정값을 차례로 확인해야 합니다. 본문 예시는 이 확인 순서를 연습하도록 LTCT가 새로 만든 것이며 원 연구의 자극이나 결과표를 복사하지 않았습니다. 적용 단계에서는 같은 질문을 다른 사례와 반례에 다시 사용해 결론이 조건 변화에 견디는지도 점검합니다. [1]
개념을 직접 점검하는 예시
사람 풀이 ‘양변을 정리해 제곱합으로 만든다’를 중간 명제 두 개로 쪼갭니다. 자동기는 각 변형이 Isabelle 규칙에 맞는지 검사합니다.
한 빈칸이라도 닫히지 않으면 전체 증명은 미완료로 남습니다.
어디까지 말할 수 있을까요?
- miniF2F 488개 고교 경시문제와 Isabelle 설정에 한정되고 자연어 풀이의 품질·모델·질의 예산에 민감합니다.
- 성공률 상승은 정확한 문장 형식화와 이미 강한 자동 증명 도구가 있다는 조건에서 얻었습니다.
원문에 근거한 한계와 LTCT의 적용 범위 검토입니다. [1]
교육 현장과 연결해 보면
AI 풀이 검토는 자연어 개요, 형식화된 중간 명제, 커널 확인 결과를 서로 다른 칸에 저장합니다.
학생은 스케치의 각 화살표가 실제로 어떤 전제와 규칙을 쓰는지 표시하고, 증명기가 해결하지 못한 증명 단계는 ‘확인 필요’로 표시합니다.
좋은 자연어 풀이 개요가 있으면 형식증명은 자동으로 성공하나요?
생각을 비교할 해설 펼치기
아닙니다. 스케치 번역과 하위목표 증명 모두 실패할 수 있으며, 최종 커널 검증이 필요합니다.
원문과 출처 정보
한국어 제목은 이해를 돕기 위한 LTCT 번역입니다. 한글 제목 뒤 괄호에 원제를 함께 표기했습니다. 저자·학술지·원문 버전은 원문 서지정보를 기준으로 확인할 수 있습니다.
초안·스케치·증명: 비형식 풀이로 형식 정리증명기 안내하기 (Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs)
Albert Q. Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, Guillaume Lample (2023). International Conference on Learning Representations (ICLR 2023), Oral.
- 자료 성격
- 국제 AI 학회 논문
- 읽은 버전
- arXiv v3, 2023-02-20 · ICLR 2023 발표본
- 확인 범위
- arXiv v3 공개 전문 전체에서 DSP 세 단계, miniF2F 488개/244개 분할, Isabelle 검증 기준, 20.9·38.9·39.3% 결과와 절제 연구를 확인. 2026-09-13 확인
- 원문 확인일
이 글은 한국어 해설이며 원문 전문 번역이 아닙니다. 도식과 활동의 제작·재구성 범위는 각 그림과 본문에 표시했습니다. 자료 선정과 출처 기준
같은 연구 흐름에서 이어 읽기
같은 원문, 저자·연구 흐름, 공통 개념 태그를 기준으로 연결한 관련 해설입니다.