Class Schedule Listing |
Fall 2025 Semester
Jul 10, 2026 |
|
 |
||
| SpTp:AI-EnabledFormalReasoning - 18744 - CS 7485 - 01 | ||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
|
Topic: AI-Enabled Formal Reasoning
Course Description: This PhD-level seminar explores the rapidly
developing intersection of large language models (LLMs) and formal
reasoning. The course begins with two foundational modules:
(1) Logic and Formal Methods: Core concepts in logic, automated and
interactive theorem proving, and formal verification.
(2) Contemporary AI Foundations: The current state of LLM technology,
including transformer architectures, agentic/CLI AI, and emerging
hybrid AI-formal systems.
The central focus is on AI-enabled formal reasoning: how LLMs can
augment or automate formal reasoning workflows, and how formal methods
can enhance the reliability, interpretability, and alignment of AI
systems. Topics include LLM-assisted proof synthesis, tactic
prediction, premise selection, counterexample generation,
specification mining, and lemma discovery.
The course is built around close reading and critical evaluation of
recent research literature. In addition, students will complete two
major projects:
Replication Project – Reproduce and rigorously assess the results of a
recent research paper.
Research Project – Propose, implement, and empirically evaluate an
original idea at the intersection of LLMs and formal reasoning.
By the end of the course, students will be equipped to conduct
original, publishable research at the frontier of AI and formal
methods.
Prerequisites: Strong background in logic and formal reasoning,
familiarity with deep learning concepts, and mathematical
maturity. Prior experience with theorem provers (e.g., ACL2/s, Coq,
Isabelle, Lean, PVS) is recommended.
Associated Term: Fall 2025 Semester Registration Dates: Apr 01, 2025 to Sep 16, 2025 Levels: Graduate Attributes: GSCS Computer & Info Science, Topics Course Boston Campus Lecture Schedule Type Traditional Instructional Method 4.000 Credits View Catalog Entry
|
| Return to Previous |
|
