NEW COURSE for SPRING 2026:
	      CISC 867.012: Seminar: Automated Reasoning
	 Feb 3 -- May 14 2026, Tue/Thu 2:20--3:40 PM, ISE 222
		      Instructor: Stephen Siegel


  "...automated formal reasoning helps us move from AI-based sentence
   completion to verifiable reasoning, and ... that unlocks trust, and
   new markets. You don’t need formal reasoning to write a poem. But
   when billions of dollars, personal data, or human lives are at
   stake? You do! In high-stakes systems, we need AI that can prove
   it’s right."
   
      --- Byron Cook
          Vice President and Distinguished Scientist
          Amazon Web Services
          

What is the future of generative AI?

Generative AI tools such as Claude have become amazingly powerful.
But ask anyone who uses them and they will tell you that you can never
trust the output.  Every line of generated code must be carefully
checked.  Worse, the code often looks correct on the surface, but has
very subtle bugs, almost as if the AI is trying to fool you.

This is where formal, automated reasoning comes in.

The field is moving towards a future where AI generates the code, and
formal verification tools like Rocq automatically provide the proof of
its correctness.  Rocq, and the closely related Lean theorem prover,
are being used in numerous projects involving AI, such as Google's
DeepMind.  They are the future of verified generated code and verified
mathematics.

Automated reasoning is a field of computer science concerned with
algorithmic approaches to logical reasoning.  Applications include
checking proofs of mathematical theorems, verifying properties of
computer programs or protocols, and verifying solutions produced by
generative AI models.  A number of AR tools have been developed, some
fully automatic and others requiring human interaction, and are being
used at companies such as Amazon, Google, and Meta.  This seminar
course covers the foundations of AR in logic, functional programming,
and type theory, and the use of state-of-the-art AR tools such as Rocq
and Lean.

The main text for the course is "Software Foundations Vol. 1: Logical
Foundations" (https://softwarefoundations.cis.upenn.edu).  It covers
the basic use of Rocq (formerly Coq) and associated theory, from the
ground up.  Participants will take turns presenting material from this
text and will do a small final project applying Rocq to a problem of
their choice.

Rocq is one of the most innovative and transformative tools in
Computer Science.  In 2013, it won the ACM Software System Award and
the ACM SIGPLAN Programming Languages Software Award.  It has had
numerous groundbreaking applications, including the development of
CompCert, a fully verified C compiler, which won the same two awards
in 2021 and 2022.  Rocq also revolutionized the field of formal,
mechanized mathematics with the groundbreaking formal proof of the
Feit-Thompson Odd Order Theorem in group theory.

Prerequisites: an undergraduate course in logic would be helpful;
programming experience in any language

References:

https://www.linkedin.com/feed/update/urn:li:activity:7420223009418027008/
https://rocq-prover.org
https://softwarefoundations.cis.upenn.edu
https://compcert.org
https://en.wikipedia.org/wiki/Feit–Thompson_theorem
https://lean-lang.org/use-cases/cedar/

Questions?  Email siegel@udel.edu.