Planning to Hammer: Difficulty-Aware Decomposition for Automating Rocq Proofs

• URL: http://arxiv.org/abs/2606.17981v1
• Date: Tue, 16 Jun 2026 14:33:15 GMT
• Title: Planning to Hammer: Difficulty-Aware Decomposition for Automating Rocq Proofs
• Abstract summary: We present Quarry, a planning-based proof synthesis framework that separates proof planning from proof execution.<n>Specifically, Quarry asks an LLM to actively propose multiple proof decompositions with arbitrary sublemmas, type-checks them in Rocq under temporarily admitted sublemmas, and ranks candidates using a proof-state-based difficulty model.<n>Experiments show that planning-based decomposition with solvability-aware ranking substantially improves automation while maintaining predictable cost.
• Score: 21.65389718022749
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: As AI-generated code proliferates, formal verification, particularly through interactive theorem provers such as Rocq and Isabelle, becomes increasingly important for ensuring software correctness. However, producing machine-checked proofs in such provers remains a bottleneck. Existing solutions bring complementary strengths to proof automation: large language models (LLMs) can propose high-level proof strategies but lack local rigor, while automated tactics such as CoqHammer can reliably discharge many local goals but lack long-range planning capabilities. To combine the best of both worlds, we present Quarry, a planning-based proof synthesis framework that separates proof planning from proof execution. Specifically, Quarry asks an LLM to actively propose multiple proof decompositions with arbitrary sublemmas, type-checks them in Rocq under temporarily admitted sublemmas, and ranks candidates using a proof-state-based difficulty model that estimates hammer solvability. It then recursively proves sublemmas within a bounded budget, effectively turning long proofs into sequences of hammer-solvable obligations. We implement Quarry on top of SerAPI and CoqHammer and evaluate it using multiple frontier LLMs across multiple benchmarks. The experimental results show that planning-based decomposition with solvability-aware ranking substantially improves automation while maintaining predictable cost. Under a uniform 10-minute wall-clock budget, Quarry improves over the strongest baseline by 7% to 13% in success rate across three Rocq benchmarks. These results demonstrate that reliable proof automation can be achieved by coordinating neural planning with symbolic execution rather than replacing either.

Related papers

• PROMISE: Proof Automation as Structural Imitation of Human Reasoning [15.113069562646302]
  We present PROMISE, a structure-aware framework that reframes proof generation as a stateful search over proof-state transitions.<n>We evaluate PROMISE on the seL4 benchmark across multiple LLM backends and compare it with prior systems such as Selene and Rango.
  arXiv  Detail & Related papers  (2026-04-07T03:49:12Z)
• Stress-Testing the Reasoning Competence of LLMs With Proofs Under Minimal Formalism [2.215655942741476]
  We introduce ProofGrid, a benchmark suite for evaluating reasoning through machine-checkable proofs.<n>ProofGrid contains 15 tasks spanning proof writing, proof checking, proof masking, and proof gap-filling.<n> Tasks are expressed in minimal formal notation, especially NDL, a compact natural-deduction language that fits in short prompts.
  arXiv  Detail & Related papers  (2026-04-07T01:19:41Z)
• Stepwise: Neuro-Symbolic Proof Search for Automated Systems Verification [21.423111823947867]
  This paper introduces a neuro-symbolic proof generation framework designed to automate proof search for systems-level verification projects.<n>The framework performs a best-first tree search over proof states, repeatedly querying an LLM for the next candidate proof step.<n>Results across further benchmarks demonstrate strong generalization, indicating a viable path toward scalable automated software verification.
  arXiv  Detail & Related papers  (2026-03-20T07:45:49Z)
• Test-Time Scaling with Diffusion Language Models via Reward-Guided Stitching [66.39914384073145]
  We propose a self-consistency framework that turns cheap diffusion-sampled reasoning into a reusable pool of step-level candidates.<n>We find that step-level recombination is most beneficial on harder problems.<n>Our training-free framework improves average accuracy by up to 2 across six math and coding tasks.
  arXiv  Detail & Related papers  (2026-02-26T11:08:39Z)
• Proof-RM: A Scalable and Generalizable Reward Model for Math Proof [67.53066972145183]
  Large Language Models (LLMs) have demonstrated strong math reasoning abilities through Reinforcement Learning with *Verifiable Rewards* (RLVR)<n>Many advanced mathematical problems are proof-based, with no guaranteed way to determine the authenticity of a proof by simple answer matching.<n>To enable automatic verification, a Reward Model (RM) capable of reliably evaluating full proof processes is required.
  arXiv  Detail & Related papers  (2026-02-02T17:42:53Z)
• Scaling Code-Assisted Chain-of-Thoughts and Instructions for Model Reasoning [65.20602712957725]
  Caco is a novel framework that automates the synthesis of high-quality, verifiable, and diverse instruction-CoT reasoning data.<n>Our work establishes a paradigm for building self-sustaining, trustworthy reasoning systems without human intervention.
  arXiv  Detail & Related papers  (2025-10-05T07:59:24Z)
• seqBench: A Tunable Benchmark to Quantify Sequential Reasoning Limits of LLMs [1.0519693622157462]
  We introduce seqBench, a benchmark for probing sequential reasoning limits in Large Language Models (LLMs)<n>We find that even top-performing models systematically fail on seqBench's structured reasoning tasks despite minimal search complexity.
  arXiv  Detail & Related papers  (2025-09-21T01:32:13Z)
• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [16.8655558789989]
  We present APOLLO (Automated PrOof repair viaLLM and Lean cOllaboration), a model-agnostic agentic framework for automated theorem proving.<n>A set of agents analyze the proofs, fix the syntax errors, identify the mistakes in the proofs using Lean, isolate failing sub-lemmas, utilize automated solvers, and invoke an LLM on each remaining goal.<n>Our results demonstrate that targeted, compiler-guided repair of LLM outputs yields dramatic gains in both efficiency and correctness.
  arXiv  Detail & Related papers  (2025-05-09T03:38:31Z)
• Sample, Don't Search: Rethinking Test-Time Alignment for Language Models [55.2480439325792]
  We introduce QAlign, a new test-time alignment approach.<n>As we scale test-time compute, QAlign converges to sampling from the optimal aligned distribution for each individual prompt.<n>By adopting recent advances in Markov chain Monte Carlo for text generation, our method enables better-aligned outputs without modifying the underlying model or even requiring logit access.
  arXiv  Detail & Related papers  (2025-04-04T00:41:40Z)
• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  Large language models (LLMs) struggle with consistent and accurate reasoning. LLMs are trained primarily on correct solutions, reducing their ability to detect and learn from errors. We propose a novel collaborative method integrating Chain-of-Thought (CoT) and Program-of-Thought (PoT) solutions for verification.
  arXiv  Detail & Related papers  (2024-10-05T05:21:48Z)
• Self-Evaluation Guided Beam Search for Reasoning [61.523627290397556]
  We introduce a stepwise self-evaluation mechanism to guide and calibrate the reasoning process of Large Language Model (LLM) We propose a decoding algorithm integrating the self-evaluation guidance via beam search. Our approach surpasses the corresponding Codex-backboned baselines in few-shot accuracy by $6.34%$, $9.56%$, and $5.46%$ on the GSM8K, AQuA, and StrategyQA.
  arXiv  Detail & Related papers  (2023-05-01T02:37:59Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.