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

Ning Zhang; Nongyu Di; Xiaoxing Ma; Yuan Yao; Zenan Li

REVIEW 2 major objections 2 minor 1 cited by

Quarry improves Rocq proof success rates by 7% to 13% using solvability-ranked decompositions.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.3

2026-06-26 23:37 UTC pith:24OAX45K

load-bearing objection Quarry gets modest gains on Rocq proofs by having an LLM generate multiple decompositions, type-check them under admits, rank by a difficulty model that predicts hammer success, and recurse inside a fixed time budget. the 2 major comments →

arxiv 2606.17981 v2 pith:24OAX45K submitted 2026-06-16 cs.SE

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

Ning Zhang , Nongyu Di , Zenan Li , Yuan Yao , Xiaoxing Ma This is my paper

classification cs.SE

keywords Rocq proof automationCoqHammerLLM decompositionsolvability rankingformal verificationproof planninghybrid neural-symbolic

verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces Quarry to automate Rocq proofs by having an LLM generate multiple decompositions into sublemmas, type-checking them temporarily, and ranking them with a model that estimates how likely CoqHammer is to solve each one. It then recursively proves the selected sublemmas inside a fixed time budget, converting hard long-range proofs into chains of short solvable goals. This separation of neural planning from symbolic execution raises success rates over baselines on three benchmarks while keeping costs predictable. A reader would care because formal verification is a growing bottleneck for AI-generated code, and the method shows how to combine the strengths of language models and automated tactics rather than relying on one or the other.

Core claim

Quarry asks an LLM to propose multiple proof decompositions with arbitrary sublemmas, type-checks them in Rocq under admitted sublemmas, ranks the candidates by a proof-state-based difficulty model that predicts hammer solvability, and recursively proves sublemmas within a bounded budget, turning long proofs into sequences of hammer-solvable obligations and delivering 7% to 13% higher success rates than the strongest baseline across three Rocq benchmarks under a uniform 10-minute wall-clock limit.

What carries the argument

The proof-state-based difficulty model that estimates hammer solvability of LLM-proposed decompositions to enable ranking and recursive sublemma proving.

Load-bearing premise

The difficulty model accurately predicts which decompositions will be solvable by CoqHammer so that ranking selects effective paths.

What would settle it

A set of proof attempts where the model consistently ranks decompositions that later fail hammer solving above ones that succeed, causing overall failure within the 10-minute budget.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

Long proofs reduce to sequences of short obligations that CoqHammer can discharge.
Success rates rise 7% to 13% over baselines while cost stays predictable inside a fixed time limit.
The same planning-plus-execution loop works with multiple frontier LLMs on multiple benchmarks.
Neural planning and symbolic tactics coordinate without one replacing the other.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same decomposition-ranking idea could be tested on Isabelle or other interactive provers that have strong automated tactics.
If the difficulty model generalizes beyond CoqHammer, it might support hybrid automation for additional tactics or provers.
Higher automation rates could shorten the time needed to verify larger codebases generated by AI tools.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Desk Editor's Note

Quarry gets modest gains on Rocq proofs by having an LLM generate multiple decompositions, type-check them under admits, rank by a difficulty model that predicts hammer success, and recurse inside a fixed time budget.

read the letter

The core idea is straightforward: separate the LLM's job of breaking goals into sublemmas from the hammer's job of discharging them, and use a proof-state difficulty model to decide which decompositions are worth trying first.

What is new is the combination of active multi-candidate generation, temporary type-checking to filter invalid splits, and solvability-aware ranking before bounded recursion. Prior approaches either let the model run the whole proof or hand everything straight to the hammer. This one inserts an explicit planning step that turns long goals into sequences of smaller hammer-friendly obligations.

The paper does well at keeping the method practical. The uniform 10-minute wall-clock budget is a sensible control, and the reported 7-13% lift over the strongest baseline across three benchmarks suggests the ranking step is doing something useful rather than just adding overhead.

