Apriori Knowledge in an Era of Computational Opacity: The Role of AI in Mathematical Discovery
Eamon Duede and Kevin Davey
我们可以从计算机程序的输出中获取数学事实的知识吗? 像Burge这样的人(在我们看来是正确的)认为,例如,Appel和Haken从他们的计算机程序中获得了四色定理的先验知识,因为他们的程序只是自动化了人类的数学推理形式。 然而,与此类程序不同,我们认为现代LLM和DNN的不透明性在以类似的方式从中获取先验数学知识方面造成了障碍。 我们声称,如果一个自动将人类形式的证明检查程序附加到这些机器上,那么我们毕竟可以从它们中获得先验数学知识,即使原始机器对我们来说是完全不透明的,并且它们输出的证明本身可能不是人类可调查的。
Can we acquire apriori knowledge of mathematical facts from the outputs of computer programs? People like Burge have argued (correctly in our opinion) that, for example, Appel and Haken acquired apriori knowledge of the Four Color Theorem from their computer program insofar as their program simply automated human forms of mathematical reasoning. However, unlike such programs, we argue that the opacity of modern LLMs and DNNs creates obstacles in obtaining apriori mathematical knowledge from them...