Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

DAInfer+: Neurosymbolic Inference of API Specifications from Documentation via Embedding Models

Maryam Masoudian, Anshunkang Zhou, Chengpeng Wang, Charles Zhang

Abstract

Modern software systems heavily rely on various libraries, which require understanding the API semantics in static analysis. However, summarizing API semantics remains challenging due to complex implementations or unavailable library code. This paper presents DAInfer+, a novel approach for inferring API specifications from library documentation. We employ Natural Language Processing (NLP) to interpret informal semantic information provided by the documentation, which enables us to reduce the specification inference to an optimization problem. Specifically, we investigate the effectiveness of sentence embedding models and Large Language Models (LLMs) in deriving memory operation abstractions from API descriptions. These abstractions are used to retrieve data-flow and aliasing relations to generate comprehensive API specifications. To solve the optimization problem efficiently, we propose neurosymbolic optimization, yielding precise data-flow and aliasing specifications. Our evaluation of popular Java libraries shows that zero-shot sentence embedding models outperform few-shot prompted LLMs in robustness, capturing fine-grained semantic nuances more effectively. While our initial attempts using two-stage LLM prompting yielded promising results, we found that the embedding-based approach proved superior. Specifically, these models achieve over 82% recall and 85% precision for data-flow inference and 88% recall and 79% precision for alias relations, all within seconds. These results demonstrate the practical value of DAInfer+ in library-aware static analysis.

DAInfer+: Neurosymbolic Inference of API Specifications from Documentation via Embedding Models

Abstract

Modern software systems heavily rely on various libraries, which require understanding the API semantics in static analysis. However, summarizing API semantics remains challenging due to complex implementations or unavailable library code. This paper presents DAInfer+, a novel approach for inferring API specifications from library documentation. We employ Natural Language Processing (NLP) to interpret informal semantic information provided by the documentation, which enables us to reduce the specification inference to an optimization problem. Specifically, we investigate the effectiveness of sentence embedding models and Large Language Models (LLMs) in deriving memory operation abstractions from API descriptions. These abstractions are used to retrieve data-flow and aliasing relations to generate comprehensive API specifications. To solve the optimization problem efficiently, we propose neurosymbolic optimization, yielding precise data-flow and aliasing specifications. Our evaluation of popular Java libraries shows that zero-shot sentence embedding models outperform few-shot prompted LLMs in robustness, capturing fine-grained semantic nuances more effectively. While our initial attempts using two-stage LLM prompting yielded promising results, we found that the embedding-based approach proved superior. Specifically, these models achieve over 82% recall and 85% precision for data-flow inference and 88% recall and 79% precision for alias relations, all within seconds. These results demonstrate the practical value of DAInfer+ in library-aware static analysis.

Paper Structure

This paper contains 30 sections, 6 equations, 16 figures, 3 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Background and Overview
  3. Library-Aware Data-Flow and Alias Analysis
  4. Different Perspectives of Inferring API Specifications
  5. Overview of DAInfer+
  6. Problem Formulation
  7. Documentation Model
  8. API Aliasing Specification
  9. Problem Statement
  10. Documentation Model Abstraction
  11. API Value Graph
  12. Label Abstraction
  13. Problem Reduction
  14. Specification Inference via Neurosymbolic Optimization
  15. Overall Algorithm
  16. ...and 15 more sections

Figures (16)

  • Figure 1: Examples of library documentation. We use $m_i$ to denote the API with the ID $i$ in the paper.
  • Figure 2: Workflow of DAInfer+
  • Figure 3: The API value graph of the documentation model induced by the documentation in Figure \ref{['fig:javadoc']}
  • Figure 4: An optimal solution to the problem instance over the API value graph shown in Figure \ref{['fig:graph']}
  • Figure 5: The prompt templates of two-staged prompting
  • ...and 11 more figures

Theorems & Definitions (29)

  • Example 1
  • Example 2
  • Definition 1
  • Example 3
  • Definition 2
  • Example 4
  • Definition 3: API Value Graph
  • Example 5
  • Definition 4
  • Example 6
  • ...and 19 more