LLM 기반 형식 증명 보조기(예: Lean)는 수학적 발견 자동화에 큰 가능성을 지니고 있지만, 구문적 정확성을 넘어 인간처럼 수학적 구조를 실제로 이해하는지는 의문이다. 본 논문은 다양한 영역에서 기본 도구인 수학적 부등식을 통해 이 질문을 조사한다. 최신 증명기는 기본적인 부등식을 풀 수 있지만, 본 논문에서는 인간의 직관적인 구성성을 다루는 능력을 조사한다. 변수 복제, 대수적 재작성 및 다단계 구성을 포함한 체계적인 변환을 통해 기본 부등식으로부터 구축된 Ineq-Comp라는 벤치마크를 소개한다. 이러한 문제는 인간에게는 여전히 쉽지만, Goedel, STP 및 Kimina-7B를 포함한 대부분의 증명기는 상당히 어려움을 겪는다. DeepSeek-Prover-V2-7B는 문제를 하위 문제로 분해하도록 훈련되었기 때문에 상대적으로 강건하지만, 여전히 20%의 성능 저하(pass@32)를 보인다. 놀랍게도, 구성 요소의 형식적 증명이 맥락에 제공되는 경우에도 모든 모델의 성능이 저조하게 유지되는데, 이는 약점의 원인이 실제로 구성적 추론에 있음을 보여준다. 본 연구 결과는 현재 AI 증명기의 일반화 동작과 인간의 수학적 직관 사이에 지속적인 격차가 있음을 보여준다.
