쉬운 부등식을 합성한 문제에서 증명 인공지능(AI)가 갑자기 약해질까?
Ineq-Comp v2를 바탕으로 익숙한 부등식의 변수 복제·대수 재작성·다단계 합성이 현재 Lean 증명 모델의 구성적 일반화를 크게 흔드는지 살펴봅니다.
그림에서 무엇을 볼까요?
두 개의 쉬운 부등식 조각이 재작성과 합성 노드를 지나 Lean 목표로 가며 중간 합성 지점에 병목 표시가 있는 흐름도
조각 A가 x+y ≥ 2√xy를 주고 조각 B가 다른 변수쌍에 같은 원리를 준다고 하자. 목표식은 두 결과를 곱하거나 치환해야만 나타날 수 있다.
각 조각의 증명을 프롬프트에 넣어도 목표에 맞는 치환과 순서를 선택하지 못하면 전체 증명은 실패한다. 부품 보유와 계획 성공은 다른 능력이다.
함께 확인할 점
Ineq-Comp는 부등식과 Lean 환경에 집중한 벤치마크로 전체 수학 추론 능력을 대표하지 않는다.
성능은 모델·샘플 예산·프롬프트·라이브러리 버전에 의존하며 pass@32는 단일 시도 정확도가 아니다.
생각해 볼 질문
구성 요소 증명을 모두 제공했는데 실패하면 모델이 그 정리를 전혀 모른다는 뜻일까?
8,192번 중 한 번 성공한 80.7%를 ‘한 번의 실력’으로 읽어도 될까?
수학 인공지능(AI) 시험은 정답만 모으면 충분할까?
수학 자료를 더 읽은 언어모델은 증명도 믿을 수 있을까?