본문으로 건너뛰기
J
피드

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

general 약 3분
tags
#math#sage#quantifier-elimination#competition-math#model-theory
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)에서 이런 문제 보면 "컴퓨터가 해줄 수 있는데"라고 댓글 달고 싶은 충동을 참고 있다가 블로그에 풀었다고 함

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

prev

이전 기사 (P)

next

다음 기사 (N)

댓글

댓글

댓글을 불러오는 중...

관련 기사

general

폐쇄된 클라이밋닷거브, 공공 데이터 덕분에 클라이밋닷어스로 되살아나다

미국 정부의 기후 정보 사이트 Climate.gov가 예산 삭감으로 내려간 뒤, 전직 NOAA 관련자들이 Climate.us로 핵심 자료를 복원했어. 15년 넘게 쌓인 기후 지도, 교육 자료, 기후 지표 보고서, 삭제된 제5차 국가기후평가까지 되살린 배경에는 미국 정부 데이터가 법적으로 퍼블릭 도메인이라는 점이 있었어. 다만 운영은 기부에 의존하고 있어, 공공 인프라를 민간이 임시로 떠받치는 불안정한 구조도 같이 드러나.

general

AI 시대에도 인간 관리자가 남는 이유는 결국 ‘책임’ 때문임

생성형 AI가 기업 경영의 많은 판단을 도와도, 인간 관리자의 역할이 사라지지는 않는다는 주장이다. 글은 공감, 검증, 실행, 책임이라는 네 가지 영역에서 AI가 아직 인간 관리자를 대체하기 어렵다고 설명한다.

general

서로 1만 달러 주고받으면 매출 1만 달러? 스타트업 매출 놀이를 비꼰 풍자 사이트

LARP는 창업자끼리 같은 금액을 서로 주고받은 것처럼 장부에 기록해 매출을 만든다는 설정의 풍자 사이트다. 실제 제품, 고객, 현금 이동 없이도 연간 반복 매출(ARR)을 부풀릴 수 있다는 식으로, 스타트업의 매출 인정과 상호 거래 관행을 날카롭게 비꼰다.

general

뱅크오브아메리카, 소버린 클라우드 수요 보고 아이오노스에 매수 의견

뱅크오브아메리카가 유럽 웹 호스팅·도메인 기업 아이오노스에 매수 의견과 목표주가 37유로를 제시했다. 핵심 논리는 중소기업 대상 웹 서비스, AI 업셀링, 소버린 클라우드 수요가 맞물리며 2025년부터 2028년까지 매출과 이익이 성장할 수 있다는 것이다.

general

SDT·KT·스패로우까지, 국내 보안·클라우드·양자 업계 단신 모음

SDT는 양자 클라우드 플랫폼 큐레카에 양자내성암호를 적용하고 CUDA-Q 교육 모듈을 3개 국어로 제공하기로 했다. KT, 스패로우, 매스웍스, 아이씨티케이, 오케스트로 클라우드도 각각 메일보안, 앱 보안, 디지털 트윈, 양자보안, 공공 클라우드 전환 관련 소식을 냈다.