WitAlloc: Dependency-Aware Claim–Witness Allocation for Neural Proof Repair

A sound check can be spent on the wrong proof node: a cheap leaf may pass while one unchecked upstream error invalidates its dependency cone. WitAlloc therefore allocates a claim and its executable witness jointly. It compiles generated traces into typed dependency DAGs, admits context-bound contracts from five frozen witness families, and ranks affordable pairs by source risk, false-pass-adjusted fidelity, inclusive reach, and cost; a failed contract rebuilds the affected subgraph and must pass a rebound audit. Across miniF2F, SV-COMP, and MATH-Combinatorics, this ordering of an identical typed inventory adds 2.1–2.2 accepted-correct points and removes 2.6–4.2 false-acceptance points relative to uniform placement. Against a 355M-parameter learned step verifier, paired gains are 0.7–0.9 accepted-correct points and 2.0–2.1 fewer false-acceptance points at lower realized cost; prospective natural errors show 4.6–6.1 fewer accepted-wrong points and 4.1–5.4 more repaired-to-correct points. The advantage peaks at intermediate caps and in high-coverage traces, where choosing which evidence to execute matters more than increasing audit volume.