[2603.19715] Stepwise: Neuro-Symbolic Proof Search for Automated Systems Verification

Computer Science > Artificial Intelligence arXiv:2603.19715 (cs) [Submitted on 20 Mar 2026] Title:Stepwise: Neuro-Symbolic Proof Search for Automated Systems Verification Authors:Baoding He, Zenan Li, Wei Sun, Yuan Yao, Taolue Chen, Xiaoxing Ma, Zhendong Su View a PDF of the paper titled Stepwise: Neuro-Symbolic Proof Search for Automated Systems Verification, by Baoding He and 6 other authors View PDF HTML (experimental) Abstract:Formal verification via interactive theorem proving is increasingly used to ensure the correctness of critical systems, yet constructing large proof scripts remains highly manual and limits scalability. Advances in large language models (LLMs), especially in mathematical reasoning, make their integration into software verification increasingly promising. This paper introduces a neuro-symbolic proof generation framework designed to automate proof search for systems-level verification projects. The framework performs a best-first tree search over proof states, repeatedly querying an LLM for the next candidate proof step. On the neural side, we fine-tune LLMs using datasets of proof state-step pairs; on the symbolic side, we incorporate a range of ITP tools to repair rejected steps, filter and rank proof states, and automatically discharge subgoals when search progress stalls. This synergy enables data-efficient LLM adaptation and semantics-informed pruning of the search space. We implement the framework on a new Isabelle REPL that exposes fine-grai...