Definition modeling is used as a probe of what a language model has internalized about a domain, and it has been studied on general lexicography and on jargon-heavy specialist domains. We extend this task to mathematics, where a term can be defined very differently for different communities. In this context we study the baseline capacity of models to retrieve generate definitions, and their audience-bias when explaining mathematical terms without specific guidance. We further asses to what extent can they follow a certain style when directed, and to which degree being exposed to definitions aid or hurt model performance when solving mathematical questions.

As we continue to extend their range of applications, the study of the generalization capabilities of large language models (LLM) has become an important topic. Previous works have recently proposed to study these abilities in the context of mathematical reasoning. This was done by asking models to reproduce proofs that they have most likely seen during training, but when key symbols are replaced. Since this evaluation relies heavily on human feedback, we study to what degree this evaluation can be automatically performed. To that end, we simulate the human evaluation proposed by previous work by interactively presenting the same questions to the LLMs as prompts. We analyze the degree of alignment between human and model answers via an accuracy and correlation analysis, as well as via inter-annotator agreement metrics. We test a selection of models, including ones with reasoning capabilities, and show LLMs currently have important limitations in this regard, which cannot be addressed by ICL.

We study the generalization capabilities of large language models (LLM) through the lens of mathematical reasoning, asking if these models can recognize that two structures are the same even when they do not share the same nomenclature. We propose a human study to evaluate if LLMs reproduce proofs that they have most likely seen during training, but when the symbols do not match the ones seen. To test this in a controlled scenario, we look at proofs in propositional calculus, foundational for other logic systems, semantically complete and widely discussed online. We replace the implication operator (→) with an unrelated, arbitrary symbol (♠) and ask experts to evaluate how the output of a selection of LLMs changes in terms of compliance, correctness, extensiveness and coherence. Our results show that nearly all our tested models produce lower quality proofs in this test, in particular open-weights models, suggesting the abilities of these LLMs to reason in this context have important limitations.