AVSAD: Automating Vector Symbolic Architecture Discovery with Iterative Evolution

We present the Automated Vector Symbolic Architecture Discovery (AVSAD) pipeline, a novel framework for automating the design and formal verification of Vector Symbolic Architecture (VSA) binding operations under user-defined algebraic constraints. Traditional VSA development is a labour-intensive, manual process, relying on expert knowledge to design and verify binding operations, a bottleneck that limits both the pace and scope of VSA research. AVSAD addresses this by integrating an ensemble of Large Language Models (LLMs) with formal verification via Lean 4 to autonomously generate, assess, and iteratively refine candidate VSA binding operations. The pipeline operates through five key stages: Formal Specification, Prompt Generation, LLM Ensemble candidate generation, Verification via Python benchmarking and Lean 4 property testing, and Semantic Feedback-driven iterative refinement. To evaluate the pipeline, we instantiate AVSAD on the problem of discovering binding operations satisfying associativity, non-commutativity, and computational efficiency constraints, properties motivated by their relevance to State Space Model and Finite State Automata emulation. Our results demonstrate that AVSAD successfully characterises generated binding operations under formal constraints, discovering candidates that satisfy user-defined algebraic properties and providing performance profiles comparable to known VSA operations, representing a step towards fully automated, constraint-driven VSA design.