在计算不透明时代中的先验知识：人工智能在数学发现中的作用
Apriori Knowledge in an Era of Computational Opacity: The Role of AI in Mathematical Discovery
AI总结：
本文探讨了在计算不透明时代，通过AI获取数学先验知识的挑战与可能方法，强调证明检查器在其中的关键作用。
摘要：
我们能否从计算机程序的输出中获得数学事实的先验知识？人们如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 in similar ways. We claim though that if a proof-checker automating human forms of proof-checking is attached to such machines, then we can obtain apriori mathematical knowledge from them after all, even though the original machines are entirely opaque to us and the proofs they output may not, themselves, be human-surveyable.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
