Recent advancements in Large Language Models (LLMs) have enabled them to perform exceptionally well on diverse natural language processing and reasoning challenges, with emergent abilities that increasingly mimic human cognition. While LLMs show promise in general mathematical problem-solving, their ability to generate informal, step-by-step proofs for Olympiad-level theorems that are both logically sound and human-verifiable remains underexplored. Existing research has primarily focused on formal theorem proving, which depends on strict symbolic systems and external verifiers, often neglecting the nuanced demands of informal mathematical reasoning. In this paper, we introduce Planning to Prove, a prompt-based framework designed to guide LLMs in producing coherent, step-by-step informal proofs for Olympiad-level inequalities. This approach leverages the inherent capacity of LLMs for multi-step reasoning and planning, enabling the model to first construct a structured outline of the proof before generating the detailed argument. The proposed method is evaluated on a curated set of inequality problems from Mathematical Olympiads and demonstrates that it improves both the correctness and interpretability of the generated proofs. The results highlight the critical role of structured reasoning in informal mathematical domains and suggest promising directions for enhancing LLM performance in advanced mathematical reasoning tasks.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Planning to Prove: Improving Informal Proofs of Olympiad Inequalities from Large Language Models

  • Le Van Thanh,
  • Do Xuan Trong,
  • Pham Duc Tinh,
  • Hai Van Pham

摘要

Recent advancements in Large Language Models (LLMs) have enabled them to perform exceptionally well on diverse natural language processing and reasoning challenges, with emergent abilities that increasingly mimic human cognition. While LLMs show promise in general mathematical problem-solving, their ability to generate informal, step-by-step proofs for Olympiad-level theorems that are both logically sound and human-verifiable remains underexplored. Existing research has primarily focused on formal theorem proving, which depends on strict symbolic systems and external verifiers, often neglecting the nuanced demands of informal mathematical reasoning. In this paper, we introduce Planning to Prove, a prompt-based framework designed to guide LLMs in producing coherent, step-by-step informal proofs for Olympiad-level inequalities. This approach leverages the inherent capacity of LLMs for multi-step reasoning and planning, enabling the model to first construct a structured outline of the proof before generating the detailed argument. The proposed method is evaluated on a curated set of inequality problems from Mathematical Olympiads and demonstrates that it improves both the correctness and interpretability of the generated proofs. The results highlight the critical role of structured reasoning in informal mathematical domains and suggest promising directions for enhancing LLM performance in advanced mathematical reasoning tasks.