본문으로 건너뛰기
피드

수학 경시대회 부등식 문제를 양화사 소거로 컴퓨터에게 풀게 하기

general 약 3분
vote
0
댓글
북마크

모델 이론의 양화사 소거(Quantifier Elimination)와 SageMath+QEPCAD를 이용해 경시대회 수준의 다항식 부등식 문제를 자동으로 증명하는 방법을 소개.

  • 1

    실수 체에서 양화사가 포함된 논리식을 동치인 양화사 없는 수식으로 변환 가능

  • 2

    SageMath + QEPCAD로 몇 줄의 코드만으로 복잡한 부등식 증명

  • 3

    등호 조건까지 자동으로 확인 가능

  • 4

    입력은 다항식 형태여야 하므로 루트·분수는 사전 변환 필요

  • 수학 경시대회에 나오는 인위적인 부등식 문제들을 양화사 소거(Quantifier Elimination, QE)라는 모델 이론의 정리로 컴퓨터한테 자동으로 풀게 할 수 있다는 이야기

  • 핵심 아이디어: 실수 체(real closed field)에서 양화사가 포함된 논리식(∀x, ∃x)을 양화사 없는 동치 수식으로 변환할 수 있음. 예를 들어 "∃x. ax² + bx + c = 0"은 "b² - 4ac ≥ 0"과 동치인데, 이걸 일반화해서 아무리 복잡한 다변수 부등식도 기계적으로 처리 가능

  • 도구는 SageMath + QEPCAD. sage -i qepcad으로 설치하고, 양화사가 포함된 수식을 넣으면 양화사 없는 동치식을 뱉어줌. 코드가 놀라울 정도로 짧음

  • 예제 1: a⁴ + b⁴ = 17일 때 15(a+b) ≥ 17 + 14√(2ab) 증명 — √를 제곱으로 치환해서 다항식으로 만든 뒤 sage에 던지면 끝. 등호 조건이 (1,2)와 (2,1)뿐이라는 것까지 자동으로 확인 가능

  • 예제 2: (x + 1/x)(y + 1/y)(z + 1/z) ≥ (x + 1/y)(y + 1/z)(z + 1/x) 증명 — xyz를 양변에 곱해서 다항식으로 만들고 sage에 넣으면 참임이 확인되고, 등호 조건의 기하학적 구조까지 알려줌

  • 제한사항은 입력이 다항식 부등식이어야 한다는 것. √나 분수가 있으면 먼저 양변을 곱하거나 제곱해서 다항식 형태로 바꿔야 함

  • 글쓴이 왈, MSE(Math StackExchange)에서 이런 문제 보면 "컴퓨터가 해줄 수 있는데"라고 댓글 달고 싶은 충동을 참고 있다가 블로그에 풀었다고 함

수학의 '핵무기'를 경시대회 문제에 쓰는 유쾌한 오버킬. 연구자라면 이런 도구를 알아두면 시간 절약이 될 것

댓글

댓글

댓글을 불러오는 중...

general

Last.fm, 소유권 바뀌고 독립 회사로 새 출발

Last.fm이 소유권 변경을 거쳐 독립 회사로 운영된다고 밝혔다. 계정, 청취 기록, 스크로블, Pro 구독, API 기능은 그대로 유지되며 사용자 데이터 처리 방식도 바뀌지 않는다고 안내했다.

general

구글이 “사람들은 AI 모드를 좋아한다”고 하자 덕덕고 방문이 28% 가까이 늘어남

구글 검색이 AI 모드와 AI 개요를 전면에 밀어붙이는 사이, AI 없는 검색을 내세운 덕덕고 쪽 트래픽이 눈에 띄게 뛰었다. 덕덕고는 “사람들이 원하는 건 AI 자체의 찬반이 아니라 선택권”이라고 보고 있다.

general

경기도, 도민 15만 명 대상 AI·디지털 교육 시작

경기도가 2026년 AI디지털배움터를 열고 약 15만 명을 대상으로 스마트폰, 키오스크, 생성형 AI, 업무 자동화 교육을 운영해. 고령층과 정보취약지역 주민을 위한 찾아가는 교육, 청년·소상공인 대상 AI 활용 교육까지 범위를 넓힌 게 특징이야.

general

NIA “공공 AX 표준 만들고, 정책부터 현장 구현까지 직접 잇겠다”

한국지능정보사회진흥원(NIA)이 AI 기본법에 따른 인공지능정책센터로 지정되며 공공 부문의 AI 전환을 지원하겠다는 방향을 밝혔다. 핵심은 부처·지자체가 각자 따로 AI를 도입하다 생기는 중복 투자와 표준 부재를 줄이고, 일부 유스케이스는 정책 설계에서 구현까지 직접 밀어붙이겠다는 것.

general

최악의 면접은 코딩 테스트가 아니라 ‘무단 심리평가’였다

한 엔지니어가 정신건강 스타트업의 창업 엔지니어 면접에서 겪은 일을 공유했다. 기술 평가도 하기 전에 90분짜리 컬처핏 인터뷰에서 인생의 가장 힘든 날, 가족 문제, 실패한 관계 같은 사적인 이야기를 끌어냈고, 다음 날 한 줄짜리 탈락 메일을 받았다는 내용이다.