Barış Bayazıt

About À propos

I'm a third-year undergraduate student at the University of Toronto in the computer science specialist program, graduating in 2027. I'm lucky to be supervised by Prof. Xujie Si in the Department of Computer Science in the Programming Languages and Software Engineering group. Broadly speaking, my research interests include programming languages, formal verification, and applications of machine learning in adjacent areas. Fun fact: I listen to all types of music! My playlists have over 4,500 different songs in total. I also love learning foreign languages and have an 800+ day Duolingo streak.

Je suis étudiant de troisième année au premier cycle à l'Université de Toronto dans le programme spécialisé en informatique, et je terminerai mes études en 2027. J'ai la chance d'être supervisé par Prof. Xujie Si au Department of Computer Science, au sein du Programming Languages and Software Engineering Group. De façon générale, mes intérêts de recherche comprennent les langages de programmation, la vérification formelle et les applications de l'apprentissage automatique dans les domaines connexes. Fait amusant : j'écoute tous les styles de musique, et mes listes de lecture comptent plus de 4 500 chansons différentes. J'adore aussi apprendre des langues étrangères et j'ai une série de plus de 800 jours sur Duolingo.

Research Recherche

• A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants

  PDF / ACM Digital Library · LMPL @ ICFP/SPLASH 2025

  How well can LLMs write Rocq Prover (formerly Coq) proofs? What context do they need? Published at the LMPL Workshop at ICFP/SPLASH 2025. Special thanks to PAC (ACM SIGPLAN) and the Dr. Roseann Runte Award (Victoria College) for allowing me to present this work in person!

  Barış Bayazıt, Yao Li, and Xujie Si. 2025. A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants. In Proceedings of the 1st ACM SIGPLAN International Workshop on Language Models and Programming Languages (LMPL '25), October 12-18, 2025, Singapore, Singapore. ACM, New York, NY, USA, 15 pages. DOI: 10.1145/3759425.3763391.
• VerifyThisBench: Generating Code, Specifications, and Proofs All at Once

  Preprint (arXiv) · VerifyThis-Verus · VerifyThis competition

  Can LLMs write the code, the specification, and the proof that their code is correct, all at the same time? In this joint work, I created VerifyThis-Verus, implementations of past VerifyThis competition challenges in Rust and Verus to be used as ground truth. This work is currently under review.

  Deng, X., Zhong, S., Bayazıt, B., Veneris, A., Long, F., and Si, X. 2025. VerifyThisBench: Generating Code, Specifications, and Proofs All at Once. arXiv:2505.19271 [cs.SE].

• RESpecBench: Evaluation of Specification Generation with Automated Verification

  Preprint (PDF)

  Most benchmarks on LLMs evaluate the model's answers using tests. However, testing provides no formal guarantees. How can we establish semantic equivalence between the specification generated by the LLM from natural language and the oracle specification? This work is currently under review.

  • Best Poster Award, Department of Computer Science Summer Undergraduate Poster Session.

• A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants

  PDF / Bibliothèque numérique ACM · LMPL @ ICFP/SPLASH 2025

  Dans quelle mesure les MLL peuvent-elles écrire des preuves Rocq Prover (anciennement Coq) et de quel contexte ont-elles besoin ? Ce travail a été présenté à l'atelier LMPL lors d'ICFP/SPLASH 2025. Merci à PAC (ACM SIGPLAN) et au Dr. Roseann Runte Award (Victoria College) qui m'ont permis de présenter ce projet en personne !

  Barış Bayazıt, Yao Li et Xujie Si. 2025. A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants. Actes du 1er ACM SIGPLAN International Workshop on Language Models and Programming Languages (LMPL '25), 12-18 octobre 2025, Singapour. ACM, New York, NY, USA, 15 pages. DOI : 10.1145/3759425.3763391.
• VerifyThisBench: Generating Code, Specifications, and Proofs All at Once

  Prépublication (arXiv) · VerifyThis-Verus · Compétition VerifyThis

  Les MLL peuvent-elles écrire simultanément le code, la spécification et la preuve que ce code est correct ? Dans ce travail collaboratif, j'ai créé VerifyThis-Verus : des implémentations en Rust et Verus des défis VerifyThis pour servir de référence. L'article est actuellement en cours d'évaluation.

  Deng, X., Zhong, S., Bayazıt, B., Veneris, A., Long, F., et Si, X. 2025. VerifyThisBench: Generating Code, Specifications, and Proofs All at Once. arXiv:2505.19271 [cs.SE].

• RESpecBench: Evaluation of Specification Generation with Automated Verification

  Prépublication (PDF)

  La plupart des bancs d'essai pour les MLL évaluent les réponses à l'aide de tests, qui n'offrent toutefois aucune garantie formelle. Comment établir l'équivalence sémantique entre la spécification produite par le modèle et la spécification oracle ? Ce projet est actuellement en cours de révision.

  • Prix de la meilleure affiche, Session d'affiches estivale des étudiant·e·s de premier cycle du Department of Computer Science.

Contact me Contact

I always reply to my emails! If you're interested in working on a project, feel free to get in touch.

Je réponds toujours à mes courriels ! Si un projet vous intéresse, n'hésitez pas à me contacter.