Alapfogalmak
계산 불투명성 시대에도 인공지능을 활용하여 선험적 수학적 지식을 얻을 수 있다. 이를 위해서는 인간의 증명 검사 능력을 기계화한 투명한 증명 검사기를 활용해야 한다.
Kivonat
이 논문은 계산 불투명성 시대에 인공지능이 수학적 지식 생성에 어떤 역할을 할 수 있는지 탐구한다.
1977년 Appel과 Haken의 컴퓨터 증명을 통해 수학에서 컴퓨터의 역할이 논의되기 시작했다. Burge는 이 증명이 선험적 수학적 지식을 제공한다고 주장했는데, 이는 컴퓨터가 수행한 계산이 인간의 수학적 추론 능력을 기계화한 것이기 때문이다.
그러나 딥러닝 모델(DNN)과 대규모 언어 모델(LLM)은 내부 작동 원리가 불투명하기 때문에, 이들의 출력으로부터 직접 수학적 지식을 얻을 수 없다. 이들의 출력은 단지 귀납적으로 정당화된 신념을 제공할 뿐이다.
그럼에도 불구하고, 만약 DNN이나 LLM이 인간이 검사할 수 있는 증명을 출력한다면, 이를 검사함으로써 선험적 수학적 지식을 얻을 수 있다. 즉, 투명한 증명 검사기를 활용하면 불투명한 인공지능 시스템으로부터 간접적으로 수학적 지식을 얻을 수 있다.
이를 통해 인공지능이 순수 수학에서 진정한 수학적 지식 생성에 중요하고 변혁적인 역할을 할 수 있음을 시사한다.
Statisztikák
1977년 Appel과 Haken은 컴퓨터를 이용하여 4색 정리를 증명했다.
딥러닝 모델(DNN)과 대규모 언어 모델(LLM)은 내부 작동 원리가 불투명하다.
[RPBN+23]에서 LLM을 활용하여 Cap Set 문제에 대한 새로운 결과를 얻었다.
Idézetek
"Appel and Haken did indeed attain apriori knowledge of the truth of the Four Color Theorem from the output of their computer program."
"We can acquire genuine mathematical knowledge of a fact whose proof was generated by a process that is not mathematically intelligible to us, and is so complex that it is not human-checkable in any way."