about
LLMs struggle with math reasoning, because they can't conjecture (arxiv.org)
5 points by trehcrob 353 days ago | hide | past | pdf | 3 comments on HN

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

add comment on HN

LLMs struggle with reasoning --- period, the end.

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.

It's not just that LLMs are probabilistic, it's that the illusion of reasoning in English doesn't transfer to formal systems. I find it quite interesting how far LLM reasoning can be pushed in for example code generation. But there is a massive difference between plausible argumentation and provably correct statements.
it's that the illusion of reasoning in English doesn't transfer to formal systems.

This is because there is very little reasoning --- it's an "illusion".

Data retrieval is not "reasoning". A person with a photographic memory and instant recall is not necessarily a "genius" --- though it may appear that way to some.