Generation of Verified Assembly Code Using Dafny and Reinforcement Learning
summary
Reinforcement learning generates assembly programs while a Dafny model of machine state automatically verifies input-output properties, turning testing into full proof. The pipeline maps a 32-instruction subset to read/write state transitions in Dafny, searches about 2 million programs for a 4-element reverse task, and finds a correct implementation after roughly 250k programs (~20 minutes) when verification is offloaded to the cloud. Combining fast unit tests with Dafny verification and cached counterexamples speeds learning and reduces proof overhead.
AI-written summary · about
chapters (9)
- 0:00Verified assembly generation
- 1:26Reinforcement learning basics
- 3:54AlphaDev and its reinforcement learning approach
- 6:00Testing generated programs
- 7:05Dafny for verified code
- 10:37Problem and RL results
- 12:03Optimizing RL performance
- 13:45Testing and verification
- 14:52Q&A
related talks
34mFrom Vibe Coding to Vericoding
18mActive Learning for Neurosymbolic Program Synthesis
59mVerification and Machine Learning
33mFormal Verification of Probabilistic Deep Reinforcement Learning Policies with(…)
59mWhats and Whys of Neural Network Verification (A Declarative Programming Perspec...
14mAutomated Verification of Soundness of DNN Certifiers
20mIncremental Verification of Neural Networks
42mUnraveling AI terminology