산술-기하평균 부등식 하나를 아는 모델이 그 부등식을 두 번 조합한 문제도 쉽게 풀까? Zhao와 동료 7명은 Ineq-Comp 벤치마크에서 인간에게 직관적인 기본 부등식을 변수 복제, 대수적 재작성, 여러 단계의 합성으로 바꿔 Lean 증명 모델을 시험했다. 2025년 5월 19일 v1과 2025년 10월 20일 v2를 구분했고, 이번 검수에서는 arXiv v2 공개 HTML·PDF와 공개 코드 링크 범위를 확인했다.
연구를 읽는 두 가지 질문
연구 질문과 벤치마크
연구진은 형식 증명기가 문법적으로 올바른 코드를 생성하는 것을 넘어, 익숙한 수학 구조를 변형된 문제에서도 알아보는지 묻는다. 씨앗 부등식에 변수 복제, 동치 대수식, 다단계 합성 변환을 체계적으로 적용해 Ineq-Comp를 만들었다. 핵심 비교는 원래 문제와 구성적 변형의 성공률 차이다. 문제·평가 코드를 공개해 재현 경로를 제공하지만, 벤치마크가 모든 수학 영역을 대표하는 것은 아니다. [Zhao et al., arXiv:2505.12680v2]
합성에서 드러난 성능 하락
Goedel, STP, Kimina-7B 등 여러 증명기가 구성 문제에서 크게 약해졌다. 상대적으로 견고한 DeepSeek-Prover-V2-7B도 pass@32 기준 20% 성능 하락을 보였다. 671B 규모 모델에서도 씨앗 문제와 구성 변형 사이의 격차가 남았다. 여기서 20%는 논문이 보고한 해당 조건의 하락이며 모든 문제의 절대 정답률이나 한 번 생성의 실패율과 같은 값이 아니다. [Ineq-Comp results]
부품 증명을 줘도 조립이 어려웠다
흥미롭게도 구성 요소의 형식 증명을 문맥에 제공한 조건에서도 모든 모델의 성능이 낮았다. 필요한 부등식 조각을 모르는 것만으로 실패를 설명하기 어렵고, 어떤 조각을 어떤 순서로 재작성해 결론에 맞출지 계획하는 구성 추론이 병목일 수 있다. 다만 프롬프트 길이, 탐색 예산, Lean 라이브러리와 모델 훈련자료도 결과에 영향을 준다. ‘인간은 이해하고 AI는 이해하지 못한다’는 철학적 결론을 직접 측정한 것은 아니다. [Constituent-proof condition]
pass@k를 읽는 법
pass@32는 한 문제에 여러 후보를 뽑았을 때 적어도 하나가 검증기를 통과할 확률을 추정하는 지표다. 한 번의 생성 정확도인 pass@1과 같지 않다. 더 많은 후보와 계산을 허용하면 수치가 오를 수 있으므로 모델 비교에는 샘플 수, 시간·토큰 예산, 검증 규칙을 함께 기록해야 한다. Lean 검증 통과는 형식적 정당성을 강하게 보장하지만, 벤치마크 변환이 교육적으로 자연스러운지나 새로운 수학적 통찰을 보장하지는 않는다. [Evaluation details]
LTCT 적용: 원리 기억과 구성 계획을 분리하기
이 AI 벤치마크는 LTCT 시험이나 학생 교육 효과를 검증하지 않았다. 적용 아이디어로 기본 부등식 한 단계 문항과 같은 조각을 두 단계로 합성한 문항을 짝지어, ‘원리 인출’과 ‘계획·재작성’을 별도 점수로 볼 수 있다. AI 보조 해설도 최종 Lean 통과 여부, 사용한 씨앗 정리, 후보 수를 기록한다. 학생 평가에 모델의 pass@32를 그대로 인간 성취 지표로 옮기지 않는다. [LTCT 적용 제안]
두 조각을 아는 것과 이어 붙이기
조각 A가 x+y ≥ 2√xy를 주고 조각 B가 다른 변수쌍에 같은 원리를 준다고 하자. 목표식은 두 결과를 곱하거나 치환해야만 나타날 수 있다.
각 조각의 증명을 프롬프트에 넣어도 목표에 맞는 치환과 순서를 선택하지 못하면 전체 증명은 실패한다. 부품 보유와 계획 성공은 다른 능력이다.
어디까지 말할 수 있을까요?
- Ineq-Comp는 부등식과 Lean 환경에 집중한 벤치마크로 전체 수학 추론 능력을 대표하지 않는다.
- 성능은 모델·샘플 예산·프롬프트·라이브러리 버전에 의존하며 pass@32는 단일 시도 정확도가 아니다.
원문에 근거한 한계와 LTCT의 적용 범위 검토입니다. [1]
교육 현장과 연결해 보면
수학·정보 수업에서는 씨앗 문제와 대수 재작성·변수 복제·다단계 합성 변형을 짝지어 전이 실패 지점을 기록합니다.
AI 결과에는 공개본 버전, 모델 크기, pass@k의 k, 후보 수와 Lean 검증 여부를 함께 표시합니다.
구성 요소 증명을 모두 제공했는데 실패하면 모델이 그 정리를 전혀 모른다는 뜻일까?
생각을 비교할 해설 펼치기
그렇게 단정할 수 없다. 조각을 목표식에 맞게 선택·변형·순서화하는 구성 계획이 실패했을 수 있다. 지식과 조립 능력을 나눠 진단해야 한다.
원문과 출처 정보
한국어 제목은 이해를 돕기 위한 LTCT 번역입니다. 한글 제목 뒤 괄호에 원제를 함께 표기했습니다. 저자·학술지·원문 버전은 원문 서지정보를 기준으로 확인할 수 있습니다.
부등식 구성 추론 벤치마크: 부등식 자동정리증명의 인간 직관적 구성 추론 벤치마크 (Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving on Inequalities)
Haoyu Zhao; Yihan Geng; Shange Tang; Yong Lin; Bohan Lyu; Hongzhou Lin; Chi Jin; Sanjeev Arora (2025). arXiv; NeurIPS 2025 Datasets and Benchmarks track.
- 자료 성격
- 공개 학회 논문
- 읽은 버전
- arXiv v2, 2025-10-20 (v1: 2025-05-19)
- 확인 범위
- arXiv v2 공개 HTML·PDF에서 변환 유형, 모델 비교, pass@32의 20% 하락, 구성요소 증명 제공 조건과 공개 코드 범위를 확인
- 원문 확인일
이 글은 한국어 해설이며 원문 전문 번역이 아닙니다. 도식과 활동의 제작·재구성 범위는 각 그림과 본문에 표시했습니다. 자료 선정과 출처 기준
같은 연구 흐름에서 이어 읽기
같은 원문, 저자·연구 흐름, 공통 개념 태그를 기준으로 연결한 관련 해설입니다.