The soft spots are in the evaluation details that are missing from the abstract. We do not see how the difficulty model is trained, whether it was tuned on the same benchmarks used for testing, or what the actual baselines implement. Without ablations or error bars it is hard to tell how much of the gain comes from the planning layer versus other factors. These are fixable but they matter for judging whether the result generalizes.

This is for people already working on proof automation in Rocq or similar systems who want to explore LLM-symbolic hybrids. A reader who cares about concrete engineering trade-offs will get value from the architecture even if the numbers need more scrutiny.

The work shows clear thinking about the division of labor and deserves a serious referee so the community can examine the model training, full experimental setup, and any ablations.

Referee Report

2 major / 2 minor

Summary. The manuscript presents Quarry, a planning-based proof synthesis framework for Rocq that separates LLM-driven proof decomposition (proposing sublemmas) from execution. It type-checks candidate decompositions under admitted sublemmas, ranks them via a proof-state-based difficulty model estimating CoqHammer solvability, and recursively discharges sublemmas within a uniform 10-minute wall-clock budget. The central empirical claim is that this yields 7-13% higher success rates than the strongest baseline across three Rocq benchmarks when using frontier LLMs.

Significance. If the results are robust, the work demonstrates a practical hybrid architecture that leverages LLM long-range planning while retaining the local rigor of symbolic tactics such as CoqHammer. This coordination approach, rather than end-to-end replacement, addresses a recognized bottleneck in interactive theorem proving and supplies a concrete, budget-constrained evaluation protocol that could be adopted by subsequent systems.

major comments (2)

[§3] The difficulty model is load-bearing for the ranking and recursive decomposition claims (§3, difficulty-aware ranking paragraph), yet the manuscript supplies no training procedure, feature definition, or validation against actual hammer outcomes; without these, it is impossible to assess whether the model reliably predicts solvability or merely correlates with superficial proof-state properties.
[§5] The reported 7-13% gains rest on comparisons to external baselines, but the evaluation section provides no information on benchmark definitions, baseline re-implementations, statistical significance tests, error bars, or data-exclusion rules; this absence prevents verification that the stated improvements support the central claim.

minor comments (2)

[§3.2] Notation for the difficulty score and the precise interface between SerAPI and the ranking step could be clarified with a small pseudocode listing or equation.
[Abstract] The abstract and introduction repeat the 7-13% figure without indicating whether it is an absolute or relative improvement; a single clarifying sentence would remove ambiguity.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive feedback. We address each major comment below and will revise the manuscript to improve clarity and completeness where the concerns are valid.

read point-by-point responses

Referee: [§3] The difficulty model is load-bearing for the ranking and recursive decomposition claims (§3, difficulty-aware ranking paragraph), yet the manuscript supplies no training procedure, feature definition, or validation against actual hammer outcomes; without these, it is impossible to assess whether the model reliably predicts solvability or merely correlates with superficial proof-state properties.

Authors: We agree that the current description of the difficulty model in §3 is insufficiently detailed for assessing its reliability. The model is intended as a lightweight estimator of CoqHammer solvability based on proof-state features, but the manuscript does not provide the requested specifics. In the revised version we will expand the section to define the exact features, describe the training procedure (including the dataset construction and learning method), and report validation results comparing model predictions to actual hammer success rates on held-out proof states. This addition will directly address the concern about predictive power versus superficial correlation. revision: yes
Referee: [§5] The reported 7-13% gains rest on comparisons to external baselines, but the evaluation section provides no information on benchmark definitions, baseline re-implementations, statistical significance tests, error bars, or data-exclusion rules; this absence prevents verification that the stated improvements support the central claim.

