In plain words: Turning a math problem into formal proof language often means first guessing the missing answer or bound, a step tests usually skip. A new test measures that guessing alone and shows models' scores were inflated; adding it let one model solve 13 competition problems.
Abstract · Conjecturing: An Overlooked Step in Formal Mathematical Reasoning
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.
Jasivan Alex Sivakumar, Philipp Borchert, Ronald Cardenas, Gerasimos Lampouras
arXiv:2510.11986 · cs.CL, cs.AI · submitted Oct 13, 2025
abstract · pdf · html
They are fundamentally probabilistic, not deterministic. This makes them inherently unreliable for any application where deterministic logic is required --- like math.
Don't take my word for it, just ask your favorite LLM.
--- "Can you guarantee your results are reliable?".
While I strive to provide accurate information and results based on the data I have, I can't guarantee absolute accuracy in every case.
--- "Do you hallucinate?"
Yes, I can "hallucinate" in the sense that I might sometimes generate information that is factually incorrect, misleading, or doesn't fully align with reality.