Repository navigation
[Feature]: anti-pattern mining and objective fitness formulation from burrow.jsonl for heuristic guidance #104
Description
Problem / motivation
Context & Motivation
Proof Burrower maintains an append-only JSONL ledger (burrow.jsonl) recording every proof attempt, specialist recommendation, prover output, and anti-pattern encountered across sessions.
Currently, burrower ledger anti-patterns provides summary text reporting. To support heuristic and metaheuristic search algorithms (like ParadisEO's fitness evaluation operators), we need to extract a formal, quantitative fitness landscape from historical ledger entries.
Proposed solution
Proposed Changes
Quantitative Fitness Evaluator (burrower_core::fitness):
Implement an objective scoring function for candidate proof states:
Fitness(S)=w1⋅GoalReduction(S)+w2⋅SignatureSimilarity(S)−w3⋅AntiPatternPenalty(S)−w4⋅EstimatedTime(S)Fitness(S)=w1⋅GoalReduction(S)+w2⋅SignatureSimilarity(S)−w3⋅AntiPatternPenalty(S)−w4⋅EstimatedTime(S)
Define continuous and ordinal score surfaces for intermediate unproved states (e.g. remaining sub-goal count, term complexity, quantifier depth).
Automated Anti-Pattern Penalty Matrix:
Mine burrow.jsonl for high-frequency failure loops (e.g., looping simplifier rewrites, diverged induction steps).
Compute penalty weights that heavily depress the fitness score of search paths mirroring known anti-patterns.
CLI & Socket Surface:
Expose burrower fitness "<goal>" "<tactic_script>" via CLI and /tmp/burrower.sock so external optimizers and ECHIDNA can query fitness scores on demand.
Acceptance Criteria
Unit tests verify that known anti-patterns in the ledger receive significant negative fitness penalties.
Fitness evaluation latency is under 1 ms1ms per candidate script (in-memory evaluation without invoking live prover).
CLI and socket endpoints conform to the existing line-delimited JSON API specification.
Alternatives considered
No response
Rough scope
None
Additional context
References
Proof Burrower Ledger Specification: docs/ECHIDNA-INTEGRATION.adoc
ParadisEO Evaluation & Fitness Operators: eo/src/eoEvalFunc.h
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)