Exploring Mathematical Conjecturing with Large Language Models

• The task of automating the discovery of mathematical conjectures has so far primarily been addressed in symbolic systems. However, a neuro-symbolic architecture seems like an excellent fit for this task. We can assign the generative task to a neural system without much risk, even if a few non-theorems slip through, the results are checked afterwards using a symbolic theorem prover or counter-example finder. In this initial case-study, we investigate the capabilities of GPT-3.5 and GPT-4 on this task. While results are mixed, we see potential in improving on the weaknesses of purely symbolic systems. A neuro-symbolic theory exploration system could, for instance, add some more variation in conjectures over purely symbolic systems while not missing obvious candidates.

Ämnesord

NATURVETENSKAP  -- Data- och informationsvetenskap -- Programvaruteknik (hsv//swe)

NATURAL SCIENCES  -- Computer and Information Sciences -- Software Engineering (hsv//eng)

NATURVETENSKAP  -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)

NATURAL SCIENCES  -- Computer and Information Sciences -- Computer Sciences (hsv//eng)

Nyckelord

Conjecturing

Large Language Models

Theory Exploration

Publikations- och innehållstyp

kon (ämneskategori)

ref (ämneskategori)