Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs

• URL: http://arxiv.org/abs/2604.18587v1
• Date: Fri, 13 Mar 2026 01:33:20 GMT
• Title: Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs
• Abstract summary: Large language models (LLMs) have demonstrated significant potential in formal theorem proving.<n>We exploit an informative structure in formal verification: the observation that compilers map a vast space of diverse proof attempts.<n>We introduce a learning-to-refine framework that leverages this compression to perform efficient learning and proof exploration.
• Score: 48.390500145598544
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large language models (LLMs) have demonstrated significant potential in formal theorem proving, yet state-of-the-art performance often necessitates prohibitive test-time compute via massive roll-outs or extended context windows. In this work, we address this scalability bottleneck by exploiting an informative structure in formal verification: the observation that compilers map a vast space of diverse proof attempts to a compact set of structured failure modes. We introduce a learning-to-refine framework that leverages this compression to perform efficient learning and proof exploration. We perform tree search that corrects errors locally conditioned on explicit verifier feedback, thereby circumventing the costs associated with accumulating a long history of proof attempts. Extensive evaluations show that our method consistently amplifies the reasoning capabilities of base provers across varying scales. Notably, our approach achieves state-of-the-art performance on PutnamBench among publicly reported $\sim$8B and $\sim$32B parameter models under comparable test-time budgets, offering a scalable paradigm for next-generation verifier-guided reasoning.

Related papers

• Efficient Test-Time Optimization for Multi-Agent Proof Autoformalization [20.22828310618122]
  ToMap is a framework that structures proof autoformalization as a Decomposer-Formalizer-Prover pipeline.<n>We show that ToMap improves over the best previous method by 19.0% when evaluated by both syntactic correctness and semantic faithfulness.
  arXiv  Detail & Related papers  (2026-07-13T09:21:15Z)
• PLUME: Latent Reasoning Based Universal Multimodal Embedding [52.35354073629127]
  Universal multimodal embedding (UME) maps heterogeneous inputs into a shared retrieval space with a single model.<n>Recent approaches improve UME by generating explicit chain-of-thought (CoT) rationales before extracting embeddings.<n>We propose PLUME, a latent reasoning framework that advances UME by replacing verbalized CoT with a short autoregressive rollout of continuous latent states.
  arXiv  Detail & Related papers  (2026-04-02T14:04:53Z)
• Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models [8.948475969696075]
  Agentic theorem provers are pipelines that couple a mathematical reasoning model with library retrieval, subgoal-decomposition/search planner, and a proof assistant verifier.<n>We propose a distributional viewpoint and introduce provability, defined as the finite-horizon success probability of reaching a verified proof.<n>We provide a principled, component-sensitive explanation of when and why agentic theorem provers succeed on biased real-world problem distributions.
  arXiv  Detail & Related papers  (2026-02-11T05:22:24Z)
• Advancing Mathematical Research via Human-AI Interactive Theorem Proving [16.40852561664514]
  We propose a human-in-the-loop workflow for interactive theorem proving and discovery with LLMs.<n>Human experts retain control over problem formulation and admissible assumptions, while the model searches for proofs or contradictions.<n>We instantiate this workflow in a case study on the connection between manifold optimization and Grover's quantum search algorithm.
  arXiv  Detail & Related papers  (2025-12-10T09:16:27Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• Typed Chain-of-Thought: A Curry-Howard Framework for Verifying LLM Reasoning [0.0]
  Chain-of-Thought (CoT) prompting enhances the reasoning capabilities of large language models.<n>We propose a novel theoretical lens for this problem grounded in the Curry-Howard correspondence.<n>We operationalise this analogy, presenting methods to extract and map the informal, natural language steps of CoT into a formal, typed proof structure.
  arXiv  Detail & Related papers  (2025-10-01T16:06:40Z)
• Implicit Reasoning in Large Language Models: A Comprehensive Survey [67.53966514728383]
  Large Language Models (LLMs) have demonstrated strong generalization across a wide range of tasks.<n>Recent studies have shifted attention from explicit chain-of-thought prompting toward implicit reasoning.<n>This survey introduces a taxonomy centered on execution paradigms, shifting the focus from representational forms to computational strategies.
  arXiv  Detail & Related papers  (2025-09-02T14:16:02Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheorem is a comprehensive informal theorem-proving framework exploiting natural language to enhance mathematical reasoning.<n>DeepTheorem includes a large-scale benchmark dataset consisting of 121K high-quality IMO-level informal theorems and proofs.<n>We devise a novel reinforcement learning strategy (RL-Zero) explicitly tailored to informal theorem proving, leveraging the verified theorem variants to incentivize robust mathematical inference.
  arXiv  Detail & Related papers  (2025-05-29T17:59:39Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof.<n>Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment.
  arXiv  Detail & Related papers  (2024-07-14T01:43:07Z)
• Compact Proofs of Model Performance via Mechanistic Interpretability [1.4197963050877802]
  We propose using mechanistic interpretability to derive and compactly prove formal guarantees on model performance. We prototype this approach by formally proving lower bounds on the accuracy of 151 small transformers trained on a Max-of-$K$ task.
  arXiv  Detail & Related papers  (2024-06-17T17:34:25Z)

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.