Image de couverture de livre

Synthesis and Verification of Transformer Programs (Technical Report)

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Jiang, Hongjian, Hague, Matthew, Rümmer, Philipp, Lin, Anthony Widjaja
Format:	Preprint
Publié:	2026
Sujets:	Machine Learning Formal Languages and Automata Theory Logic in Computer Science
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses(Technical Report)
par: Jiang, Hongjian, et autres
Publié: (2025)

Softmax Transformers are Turing-Complete
par: Jiang, Hongjian, et autres
Publié: (2025)

Parikh's Theorem Made Symbolic
par: Hague, Matthew, et autres
Publié: (2023)

AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs (Technical Report)
par: Chen, Yu-Fang, et autres
Publié: (2024)

Parameterized Verification of Quantum Circuits (Technical Report)
par: Abdulla, Parosh Aziz, et autres
Publié: (2025)

A Practical Specification Language for Automatic Quantum Program Verification (Technical Report)
par: Tsai, Wei-Lun, et autres
Publié: (2026)

Transformers are Inherently Succinct
par: Bergsträßer, Pascal, et autres
Publié: (2025)

Length Generalization Bounds for Transformers
par: Yang, Andy, et autres
Publié: (2026)

The Role of Logic and Automata in Understanding Transformers
par: Lin, Anthony W., et autres
Publié: (2025)

General Decidability Results for Systems with Continuous Counters
par: Balasubramanian, A. R., et autres
Publié: (2025)

Dynamic Programming for Symbolic Boolean Realizability and Synthesis
par: Lin, Yi, et autres
Publié: (2024)

String Solving with Stabilization and Transducers (Technical Report)
par: Chocholatý, David, et autres
Publié: (2026)

Verifying Quantum Circuits with Level-Synchronized Tree Automata (Technical Report)
par: Abdulla, Parosh Aziz, et autres
Publié: (2024)

Negated String Containment is Decidable (Technical Report)
par: Havlena, Vojtěch, et autres
Publié: (2025)

Complementation of Emerson-Lei Automata (Technical Report)
par: Havlena, Vojtěch, et autres
Publié: (2024)

Lemur: Integrating Large Language Models in Automated Program Verification
par: Wu, Haoze, et autres
Publié: (2023)

On Complementation of Nondeterministic Finite Automata without Full Determinization (Technical Report)
par: Holík, Lukáš, et autres
Publié: (2025)

Masked Hard-Attention Transformers Recognize Exactly the Star-Free Languages
par: Yang, Andy, et autres
Publié: (2023)

A Uniform Framework for Handling Position Constraints in String Solving (Technical Report)
par: Chen, Yu-Fang, et autres
Publié: (2025)

Towards Efficient Matching of Regexes with Backreferences using Register Set Automata (Technical Report)
par: Havlena, Vojtěch, et autres
Publié: (2022)

Kofola 1.0: A Modular Approach to ω-Regular Complementation and Inclusion Checking (Technical Report)
par: Alexaj, Ondrej, et autres
Publié: (2026)

Counting Like Transformers: Compiling Temporal Counting Logic Into Softmax Transformers
par: Yang, Andy, et autres
Publié: (2024)

The Counting Power of Transformers
par: Sälzer, Marco, et autres
Publié: (2025)

What Formal Languages Can Transformers Express? A Survey
par: Strobl, Lena, et autres
Publié: (2023)

Runtime Verification: Monitoring, Knowledge, and Uncertainty (Lecture Notes)
par: Bollig, Benedikt
Publié: (2026)

MightyPPL: Verification of MITL with Past and Pnueli Modalities
par: Ho, Hsi-Ming, et autres
Publié: (2025)

Recomposition: A New Technique for Efficient Compositional Verification
par: Dardik, Ian, et autres
Publié: (2024)

SENTIL: A Runtime Verification Tool for Probabilistic Temporal Logic
par: Quansah, Paapa Kwesi, et autres
Publié: (2026)

On the Expressiveness of State Space Models via Temporal Logics
par: Alsmann, Eric, et autres
Publié: (2026)

RNN Generalization to Omega-Regular Languages
par: Pert, Charles, et autres
Publié: (2025)

Learning Quantitative Automata Modulo Theories
par: Hsiung, Eric, et autres
Publié: (2024)

Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification
par: Rao, Balaji, et autres
Publié: (2025)

Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking)
par: Lichtner, Kilian, et autres
Publié: (2025)

Uncertainty Removal in Verification of Nonlinear Systems against Signal Temporal Logic via Incremental Reachability Analysis
par: Besset, Antoine, et autres
Publié: (2025)

Data-Driven Abstractions via Binary-Tree Gaussian Processes for Formal Verification
par: Schön, Oliver, et autres
Publié: (2024)

Fast Obligation Translation and Synthesis
par: Duret-Lutz, Alexandre, et autres
Publié: (2026)

On Dependent Variables in Reactive Synthesis
par: Akshay, S., et autres
Publié: (2024)

Model Checking Temporal Properties of Recursive Probabilistic Programs
par: Winkler, Tobias, et autres
Publié: (2021)

Synthesis of Computable Regular Functions of Infinite Words
par: Dave, V., et autres
Publié: (2019)

Higher-Dimensional Timed Automata for Real-Time Concurrency
par: Amrane, Amazigh, et autres
Publié: (2024)