Generation of Verified Assembly Code Using Dafny and Reinforcement Learning

Explore the innovative approach of using Dafny and reinforcement learning to generate verified assembly code in this 18-minute conference talk from ACM SIGPLAN. Discover how Christopher Brix and Jean-Baptiste Tristan address the challenge of ensuring correctness in machine-generated assembly code, particularly for complex tasks where exhaustive testing is not feasible. Learn about the integration of Dafny into the reinforcement learning process, enabling automatic verification of assembly programs against input-output constraints without human intervention. Gain insights into how this method can guide AI agents to develop efficient and verified solutions for intricate programming tasks, building upon the recent success of algorithms like AlphaDev in generating high-performance assembly code.