이등변 삼각형 증명
초기 기계 추론 연구의 가장 인상적인 결과 중 하나: 기하학 정리 증명 프로그램이 이등변 삼각형 정리의 증명을 산출했는데, 이것은 설계자들이 예상하지 못했고 대부분의 수학자들도 알지 못했습니다.
고전적인 증명은 보조선을 작도하는 것이 필요합니다: 꼭짓점에서 각의 이등분선을 그리고, 두 개의 작은 삼각형에 SAS 합동을 사용합니다. 증명은 작동하지만 원래 문제에서 언급하지 않는 외부 작도가 필요합니다.
프로그램의 증명은 보조 작도를 사용하지 않았습니다. 삼각형 ABC를 삼각형 CBA와 비교했는데, 이는 동일한 삼각형을 역순으로 읽은 것입니다. 대응 관계 A↔A, B↔C, C↔B는 원래의 삼각형을 밑변의 꼭짓점이 바뀐 상태로 자신과 일치시킵니다. 양변은 가설에 의해 같습니다. SSS 합동에 의해, 삼각형 ABC는 삼각형 CBA와 합동이므로, 각 B는 각 C와 같습니다.
증명은 일부 유클리드 판본의 각주로 나타나지만 널리 알려지지 않았습니다. 시스템을 구축한 프로그래머들은 그것을 알지 못했습니다. 프로그램은 프로그래밍된 전략을 따라 그것을 발견했습니다: 먼저 직접 증명을 시도하고, 막히면 보조선 그리기를 시도합니다.
프로그램이 창의성을 보였는가?
해밍은 직접적인 질문을 던집니다: 이것이 기계 창의성을 구성하는가? 그의 답: 부분적으로 그렇고, & 한정이 중요합니다.
프로그래머들은 정리를 직접 증명하려고 시도하는 지시사항을 작성했고, & 막히면 보조 작도를 시도하라고 했습니다. 프로그램은 이 지시사항을 따랐습니다. 새로운 증명은 직접 증명이 우아하게 작동하는 문제에 이 지시사항을 적용함으로써 나타났습니다.
해밍의 관찰: 그것이 인간의 창의성이 작동하는 방식입니다. 당신의 기하학 교육은 당신에게 프로그램을 로드했습니다. 지시사항은: 직접 증명을 시도하고; 막히면 보조선을 그려라. 당신은 그 지시사항을 기계보다 덜 깔끔하게 배웠습니다 — 당신은 잊고, 잘못 적용하고, & 끝없는 반복이 필요합니다. 하지만 구조는 동일합니다.
해밍이 이름을 붙이는 역설: 무언가를 하는 프로그램이 존재하면, 관찰자들은 자동으로 그 동작을 일상적인 것으로 재분류합니다. 프로그램의 존재는 지능의 인상을 파괴합니다. 기계는 회의적인 청중에게 그 자신이 기계 이상의 것임을 결코 입증할 수 없습니다 — 왜냐하면 어떤 입증도 '단지 프로그래밍일 뿐'으로 재분류되기 때문입니다.
맥스 매튜스 & 컴퓨터 음악
해밍은 기하학에서 음악으로 전환하고, 이 전환은 의도적입니다: 그는 기계 추론이 명백히 분석적인 영역을 넘어 확장된다는 것을 보이고 싶어합니다.
벨 연구소의 맥스 매튜스와 존 피어스는 파형을 디지털로 합성하여 음악을 계산했습니다. 시스템은 샘플링 레이트를 선택해야 했습니다: 나이퀴스트 정리에 따르면, 주파수 f까지의 소리를 재생하려면 최소 2f의 샘플링 레이트가 필요합니다. 인간의 청각은 대략 18,000 Hz까지 확장되고; 전화 품질의 음성은 8,000 Hz를 필요로 하며, 최소 16,000 Hz의 샘플 레이트가 필요합니다.
샘플링 레이트가 고정되면, 시스템은 가능한 모든 파형을 나타내는 진폭의 어떤 수열이든 계산하고, 값들을 디지털-아날로그 변환기 & 스무딩 필터를 통과시키고, & 결과를 재생할 수 있습니다. 순수 음조는 단순 사인파입니다. 악기는 특성 있는 어택과 디케이 엔벨로프를 가진 여러 주파수를 결합합니다. 작곡은 음표 수열과 악기 모델을 지정하는 문제가 되었습니다.
그들은 그 후 물었습니다: 왜 음표를 수동으로 공급하는가? 작곡의 규칙이 존재합니다. 그들은 그 규칙과 난수 생성을 사용하여 컴퓨터가 작곡한 음악을 생산했습니다.
결과: 컴퓨터가 작곡하고 컴퓨터가 연주한 음악은 1970년대 중반까지 이미 라디오 & TV 광고에 나타나고 있었습니다. 1994년의 '최고 품질 녹음'은 디지털이었습니다. 해밍의 관찰: 이제 문제는 어떤 음향이 생산할 가치가 있는가가 아니라 어떤 음향이 기술적으로 가능한가입니다. 기술 경계는 폐쇄되었습니다; 미적 경계는 열려 있습니다.
폐쇄된 기술 경계
해밍은 예리한 주장을 제시합니다: 디지털 오디오로, 음성 재생에 대한 미래의 의미 있는 기술 개선이 있을 수 없습니다. 매체는 이론적 완전성을 달성했습니다. 남은 개선은 미학에서이지, 공학에서가 아닙니다.
그는 컴퓨터 음악 시스템이 작곡가의 역할도 변경했음을 관찰합니다: 실시간 재생은 음악회 공연을 위한 수년의 대기를 대체했습니다. 피드백 사이클이 수 배수 더 짧기 때문에 작곡가는 이제 스타일을 더 빠르게 발전시킬 수 있습니다.
일상적 직업 & 능력 질문
해밍은 대체 문제 앞에서 움츠러들지 않습니다. 컴퓨터는 일상적인 직업에서 노동자를 대체합니다. 그는 이것을 명확하게 말합니다: '로봇은 일상적인 작업을 하는 많은 인간을 대체할 것입니다. 매우 실질적인 의미에서, 기계는 일상적인 작업을 가장 잘 할 수 있고, 따라서 인간을 더 인간적인 직업으로 해방합니다.'
불편한 한정: '불행하게도, 현재 많은 인간은 기계와 경쟁할 준비가 되어 있지 않습니다 — 그들은 일상적인 작업보다 훨씬 더 많은 작업을 할 수 없습니다.'
그는 대부분의 사람들이 일상적인 업무에서 비일상적인 업무로 재교육될 수 있다는 의심을 표현합니다. 이것은 인기 있는 입장이 아닙니다. 그는 적절한 교육이 대체된 노동자들이 경쟁하도록 하게 될 것이라는 광범위한 믿음(희망이라고 그는 말합니다)을 인정합니다. 그는 공개적으로 그것을 의심한 후 계속합니다.
구분 속성
해밍의 틀 내에서 비일상적인 업무와 일상적인 업무를 구분하는 것: 상황을 신중히 분석하고 다음에 무엇을 해야 하는지 세부적으로 명시할 수 있는 능력입니다. 이것은 정확히 프로그램이 하는 일이고 — & 기계가 점점 더 많이 할 수 있는 일입니다. 문제는 인간의 명시가 필요한 상황의 집합이 축소되고 있는지 아니면 증가하고 있는지입니다.
능력 질문
벨 연구소에서의 해밍의 경력은 그에게 직접적인 관찰을 주었습니다: 수십 년에 걸쳐, 컴퓨터에 의해 인간의 관심으로부터 옮겨진 작업은 일관되게 일상적인 것으로 기울었고, & 나타난 새로운 작업은 비일상적인 것으로 기울었습니다. 남은 인간의 가치는 판단, 종합, & 추구할 문제의 선택에 있었습니다 — 실행에서가 아닙니다.
그는 제기하지만 해결하지 않습니다: 이 패턴이 영구적인가, 아니면 자동화가 결국 비일상적인 것도 소비하는가?
인간-기계 협력
해밍의 기계 추론에 대한 선호하는 틀은 경쟁이 아니라 협력입니다. 그는 인간과 기계가 함께 할 수 있지만 어느 것도 혼자서 할 수 없는 것에 관심이 있습니다.
벨 연구소에서 본 예: 긴 기호 조작을 통해 인간 대수학자를 안내하면서 판단 호출을 인간에게 남겨두는 대수 단순화 시스템; 작곡가의 창의적 도달을 확장하면서 미적 선택을 작곡가에게 남겨두는 컴퓨터 음악 시스템; 기계 패턴 인식을 인간의 맥락적 판단과 일치시키는 의료 진단 지원 시스템.
그의 예측: 다가올 수십 년의 가장 가치 있는 작업은 인터페이스에 앉아 있습니다 — 인간이 기계로 대체되지도 않고, & 기계가 인간에 의해 제약을 받지도 않고, 둘 다를 초과하는 조합입니다.
화학 합성 프로그램은 명확한 예입니다: 가능한 합성 경로를 나열했고, 비용과 수율을 계산했으며, & 선택사항을 제시했습니다. 화학자가 선택했습니다. 어느 것도 혼자서는 그렇게 잘 하지 못할 것입니다: 프로그램은 어떤 합성이 우아한지 또는 어떤 부산물이 다운스트림 사용에 중요한지 인식할 수 없습니다; 화학자는 손으로 10,000개의 경로를 나열할 수 없습니다.