Formal verification via theorem proving enables rigorous proofs of software correctness, but it is difficult to scale due to the signifi cant manual effort and expertise required. While Large Language Models (LLMs) have shown potential in automating proof generation, they frequently produce incorrect proofs on the first attempt that require iterative refinement to fix. However, most existing approaches employ fixed refinement strategies and cannot dynamically choose an effective strategy, which limits their performance. To overcome this limitation, we introduce Adapt, a novel proof refinement framework that leverages an LLM-guided decision-maker to dynamically select a suitable refinement strategy according to the state of the proof assistant and available context of an incorrect proof. We evaluate Adapt on two benchmark suites against five existing methods and find that it significantly outperforms the best baseline on both by proving 11.26% and 18.58% more theorems, respectively. Furthermore, we demonstrate Adapt’s generalizability by evaluating it across six different LLMs. We also conduct ablation studies to measure the contribution of each component and compare the trade-offs of alternative decision-maker designs.