자동추론

자동추론(Automatic Deduction)은 컴퓨터 프로그램에 의한 수학적 이론의 증명 문제를 다루는 자동화된 추론과 수학 논리(logic)의 하위 분야다. 수학적 증거에 대한 자동화된 추론은 컴퓨터 과학의 발전에 주요한 자극제였다. 인공지능(AI) 연구에 있어 핵심이기도 하다.

자동추론의 논리적 기초

19세기 말과 20세기 초의 논리는 현대 논리와 정형화(formalised)된 수학의 발달이 이었다. 1879년, 고틀로프 프레게(Gottlob Frege)는 자신의 저서 베그리프시크리프트(Begriffsschrift)에서 '완전한 명제로 이뤄진 미적분'과 '근본적인 현대 논리'를 모두 소개했다. 1884년엔 수학을 형식 논리로 표현한 산술 기초(Foundations of Arithmetic)를 출간했다. 이러한 접근은 러셀(Russell Bertrand)과 화이트헤드(Whitehead Alfred North)가 1910~1913년에 처음 출간한 수학 원리(Principia Mathematica)에 큰 영향을 주었다. 그 뒤로도 1927년에 개정된 수학 원리로 접근을 시도했다. 러셀과 화이트헤드는 사회에서 두루 통하는 진리나 도리인 '공리'와 형식논리의 '추론규칙'을 사용해서 수학적인 진리를 도출할 수 있다고 생각했고, 이로 인해 '자동화'란 것에 접근할 수 있게 된다. 1929년, 모히제스 프레스버거(Mojżesz Presburger)는 덧셈과 등호가 있는 자연수 이론(현, 프레스버거 산술(Presburger arithmetic))을 해독할 수 있다는 것을 보여주고, 그 언어에서 주어진 문장이 참인지 거짓인지를 판단할 수 있는 알고리즘을 주었다.

그러나, 이런 좋은 결과가 나온 직후, 1931년에 커트 괴델(Kurt Gödel)은 '프린키니아 매스매티카 및 관련 시스템의 확인되지 않은 문제들에 대하여(On Formally Undecidable Propositions of Principia Mathematica and Related Systems)'를 발표하여, 충분히 자명론 시스템에는 증명할 수 없는 참된 진술들이 있음을 보여주었다. 이 주장은 1930년대에 알론조 처치(Alonzo Church)와 앨런 튜링에 의해 더욱 발전하게 된다.

첫 구현

제2차 세계대전 직후, 최초의 범용 컴퓨터(general purpose computer)가 보급되었다. 1954년, 마틴 데이비스(Martin Davis)는 프린스턴 고등연구소(Princeton Institute)에서 JOHNICA 진공관 컴퓨터를 위한 Presburger의 알고리즘을 프로그래밍(programming) 했다.

관련 문제

더 단순하지만 관련 있는 문제는 정리에 대한 기존 증거가 유효한 증명 검증이다. 이를 위해, 일반적으로 원시적인 재귀 기능이나 프로그램에 의해 각각의 증명 단계를 검증할 수 있어야 하며, 따라서 문제는 항상 해독이 가능하다. 자동화된 정리 증명자에 의해 생성되는 증명들은 전형적으로 매우 크기 때문에, 증명 압축의 문제는 매우 중요하며, 결과적으로 더 쉽게 이해할 수 있고 체크할 수 있게 하는 것을 목표로 하는 다양한 기술들이 개발되었다.

교정 보조원은 시스템에 힌트를 줄 수 있는 인간 사용자를 요구한다. 자동화의 정도에 따라 프로베러는 본질적으로 증명 체커로 축소될 수 있으며, 사용자는 형식적인 방법으로 증명을 제공하거나 중요한 증명 작업을 자동으로 수행할 수 있다. 대화형 프로버들은 다양한 작업에 사용되지만, 심지어 완전히 자동화된 시스템조차도 오랫동안 인간의 수학자들을 따돌린 것, 즉 로빈스 추측을 포함한 많은 흥미롭고 어려운 이론들을 증명했다. 그러나 이러한 성공은 산발적으로 이루어지며, 어려운 문제를 해결하기 위해서는 대개 숙련된 사용자가 필요하다.

산업용

자동화된 정리 증명의 상업적 이용은 대부분 집적회로 설계와 검증에 집중되어 있다. 펜티엄 부동 소수점(FDIV) 버그 이후, 현대 마이크로프로세서의 복잡한 부동 소수점 단위는 추가적인 정밀도로 설계되었다. 어드밴스트 마이크로 디바이시스(AMD), 인텔(Intel) 등은 분할 및 기타 운영이 프로세서에서 올바르게 구현되었는지 검증하기 위해 자동화된 정리를 사용한다.

