Synthesis, Proofs, and Optimization in Arithmetic Theories

The Hong Kong University of Science and Technology
Department of Computer Science and Engineering


PhD Thesis Defence


Title: "Synthesis, Proofs, and Optimization in Arithmetic Theories"

By

Mr. Hitarth SINGH


Abstract:

The thesis explores the algorithmic and complexity-theoretic challenges in 
automated reasoning over arithmetic theories. The first part addresses 
efficient synthesis of polynomial programs using tools from real-algebraic 
geometry. We apply our techniques to two practical problems: synthesizing 
polynomial-estimates for the execution cost of smart contracts and 
automatically generating polynomial bounds for a class of recurrence systems.

The second part address the efficient proof generation for Satisfiability 
Modulo Theory (SMT) solvers. These solvers are backbone of many 
safety-critical applications, including the synthesis algorithm of the first 
part. However, SMT solvers are huge software and thus prone to bugs. 
Therefore, it is essential to ensure their correctness. We present a novel 
proof format that extends the DRAT proof format for Boolean satisfiability to 
SMT, called eDRAT. These proofs have negligible proof generation overhead and 
enable modular proof checking. We describe the proof checker for two core SMT 
theories: QFLRA and QFUF.

The final part presents a study of the complexity of optimization problem of 
integer linear-exponential programs which extend classical integer linear 
programs with the exponentiation function. The feasibility of such a program 
is decidable and NP- complete. We first introduce a class of arithmetic 
circuit that can efficiently represent the solutions of such programs. We 
describe various procedures for efficient algebraic operations over these 
circuits. The central result of this part is that the optimal solutions of 
such programs have efficient representation of polynomial-size in the input.


Date:                   Thursday, 14 August 2025

Time:                   4:00pm - 6:00pm

Venue:                  Room 5501
                        Lifts 25/26

Chairman:               Dr. Sisi JIAN (CIVL)

Committee Members:      Prof. Fangzhen LIN (Supervisor)
                        Dr. Amir GOHARSHADY (Co-supervisor, Oxford)
                        Dr. Wei WANG
                        Prof. Ke YI
                        Dr. Ke WANG (MATH)
                        Dr. Guillermo A. PÉREZ (UAntwerp)