Authors: We acknowledge that §5 currently lacks the level of detail needed for full reproducibility and verification of the reported gains. In the revised manuscript we will augment the evaluation section with: explicit definitions and sources for the three Rocq benchmarks, descriptions of baseline re-implementations (including any adaptations made), results of statistical significance tests with appropriate error bars or confidence intervals, and a clear statement of any data-exclusion criteria. These additions will allow independent assessment of whether the 7-13% improvements are robustly supported. revision: yes

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper describes an empirical system (Quarry) that combines LLM planning with CoqHammer execution and a difficulty model for ranking decompositions. All reported results are direct success-rate comparisons against external baselines under a fixed wall-clock budget; no equations, derivations, fitted parameters renamed as predictions, or load-bearing self-citations appear in the provided text. The architecture is presented as a pragmatic engineering combination rather than a mathematical derivation that reduces to its own inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract supplies no information on free parameters, axioms, or invented entities.

pith-pipeline@v0.9.1-grok · 5804 in / 1125 out tokens · 37956 ms · 2026-06-26T23:37:13.433556+00:00 · methodology

0 comments

read the original 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.

Figures

Figures reproduced from arXiv: 2606.17981 by Ning Zhang, Nongyu Di, Xiaoxing Ma, Yuan Yao, Zenan Li.

**Figure 1.** Figure 1: Proof tree for max_deg_remove_node found by Quarry. The tree has depth 3 and 12 nodes. Green leaves are discharged by CoqHammer or simple induction; blue nodes required further decomposition. Each leaf involves only one or two definitions, making it tractable for automation. • degree_remove_node_preserve: removing a non-adjacent node preserves the degree of 𝑣 (requires one further sublemma about set cardi… view at source ↗

**Figure 2.** Figure 2: Quarry workflow. Given a goal, the system enters the Generate–Rank–Solve loop: the LLM proposes 𝑘 candidate decompositions, which are filtered by Rocq-side verification (Admitted sublemmas); the difficulty model ranks survivors by estimated solvability; and the top-𝐵 candidates are recursively solved using automation tools (e.g., CoqHammer). Unsolved subgoals re-enter the loop (dashed arrow). The bottom r… view at source ↗

**Figure 3.** Figure 3: How Quarry processes the root goal of the running example through the Generate–Rank pipeline. The LLM produces a structured decomposition; Rocq verification (part of Generate) confirms conditional correctness; the difficulty model estimates sublemma solvability. candidate–outcome mapping needed to evaluate alternative ranking policies without new LLM calls. 5 Difficulty-Aware Ranking and Learning Recall th… view at source ↗

**Figure 4.** Figure 4: Cumulative success rate vs. wall-clock time. Over 90% of successful proofs complete within 5 minutes; [PITH_FULL_IMAGE:figures/full_fig_p017_4.png] view at source ↗

**Figure 5.** Figure 5: reports per-theorem token usage and LLM request counts for Quarry and Cobblestone on the three benchmarks. Quarry uses fewer requests per theorem than Cobblestone on all benchmarks (e.g., 7.2 vs. 11.5 on CoqGym100) while proving more theorems, reflecting the efficiency of difficulty-aware ranking in avoiding fruitless decomposition paths. On Wigderson100, Quarry’s per-theorem token usage is higher (45.6K v… view at source ↗

**Figure 6.** Figure 6: Effect of rollout budget 𝑘 on the number of proved theorems. The default 𝑘=8 captures most of the benefit; gains plateau beyond 𝑘=12. Takeaway. Both ranking and deep CoqHammer integration are individually significant. Ranking steers the budget toward hammer-solvable decompositions, while invoking CoqHammer at every node captures leaf-level goals that LLM-only methods miss. 6.5 RQ4: Budget Sensitivity, LLM … view at source ↗

**Figure 7.** Figure 7: Effect of leaf-goal solver. Replacing CoqHam [PITH_FULL_IMAGE:figures/full_fig_p020_7.png] view at source ↗

discussion (0)

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints
cs.AI 2026-07 conditional novelty 6.0

Typed local edits on Lean proof blueprints match free-form repair coverage on localized defects while using far fewer tokens and lower cost.