← Back to all news
arXiv AI

Repair, Retry, and the Cost of Hindsight: Verifier Feedback in Formal Theorem Proving

The paper investigates how verifier feedback influences self‑repair in formal theorem proving. Using controlled one‑step experiments on Lean with frozen Qwen3.6‑27B and DeepSeek‑Prover‑V2‑7B, the authors find that showing a model its failed predecessor can hurt success and increase copying, while providing the corresponding compiler error can partially recover performance. In sequential trials, Qwen benefits from correct diagnostics within failed‑proof histories, but no feedback condition outperforms simple instruction‑only resampling, indicating that verifier feedback can aid repair yet cannot fully offset the cost of conditioning on a failed attempt.

Related stories

arXiv AI
4d ago

Fix, Not Just Resample: Bounded Compiler-Guided Repair in Lean 4

The paper presents a bounded, online step-level repair module for Lean 4 that uses compiler error messages to fix rejected tactics instead of discarding them. By sampling up to $K$ candidate tactics and allowing at most $R$ repairs per step, the method improves solve rates over a sampling-only baseline, achieving up to a 32% relative gain and solving 82 additional theorems on a 1,990-theorem subset of the LeanDojo benchmark. The approach trades extra runtime for reachable proofs, with most benefit coming from early repair attempts and shallow tactic failures, and it successfully replicates on the Lean Workbook benchmark, nearly doubling its solve rate without regressions.

By Haotian Deng, Chris Farber, Sonal Narasimha, Samskrithi Sivakumar, Yexiang Xue
llmsbenchmarks
More like this →
arXiv AI
Oct 16

Don't Regenerate, Debug: A Domain-Specific Agent for Repairing Near-Miss Accelerator Kernels

The paper introduces a domain‑specific debugging agent for repairing near‑miss accelerator kernels, arguing that debugging is more efficient than regenerating kernels from scratch. It tackles knowledge scarcity, integrity, and cost control through pattern retrieval, anti‑cheat detection, and convergence safeguards. Empirical results show the debug agent achieves a 66.7% Pass@1 rate and uses 92.8% fewer tokens per success compared to traditional regeneration methods.

By Yansong Sun, Shenxiu Wu, Siyuan Chen, Runlin Hou, Junhao Qiu, Junming Cao, Shudi Shao, Zhichao Lu, Qingfu Zhang
llmsragagentsreinforcement-learningbenchmarks
More like this →
arXiv AI
Aug 5

Don't Regenerate, Debug: A Domain-Specific Agent for Repairing Near-Miss Hardware Operators

arXiv:2608. 02712v1 Announce Type: cross Abstract: Kernel generation for hardware accelerators such as GPUs and NPUs has become a proving ground for large language models (LLMs), and state-of-the-art systems raise correctness through pipelines that couple LLMs with agentic reinforcement learning and evolutionary search.

By Yansong Sun, Shenxiu Wu, Siyuan Chen, Runlin Hou, Junhao Qiu, Junming Cao, Shudi Shao, Zhichao Lu, Qingfu Zhang
llmsragagentsreinforcement-learningbenchmarks
More like this →
arXiv Computation and Language
Aug 31

Why Didn't It Check? Unsupported Final Claims and Their Repair in Two Tool-Equipped Language Models

The study investigates how language models equipped with tools can still produce unsupported final claims, even when a single tool call could resolve the uncertainty. It defines two metrics—occurrence (how often unsupported claims arise) and conditional repair (how often they are fixed when evidence is provided). Experiments on Qwen3-32B and Gemma 4 show that providing the missing evidence consistently repairs all unsupported claims in the Qwen3-32B setup, while the Gemma 4 model never produced unsupported claims under the tested conditions.

By Justin Bronder
llms
More like this →