7 papers
Synthesis and Verification of Transformer Programs (Technical Report)
Hongjian Jiang, Matthew Hague, Philipp Rümmer +1
C-RASP is a simple programming language that was recently shown to capture concepts expressible by transformers. In this paper, we develop new algorithmic techniques for automatica…
Softmax Transformers are Turing-Complete
Hongjian Jiang, Michael Hahn, Georg Zetzsche +1
Hard attention Chain-of-Thought (CoT) transformers are known to be Turing-complete. However, it is an open problem whether softmax attention Chain-of-Thought (CoT) transformers are…
Extracting Robust Register Automata from Neural Networks over Data Sequences
Chih-Duo Hong, Hongjian Jiang, Anthony W. Lin +3
Automata extraction is a method for synthesising interpretable surrogates for black-box neural models that can be analysed symbolically. Existing techniques assume a finite input a…
The Power of Regular Constraint Propagation (Technical Report)
Matthew Hague, Artur Jeż, Anthony W. Lin +2
The past decade has witnessed substantial developments in string solving. Motivated by the complexity of string solving strategies adopted in existing string solvers, we investigat…
OSTRICH2: Solver for Complex String Constraints
Matthew Hague, Denghang Hu, Artur Jeż +4
We present OSTRICH2, the latest evolution of the SMT solver OSTRICH for string constraints. OSTRICH2 supports a wide range of complex functions on strings and provides completeness…
HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses(Technical Report)
Hongjian Jiang, Anthony W. Lin, Oliver Markgraf +2
We present HornStr, the first solver for invariant synthesis for Regular Model Checking (RMC) with the specification provided in the SMT-LIB 2.6 theory of strings. It is well-known…