6 papers
Learning to Reason with Insight for Informal Theorem Proving
Yunhe Li, Hao Shi, Bowen Deng +8
Although most of the automated theorem-proving approaches depend on formal proof systems, informal theorem proving can align better with large language models' (LLMs) strength in n…
Efficient Symbolic Execution of Software under Fault Attacks
Yuzhou Fang, Chenyu Zhou, Jingbo Wang +1
We propose a symbolic execution method for analyzing the safety of software under fault attacks both accurately and efficiently. Fault attacks leverage physically injected hardware…
Understanding Formal Reasoning Failures in LLMs as Abstract Interpreters
Jacqueline L. Mitchell, Brian Hyeongseok Kim, Chenyu Zhou +1
Large language models (LLMs) are increasingly used for program verification, and yet little is known about \emph{how} they reason about program semantics during this process. In th…
Large Language Models for Interpretable Mental Health Diagnosis
Brian Hyeongseok Kim, Chao Wang
We propose a clinical decision support system (CDSS) for mental health diagnosis that combines the strengths of large language models (LLMs) and constraint logic programming (CLP).…
An Incremental Algorithm for Algebraic Program Analysis
Chenyu Zhou, Yuzhou Fang, Jingbo Wang +1
We propose a method for conducting algebraic program analysis (APA) incrementally in response to changes of the program under analysis. APA is a program analysis paradigm that cons…
FairQuant: Certifying and Quantifying Fairness of Deep Neural Networks
Brian Hyeongseok Kim, Jingbo Wang, Chao Wang
We propose a method for formally certifying and quantifying individual fairness of deep neural networks (DNN). Individual fairness guarantees that any two individuals who are ident…