Verified computation of integrals in Iscalc and experiments with LLMs
报告人：詹博华 (华为编程语言实验室)
时间：2025-04-20 10:00-11:00
地点：智华楼413
摘要：
Iscalc is a tool for verifying step-by-step computations in mathematics, such as computations of integrals and infinite series. It lies in the middle of a spectrum between computer algebra systems and interactive theorem provers, allowing users to specify computations at a higher level of abstraction compared to ITPs such as Lean and Isabelle. As such, we expect that with proper guidance, large language models can generate checked computations in Iscalc more easily than formal proofs in an ITP. We show in preliminary experiments that this is indeed the case, and describe construction of LLM agents for generating computations in Iscalc.
报告人简介：
詹博华，华为编程语言实验室技术专家。2014年博士毕业于普林斯顿大学数学系，之后在麻省理工学院和慕尼黑工业大学任博士后。2018-2024年在中科院软件所任副研究员。2024年加入华为编程语言实验室。研究工作包括证明自动化方法和交互式定理证明器的设计与实现，嵌入式系统的建模与验证，以及在程序验证、操作系统、分布式系统、量子程序验证的应用。在CAV, IJCAR/CADE, TACAS, ITP, J. Automated Reasoning等形式化方法领域的主要会议和期刊发表文章30余篇。
