Talks

Making AI Reasoning and Actions More Reliable with SMT and Lean

[Online] AI Horizons · NUS Artificial Intelligence Institute

Hosted by Dr Dianbo Liu, National University of Singapore

Language models give convincing answers, but how do we check that their reasoning is correct? The talk follows one question from natural language to a solver-checked result: translating claims into logical constraints that SMT solvers such as Z3 can check, using solver feedback to revise answers, and detecting when the translation itself is wrong. It closes with Lean-verified policy checkers that evaluate an agent’s tool calls before they execute.

@misc{singh2026reliableaitalk,
  title={Making {AI} Reasoning and Actions More Reliable with {SMT} and {Lean}},
  author={Vikash Singh},
  howpublished={Invited talk, AI Horizons series, NUS Artificial Intelligence Institute (online)},
  month=oct,
  year={2026},
  note={Slides},
  url={https://vikash-singh.me/talks/formal-verification-reliable-ai}
}

Reinforcement Learning with Verifiable Rewards

Case Western Reserve University

A first-principles tour of reinforcement learning with verifiable rewards (RLVR): how a task checker turns sampled attempts into a training signal, and how SFT, DPO, PPO and GRPO differ in what drives each update. It then covers later refinements (RLOO, Dr. GRPO, DAPO, GSPO), process rewards and richer feedback, and what improvement these methods actually measure.

@misc{singh2026rlvrtalk,
  title={Reinforcement Learning with Verifiable Rewards},
  author={Vikash Singh},
  howpublished={Talk, Case Western Reserve University},
  year={2026},
  note={Slides},
  url={https://vikash-singh.me/talks/rl-verifiable-rewards}
}