LLM 驱动的代码分析、验证及生成 January 9, 2026

Presenter: Wangyue Lu Abstract: The absence of formal specifications for external library functions is a fundamental bottleneck in automated program verification. Existing LLM-based specification synthesis approaches rely heavily on function source code and fail when confronted with third-party libraries delivered solely as binaries.

Presenter: Tengjie Lin Abstract: We present three complementary techniques for scalable LLM-driven C program verification. Minimal Support Set (MSS) captures mandatory and disjunctive dependency structures between specifications and verification targets, enabling precise cascade prediction — when a precondition is weakened, the system determines which targets remain safe, which must fail, and which need re-checking, without exhaustive re-verification.

Presenter: Linyu Yang Abstract: This talk presents recent progress in integrating classical techniques with large language models for lemma synthesis in interactive theorem proving, particularly in the context of equivalence proofs for functional programs.

Presenter: Zhongyi Wang Abstract: This talk presents recent research on enhancing the strength and practical applicability of Large Language Model (LLM)-generated formal specifications for C program verification. We discuss two complementary frameworks – AutoACSL and SpecSyn – that address key limitations of prior LLM-based approaches, which often produce specifications lacking semantic depth, verifiability, or sufficient strength for real-world verification tasks.

Presenter: Haokun Li Abstract: CLPoly 是一个 C++ 计算机代数库，其因式分解模块（4,617 行，10 种算法）完全由 LLM Agent（Claude）开发。开发过程中，在所涉及的复杂数学算法中发现了多个算法错误。为解决这一问题，我们指派同一个 LLM Agent 使用 Lean 4 和 Mathlib 对其编写的算法进行形式化验证——创建了一个自验证开发闭环：LLM 编写算法，然后在机器检查的形式方法下证明其正确性。 关键点：在整个过程（开发和验证）中，人类没有编写任何一行代码、证明或文档。人类的角色仅限于战略决策、质量标准和方向纠偏（约 150 条消息，平均约 8 个词）。Agent 自主完成所有技术工作：Mathlib API 调研、自然语言证明草稿、结构化审查、Lean 4 策略证明和迭代调试。最终成果是 6,276 行经机器检查的 Lean 4 证明（零 sorry），覆盖完整因式分解流程——包括单变量（SQF、DDF、EDF、Hensel、Zassenhaus 重组）和多变量（Wang/EEZ、MTSHL 稀疏 Hensel 提升、MDP 求解器、Vandermonde 恢复）。