BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Automatically Formally Verified Hardware using Aristotle - Satnam 
 Singh\, Software Engineer\, Harmonic
DTSTART:20260226T140000Z
DTEND:20260226T150000Z
UID:TALK243940@talks.cam.ac.uk
CONTACT:Professor Andrew W. Moore
DESCRIPTION:Aristotle is an AI theorem prover developed by "Harmonic":http
 ://harmonioc.fun which can autonomously produce multi-thousand-line formal
 \nproofs of theorems expressed in Lean 4. It achieved "Gold Medal equivale
 nt performance":https://harmonic.fun/news#blog-post-imo for the 2025 Inter
 national Mathematical Olympiad (IMO). The Aristotle system takes a Lean th
 eorem without a proof and attempts to find a proof of the theorem (when o
 ne exists). The proofs that Aristotle generates are *machine checked* by t
 he Lean 4 interactive theorem prover\, which has the highly desirable prop
 erty of an LLM-based system that *produces an answer without hallucination
 *.\n\nThis talk is aimed at a general audience and does not assume much kn
 owledge about interactive theorem provers or hardware design. The first pa
 rt of this will talk discuss the recent rise in the use of AI theorem prov
 ers and present a few high level details about the techniques Aristotle us
 ed to tackle hard problems like the IMO challenge e.g. interleaving formal
  and informal reasoning. The second part of the talk will illustrate how d
 igital hardware can be described using "Geraint Jones":https://www.cs.ox.a
 c.uk/people/geraint.jones/ and "Mary Sheeran":https://www.cse.chalmers.se/
 ~ms/ 's Ruby relational hardware description language implemented in Lean 
 4 as an embedded domain specific language. Hardware design in Ruby enjoys 
 many useful algebraic properties and typically involves applying a rich co
 llection of theorems to transform and optimize circuits. This talk will wa
 lk through a circuit design example using Ruby\, with formally expressed c
 ircuit properties automatically proved by Aristotle.\n\nAn argument will b
 e made to support the idea that a well curated collection of composable ci
 rcuit building blocks backed with a rich collection of algebraic propertie
 s for circuit transformation forms a solid basis not only for verifying pr
 operties of circuits\, but also for using machine learning to automaticall
 y *synthesize correct by construction* circuits from specifications.\n\nBi
 o: Satnam Singh is a software engineer at Harmonic working on the formal v
 erification of hardware and software. He has previously worked on the desi
 gn of machine learning chips at Google and Groq\, orchestration of distrib
 uted systems as an early member of the Kubernetes team at Google\, the dev
 elopment of tools and techniques for the formal verification of hardware a
 t Xilinx\, high level synthesis of hardware at Microsoft\, and the optimiz
 ation of Android applications at Facebook/Meta. https://satnam6502.github.
 io/bio
LOCATION:Computer Lab\, FW26
END:VEVENT
END:VCALENDAR