AI + Logic: New Framework Combines Language Models with Formal Proof Tools

As software generated by machine learning systems becomes more prevalent, verifying its correctness through formal methods grows more critical. Interactive theorem provers like Rocq and Isabelle can ensure programs are mathematically proven to work correctly, but crafting such proofs by hand remains slow and error-prone.

The Complementary Strengths Problem#

Two existing automation approaches each excel in different ways but fall short on their own. Large language models can envision high-level proof strategies and propose reasonable next steps, yet they often make logical errors when drilling into the details. Conversely, specialized automated tactics—such as CoqHammer—excel at solving well-defined local proof obligations but cannot chart a course through longer, multi-step proofs that demand forward planning.

Enter Quarry#

Researchers developed Quarry, a hybrid framework that separates the planning phase from the execution phase. The system works by having an LLM generate multiple candidate proof decompositions, breaking a complex goal into manageable sub-goals and auxiliary lemmas. Each proposed decomposition is then type-checked inside Rocq while sublemmas are temporarily left unsolved, ensuring the structure is valid. The framework then ranks these candidates using a difficulty model that predicts which sub-goals a hammer tactic can solve. Crucially, the system recursively tackles the harder sublemmas within a bounded time budget, converting unwieldy proofs into chains of hammer-solvable steps.

Results and Implications#

Testing Quarry across multiple Rocq benchmarks using state-of-the-art language models showed gains of 7% to 13% in success rate compared to the strongest existing baseline, all while operating under a consistent 10-minute computational budget. The results illustrate that mixing neural-based planning with symbolic proof verification—rather than replacing one with the other—yields more reliable automation. This approach suggests a practical path toward making formal verification less of a bottleneck for AI-assisted software development.