Conjecturing: An Overlooked Step in Formal Mathematical Reasoning

TL;DR

This paper reframes autoformalisation as two intertwined tasks by treating conjecturing as a separate prerequisite in formal mathematical reasoning. It introduces ConjectureBench, a dataset and evaluation framework with ConJudge and equiv_rfl metrics to separately assess conjecturing, and Lean-FIRe, an inference-time method that interleaves informal Chain-of-Thought with Lean-of-Thought reasoning. Empirical results show that withholding conjectures substantially degrades autoformalisation performance, even for strong models like GPT-4.1, while Lean-FIRe yields meaningful gains and achieves first end-to-end autoformalisation on PutnamBench 'no-answer' problems for some models, underscoring that latent mathematical knowledge exists but requires targeted guidance to conjecture and formalise effectively. The work suggests a clear research agenda: develop richer conjecturing data, design inference-time strategies, and train models to separate and reintegrate conjecturing within the autoformalisation pipeline.

Abstract

Autoformalisation, the task of expressing informal mathematical statements in formal language, is often viewed as a direct translation process. This, however, disregards a critical preceding step: conjecturing. Many mathematical problems cannot be formalised directly without first conjecturing a conclusion such as an explicit answer, or a specific bound. Since Large Language Models (LLMs) already struggle with autoformalisation, and the evaluation of their conjecturing ability is limited and often entangled within autoformalisation or proof, it is particularly challenging to understand its effect. To address this gap, we augment existing datasets to create ConjectureBench, and redesign the evaluation framework and metric specifically to measure the conjecturing capabilities of LLMs both as a distinct task and within the autoformalisation pipeline. Our evaluation of foundational models, including GPT-4.1 and DeepSeek-V3.1, reveals that their autoformalisation performance is substantially overestimated when the conjecture is accounted for during evaluation. However, the conjecture should not be assumed to be provided. We design an inference-time method, Lean-FIRe to improve conjecturing and autoformalisation, which, to the best of our knowledge, achieves the first successful end-to-end autoformalisation of 13 PutnamBench problems with GPT-4.1 and 7 with DeepSeek-V3.1. We demonstrate that while LLMs possess the requisite knowledge to generate accurate conjectures, improving autoformalisation performance requires treating conjecturing as an independent task, and investigating further how to correctly integrate it within autoformalisation. Finally, we provide forward-looking guidance to steer future research toward improving conjecturing, an overlooked step of formal mathematical reasoning.

Figures (13)

• Figure 1: End-to-end evaluation pipeline for conjecturing and autoformalisation, including a "seen" setting (conjecture provided) and a more realistic "unseen" setting (conjecture must be inferred). Our contributions, highlighted in blue, introduce ConjectureBench, "unseen" evaluation, and two corresponding metrics: ConJudge for assessing conjecturing during autoformalisation and equiv_rfl for standalone conjecture generation.
• Figure 2: Illustration of Lean-FIRe construction within the overall pipeline for generating autoformalisations and conjectures, where the conjecture in the green box is provided only in the "seen" setting, and CoT and LoT stand for chain/lean-of-thought.
• Figure 3: Example (1/5) from Putnam annotated with informal and formal hint reasoning steps.
• Figure 4: Example (2/5) from Putnam annotated with informal and formal hint reasoning steps.
• Figure 5: Example (3/5) from Putnam annotated with informal and formal hint reasoning steps.