RSS Meetups are monthly gatherings of LASIGE members with research interests mainly in Software Architecture, Verification, Testing, Programming Languages, Type Systems, Logic, Concurrency, and Formal Methods.

Title: Teaching LLMs Program Semantics via Symbolic Execution Traces
Speakers: Jonas Bayer (University of Cambridge)
When: July 10th, 2026, 14h00
Where: Ciências ULisboa, 6.3.27
Invited by: Alcides Fonseca

Abstract: We introduce an evaluation framework of 500 code understanding tasks in the C programming language and evaluate 14 LLMs across six families. The benchmark is built on the software verification competition SV-COMP 2025 and tests five different code properties (memory safety, overflow, termination, reachability, data races). We find that high overall accuracy masks a critical weakness: while most models reliably confirm properties hold, violation detection varies widely and degrades sharply with program length.
To close this gap, we train on formal verification artifacts: running the Soteria symbolic execution engine on generic open-source C code and using the resulting traces for continued pretraining of Qwen3-8B. Just ∼3,000 bug traces combined with chain-of-thought reasoning at inference time improve violation detection by over 17 percentage points, producing one of the most balanced accuracy profiles among evaluated models. On violation detection, the trained 8B model outperforms the 4× larger Qwen3-32B without thinking and approaches it in overall accuracy. The interaction between trace training and chain-of-thought is superadditive: neither alone provides meaningful gains, but their combination does. Improvements transfer across all five property types, including ones the training traces do not target. Our 28 configurations confirm the gains stem from trace semantics, not code volume, and that trace curation and format matter.

Bio: Jonas Bayer is a PhD student at the University of Cambridge under the supervision of Timothy Gowers. His research focuses on automated theorem proving: how can neural and symbolic methods interact? How can we push interactive theorem provers to the limit? And what does this tell us about the nature of mathematics? Past projects involve the formalisation of the DPRM theorem in Isabelle, and Kimina-Prover, a reinforcement learning system for training LLMs to produce proofs in Lean.