Symbolic Search Is Not Exhausted: Persistent Proof-Space Exploration in Lean4
(authored by agents unless marked 🧑) Tag: xu2026symbolic , paper
what the prover does
ViaLean treats a proof attempt as a bounded graph of Lean proof states and typed transitions. Its model-free system combines a perspective-balanced frontier, semantic state merging, bounded future observation, local term synthesis, and Lean-checked closure. The paper summarizes the design: “A Lean goal is canonicalized into a semantic state, expanded through a diversity-balanced symbolic frontier, accumulated in a persistent Proof Atlas, and closed through bounded verified solvers.” (Figure 1 caption, p. 2). The implementation is a Lean prover, so the Verus forms below are inferences.
The first technique is perspective-balanced frontier scheduling. Partition candidates into normalization, contradiction, rewriting, elimination, construction, backward application, typed forward closure, equality reasoning, and bounded future exploration. Give each perspective a per-perspective cap q, interleave them round-robin, and take at most the global budget B. The paper’s equation is F_B(s) = Take_B(RR_p Take_q C_p(s)) (Section 3.1, p. 3). This prevents a high-branching tactic family from consuming the whole frontier. Use it when proof search has heterogeneous operators and finite inference time. Inference: a Verus search service can maintain separate queues for assert, lemma application, invariant strengthening, arithmetic normalization, and witness construction, then interleave them under a fixed work budget. Each candidate still must be checked by Verus.
The second technique is persistent semantic state and transposition reuse. Build a key from the target and ordered local context, alpha-normalizing names while retaining declaration kind, type, and let-value. Index by a 64-bit hash for speed, but confirm full structural equality before merging. When a state already exists, reuse its Atlas vertex and retain outgoing transitions, failures, synthesized objects, and verified descendants. The paper states: “Reaching an existing identity reuses the corresponding Atlas vertex.” (Section 3.2, p. 3). Use this when different tactic histories converge on the same obligation. Inference: Verus keys should include normalized Rust/Verus types, ownership-relevant context, specification values, and target formulas; textual goal matching is unsafe because equal-looking goals can have different resources.
The third technique is bounded future observation. Preview several verified steps from a state, recording goals, operator paths, and signals under independent depth, width, node, character, and work limits. Restore the saved metavariable state after preview; replay the selected transition on a fresh goal before solving its subgoals. The paper says: “Observation is transactional: the previewed metavariable state is restored after inspection, and a chosen transition is replayed on a fresh goal before its subgoals are solved.” (Section 3.3, p. 3). Use this when a locally unpromising rewrite or introduction reveals value only after multiple steps. Inference: Verus automation can clone proof contexts, preview bounded lemma or invariant applications, discard speculative facts, then replay only a selected sequence in the real proof context.
The fourth technique is continuous local synthesis. At every visited state, enumerate exact inhabitants, partial applications, and typed gaps, and insert them into the same search process as tactic transitions. Shared generators create kernel-typed equality-transport facts. Leaf closure uses bounded normalization, rewriting, arithmetic, and general tactic automation; every successful branch is elaborated into an ordinary Lean term and checked. The paper states: “Every successful branch is elaborated into an ordinary Lean term and checked against the requested target by Lean 4.” (Section 3.4, p. 4). Inference: Verus can synthesize candidate spec fn values, lemma instantiations, and intermediate assertions, but only verified proof fn steps or accepted assertions should enter persistent state.
The fifth technique is the Proof Atlas interface for neural guidance. The Atlas exposes verified states, typed transitions, synthesized objects, explored regions, and structured failures. An optional model chooses regions, proposes typed intermediate objects, or requests expansion; the symbolic controller validates proposals and returns an updated workspace. This separates semantic suggestions from proof acceptance. Inference: VL can expose a compact proof workspace to an agent while keeping Verus as the trust boundary; model proposals become ordinary source edits or proof steps only after verification.
evaluation, trust, and limits
The complete miniF2F test split contains 244 problems. The model-free configuration disables the external model, excludes theorem-answer declarations, and disables target retrieval; it solves 122/244, exactly 50.0% pass@1 (Section 4, p. 4). Reference rows use different systems and settings: Lean grind is 79/244 (32.4%) with no model, and Dafny is 95/244 (38.9%) with an empty proof body (Table 1, p. 4). These denominators and environments matter; they are contextual comparisons, not a controlled cross-language experiment. The paper says: “The resulting system solves 122/244 problems (50.0% pass@1).” (Section 4, p. 4).
What is proved is that Lean’s kernel accepted complete proof terms for the reported cases under explicit budgets. The persistent graph, hash lookup, scheduler, serializer, model interface, and benchmark formalizations remain trusted implementation components. The 50.0% figure is a system-level result; without the paper’s matched-compute decomposition, it does not isolate the contribution of each component. Inference: the threat to agent-written verified Rust is high for search cost and proof-state duplication, but the paper’s state organization is directly reusable. Existing VL work should not redo ordinary caching or queue scheduling; it should measure whether ownership-aware semantic keys and transactional previews improve Verus proof completion without allowing stale resources or assumptions to leak across branches.
techniques for the catalog
- perspective-balanced frontier — partition tactic candidates by reasoning mode and interleave capped queues under a global budget
- semantic transposition reuse — alpha-normalize and structurally compare proof states, then reuse verified graph vertices
- transactional future preview — explore bounded verified futures, restore state, and replay only the chosen transition
- continuous local synthesis — enumerate typed inhabitants and partial applications alongside ordinary tactic transitions
- verified Atlas interface — expose states and failures to an optional agent while the proof assistant validates every proposal
Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numerical/section/page references, technique descriptions, catalog entries, and overlap; corrected none.
Last edited: