쉬운 부등식을 합성한 문제에서 증명 인공지능(AI)가 갑자기 약해질까?
Ineq-Comp v2를 바탕으로 익숙한 부등식의 변수 복제·대수 재작성·다단계 합성이 현재 Lean 증명 모델의 구성적 일반화를 크게 흔드는지 살펴봅니다.
Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving on Inequalities
게시 2026-09-13 · 약 10분해외 논리학 연구 해설 읽기 →



