Understanding LLM Proofs

William D’Alessandro heldur fyrirlestur á vegum Heimspekistofnunar Háskóla Íslands sem nefnist „Understanding LLM Proofs.“ Fyrirlesturinn verður haldinn í stofu 220 í Aðalbyggingu Háskóla Íslands, miðvikudaginn 28. október kl. 15:00-16.30 og fer fram á ensku. Verið öll velkomin. Um fyrirlesturinn: What does it take to genuinely understand a mathematical proof, as opposed to simply following the proof’s steps and coming to know its conclusion? Plan-reconstruction accounts say that one must be able to generate a rational plan of inferences corresponding to the structure of the proof. Hamami and Morris’s recent version of plan-reconstructionism specifies that, in generating such a plan, one attempts to track the intentions of the proof’s author. I argue that LLM-generated proofs make trouble for accounts of this sort. On the one hand, if LLMs lack proving intentions, then either we can’t understand the proofs they produce, or we’re forced to identify proof understanding with the ability to produce some suitable plan or other. On the other hand, if LLMs possess relevantly intention-like states (as emerging evidence suggests they well may), then understanding LLM proofs requires tracking the states in question. Each of these alternatives has unhappy consequences, leaving plan-reconstruction theorists in an apparently difficult spot.