aalok thakkar: research

I am pleased to offer the following research projects for motivated undergraduate students. These projects provide an excellent opportunity to gain hands-on research experience, develop new skills, and make meaningful contributions to the field of computer science:

expressive query synthesis: This line of work aims to extend my previous work on example-guided synthesis of relational queries to handle expressive aggregation functions (such as SUM, AVG, COUNT, MIN, MAX) which are essential for querying real world databases. The core challenge is to infer user intent from a small set of input-output examples and not require additional supervision. If interested, please read this paper as a starting point.

synthesis via constraint solving: In this paper , I have proved that the query synthesis problem (and its versions) can be modelled as a quantified boolean formula and can be solved using QBF solvers. This project focuses on implementing this hypothesis, and benchmarking the performance of constraint solving methods over enumerative search techniques.

combination and maximal syntheis: We aim to develop an exact and an approximate algorithm for synthesis of programs where: (i) the correctness specification is provided in multiple specification languages and (ii) the objective is to satisfy the maximum number of specifications.

reasoning in AI: A starting point in this direction is to develop an automated solver for knights and knaves puzzles. We create a system where Large Language Models (LLMs) translate puzzles into propositional logic constraints, which are then solved using Z3, a theorem prover. This project demonstrates practical applications of logical reasoning in AI. Symbolic Logic (CS-2160/2260) is a prerequisite for this project, which I will be teaching in the Monsoon 2024 semester.

poetry generation: Despite their impressive text generation capabilities, LLMs face challenges in consistently maintaining syntactic requirements such as word and syllable counts and positional constraints. An undergraduate project in this direction can develop and test methods for improving LLMs' ability to generate structurally sound poetry. A starting point for this topic is the paper Verse by Verse and its accompanying tool.

modelling cultural responses : In partnership with Ashoka's Center for People-centric Energy Transition, we want to explore how LLMs can model cultural responses to energy transitions (say for example firewood to gas). This project is more empirical and does not require a strong CS background.

learning technologies: This project focuses on developing a course-specific AI tutor using LLMs for undergraduate computer science courses. The primary objectives are to fine-tune an open-source LLM on course materials, implement effective prompt engineering techniques, and design interaction patterns that promote learning. Key technical challenges include domain-specific knowledge integration, handling code-related queries, and balancing hint generation with direct answer avoidance. The project will explore techniques such as retrieval-augmented generation, few-shot learning, and constrained decoding to create an AI assistant that accurately explains concepts, provides guided hints, and answers course-related questions while adhering to pedagogical principles.

automated verification: I am also interested in automated verification of three critical Indian systems: UPI (Unified Payments Interface), EVMs (Electronic Voting Machines), and Aadhaar (the national biometric ID system). The goal is to develop formal methods and tools to rigorously verify the correctness, security, and privacy properties of these systems to enhance public trust, identify potential vulnerabilities, and contribute to the overall reliability of India's digital infrastructure.

other: I am interested in theoretical computer science at large, including topics such as automata theory, formal language theory, formal methods, logic, and programming languages, particularly in their applications to program synthesis, automated verification, and artificial intelligence. Contact me if you would like to pursue a project in these areas.