讲座摘要：Existing informal language-based (e.g., human language) Large Language Models (LLMs) trained with Reinforcement Learning (RL) face a significant challenge: their verification processes, which provide crucial training signals, are neither reliable nor scalable. In fact, the prevalent large proprietary models could hardly generate verifiable programs. A promising yet largely uncharted alternative is formal language-based reasoning. Grounding LLMs in rigorous formal systems where generative models operate in formal language spaces (e.g., Dafny) enables the automatic and mathematically provable verification of their reasoning processes and outcomes. This capability is pivotal for achieving large-scale, reliable formal software verification. It is a common practice to employ human-annotated chain-of-thought and other human priors to induce the reasoning and coding capabilities of LLMs. Unfortunately, it becomes unacceptably all-consuming to provide such priors for supervising complex programming tasks. In this work, we systematically explore ways to reduce human priors with the formal language, Dafny, as the main environment for our pilot study. Our pipeline mainly relies on introducing an automatic and scalable data curation pipeline, and careful RL designs integrated with feedback from the formal language verifier. We introduce DafnyComp, a benchmark of compositional formal programs with auto-formalized specifications for specification reasoning. Our supervised fine-tuning (SFT) stage enables even small models (e.g., 0.5B) to generate syntactically valid and verifiable Dafny code.
讲者信息：付杰目前是上海人工智能实验室的青年科学家，同时是上海创智学院全职导师。他曾在加拿大Mila做博后，师从Yoshua Bengio和Chris Pal。他博士毕业于新加坡国立大学，师从Tat-Seng Chua。他获得过ICLR 2021，NAACL 2024杰出论文奖。他目前的研究兴趣是深度强化学习、大语言模型、自动形式化验证等技术，用于降低人类社会的各种防御成本，从而提升人类社会的整体抗风险能力。其个人主页为 https://bigaidream.github.io/