참고자료

• Automated theorem proving - https://en.wikipedia.org/wiki/Automated_theorem_proving

같이 보기

• 추론
• 인공지능

이 자동추론 문서는 인공지능 기술에 관한 글로서 검토가 필요합니다. 위키 문서는 누구든지 자유롭게 편집할 수 있습니다. [편집]을 눌러 문서 내용을 검토·수정해 주세요.

인공지능 : 인공지능 서비스, 인공지능 로봇, 인공지능 기술 □■⊕, 인공지능 기업, 인공지능 인물 인공지능 기술 AI 워싱 • 랭체인 • 로봇공학 • 로봇기술 • 인지과학 • 자동추론 • 자연어 처리 • 지능 • 지식표현 • 컴퓨터 비전 • 튜링 테스트 • 프롬프트 • 프롬프트 엔지니어링 문자인식과 음성인식 ICR • OCR • OMR • TTS • URL • 글자 • 답변 • 대화 • 동영상 • 디자인 • 맥락 • 문서 • 문자 • 문자인식 • 문자채팅 • 발음 • 번역 • 분류 • 상담 • 소스코드 • 스토리 • 얼굴 • 얼굴인식 • 음성 • 음성채팅 • 음성인식(STT) • 이미지 • 인공어 • 인공지능 음성 • 자막 • 자연어 • 질문 • 채팅 • 코드 • 코딩 • 텍스트 • 통번역 • 통역 • 파일 • 폴더 • 화상채팅 • 화자인식 인공지능 데이터 데이터라벨러 • 데이터라벨링 • 데이터셋 • 돌마 • 벡터 • 벡터DB • 벡터공간 • 스칼라 • 임베딩 • 크라우드워커 • 토큰 • 토큰화 인공지능 학습 ADP • CoLLM • DALL-E • DDPG • DQN • LAM • LMM • SARSA • sLLM • SLM • 강화학습 • 거대언어모델(LLM) • 결정이론적 메타추론 • 계통적 강화학습 • 과적합 • 동적 계획법 • 딥러닝 • 딥큐러닝 • 머신러닝(기계학습) • 메타추론 • 모델 기반 강화학습 • 모델 프리 강화학습 • 미세조정(파인튜닝) • 반영식 아키텍처 • 비지도학습 • 사전학습 • 수시 알고리즘 • 어니 • 에이전트 • 인공지능 학습 • 전이학습 • 준지도학습 • 지도학습 • 추론 • 학습 • 확률적 경사하강법 인공지능 알고리즘 AGI • ANI • ASI • RAG • XAI • 가중치 • 관계형 네트워크(RN) • 뉴런 • 다층퍼셉트론 • 단층퍼셉트론 • 데이터마이닝 • 방사신경망 • 볼츠만 머신 • 분산 샌드박스 • 생성대립신경망(GAN) • 생성형 AI • 수퍼얼라인먼트 • 순전파 • 순환신경망(RNN) • 시그모이드 함수 • 신경망 • 신경망 구조 • 심층신경망(DNN) • 심층신뢰신경망(DBN) • 양방향 비고정값 암호 체계(TSID) • 역전파 • 은닉층 • 인공신경망(ANN) • 인공지능(AI) • 제한 볼츠만 머신(RBM) • 전방전달신경망 • 주의 메커니즘 • 코헨 자기조직 신경망 • 텍스트마이닝 • 트랜스포머 • 파이 • 퍼셉트론 • 합성곱 신경망(CNN) 계산복잡도 NP • NP-완전 • 계산복잡도 • 공간복잡도 • 시간복잡도 • 여 NP • 여 NP-완전 인공지능 프로그램 BCI • GPT • 딥블루 • 딥페이크 • 멀티모달 AI • 모달 • 모달리티 • 모달창 • 알렉스넷 • 어니 • 알파고 • 알파고제로 • 알파폴드 • 왓슨 • 카페 • 컨트롤넷 • 텐서플로 • 텔레파시 • 토치 • 파이토치 • 한돌 인공지능 특징 결정이론 • 계산상의 합리성 • 논리학 • 논리주의자 • 분산성 • 불확실성 • 삼단논법 • 선호도 • 예측곤란성 • 완벽한 합리성 • 유계 합리성 • 이유 불충분의 원리 • 자율성 • 최대기대효용 • 할루시네이션 • 효용이론 인공지능 법적 지위 권리주체성 • 소버린 AI • 전자대리인 • 전자적 인간 • 책임법 위키 : 자동차, 교통, 지역, 지도, 산업, 기업, 단체, 업무, 생활, 쇼핑, 블록체인, 암호화폐, 인공지능, 개발, 인물, 행사, 일반