一句话：用 Z3 约束求解替代纯 LLM 版本猜测，仅对缺失元数据选择性调用 LLM，将 Python 依赖解析成功率从 54.8% 提升至 83.6%。
依赖解析即挑选一组可无冲突共存的包版本，是现代软件项目构建失败的重要来源；在 Python 生态中，Python 2/3 不兼容、包废弃以及元数据普遍缺失使该问题尤为棘手。已有的 PLLM 方案完全依赖大语言模型从代码中推断 Python 与包版本，并依据构建错误反复修复，代价高且准确性有限。本文提出 SMT-LLM，一个以形式化约束求解取代纯 LLM 猜测的混合系统：它通过 AST 分析确定性地提取 import 并检测 Python 版本，用 vermin 推断最低 Python 版本，并采用五层 import-to-package 解析器在任何 LLM 调用之前先查询 PyPI；随后基于 PyPI 元数据与（仅对元数据缺失包进行的）LLM 填补依赖构建约束图，交由 Z3 SMT 求解器求出一致的版本赋值。在 HG2.9K 基准上使用 Gemma2:9B（10 GB 显存）评测，SMT-LLM 解析成功率达 83.6%，而 PLLM 为 54.8%；中位解析时间由 151.5 秒降至 23.9 秒（快 6.3 倍），每片段平均 LLM 调用从约 24.9 次降至 2.26 次（减少 11 倍）。
Dependency resolution is the task of selecting package versions that can be installed together without conflicts. It accounts for a significant share of build failures in modern software projects. In the Python ecosystem, this task is especially challenging due to Python 2/3 incompatibilities, deprecated packages, and widespread missing metadata. Recent work, such as PLLM, tackles this problem by using large language models (LLMs) to infer Python and package versions from code and iteratively repairing them based on build errors. We present SMT-LLM, a hybrid system that replaces LLM-only version guessing with formal constraint solving. SMT-LLM uses deterministic import extraction and Python version detection via abstract syntax tree (AST) analysis, the vermin tool to infer minimum Python versions, and a five-tier import-to-package resolver that queries PyPI before any LLM call. We construct a constraint graph from PyPI metadata and LLM-imputed dependencies for packages with missing metadata, then solve for consistent version assignments using a Z3 satisfiability modulo theories (SMT) solver. On the HG2.9K benchmark using Gemma2:9B (10 GB VRAM), SMT-LLM resolves 83.6% of snippets compared to PLLM's 54.8%, while reducing median resolution time from 151.5 s to 23.9 s (6.3× faster) and average LLM calls from ~24.9 to 2.26 per snippet (11× reduction).
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{abs-2605-11772,
title = {Breaking the Dependency Chaos: A Constraint-Driven Python Dependency Resolution Strategy with Selective LLM Imputation},
author = {Kowshik Chowdhury and Dipayan Banik and Shazibul Islam Shamim},
booktitle = {FSE},
year = {2026},
doi = {10.1145/3803437.3808241}
}