Repository navigation
[Feature]: combinatorial tactic playbook synthesis using delta/partial neighborhood evaluation (ParadisEO-mo) #105
Description
Problem / motivation
Context & Motivation
Proof Burrower currently indexes lemma signatures and routes stuck proof goals through specialist readers (Algebraist, Combinatorialist, Order-Theorist). Each specialist emits a relatively static or linearly sequenced "tactic playbook" which is then executed against echidna prove --prover Isabelle.
Finding an effective tactic script is fundamentally a discrete combinatorial optimization problem over a non-linear search space:
Tactic choice (simp, auto, blast, metis, induction, coinduction).
Rule ordering and lemma arguments.
Instantiation terms and quantifier substitutions.
ParadisEO’s mo (Moving Objects) module is uniquely specialized for combinatorial local search (Simulated Annealing, Tabu Search, Variable Neighborhood Search) using partial/delta evaluation—evaluating the fitness change of a neighborhood operator without full recalculation.
Proposed solution
Proposed Changes
Neighborhood Move Operators for Proof Scripts:
Define discrete mutation and neighborhood operators for tactic ASTs:
Swap adjacent tactic steps.
Substitute premise tokens based on signature Jaccard distance.
Adjust tactic parameter flags (e.g. simp add: ... vs blast).
Delta Evaluation & Tactic Cache:
Implement state caching for intermediate proof goals: when a mutation only modifies step kk in an nn-step script, replay steps 1…k−11…k−1 from cache and evaluate only the delta from step kk onwards.
Local Search Engine in Specialist Swarm:
Integrate a Tabu Search / VNS driver in burrower swarm to dynamically explore high-ranking tactic mutations when baseline specialist playbooks fail.
Enforce strict attempt bounds and timeouts before falling back to manual review.
Acceptance Criteria
burrower swarm demonstrates automated synthesis of multi-step proofs on a set of benchmark lemmas that fail under static single-specialist playbooks.
Intermediate goal caching reduces redundant prover invocations by at least 40%40% during local search iterations.
Full compatibility maintained with existing burrow.jsonl ledger formats.
Alternatives considered
No response
Rough scope
None
Additional context
References
ParadisEO Local Search & Neighborhoods: mo module in [nojhan/paradiseo](https://nojhan.github.io/paradiseo/#Why)
Proof Burrower Architecture: crates/burrower-core
Before submitting
- I searched existing issues and discussions for this idea.
- This fits the scope and goals of the project as I understand them.
- I would be willing to help implement this.
Activity
docs(plans): ultraplan and cross-repo hand-offs (plan only) (#106)