用大模型把Python转成C，用成熟工具验证Python代码并定位错误。
PyVeritas: On Verifying Python via LLM-Based Transpilation and Bounded Model Checking for C
- 用大模型将Python代码转为可验证的C代码，避免手动编译复杂性。
- 在两个基准测试中，转换准确率达80%~90%，支持断言验证与故障定位。
- 适合想用形式化方法验证小型非平凡Python程序的开发者。
Python已成为通用编程主流语言，但缺乏可靠的正式验证工具。相比之下，C语言程序员可利用成熟的模型检测器（如CBMC）进行符号推理与故障定位。由于Python固有的复杂性以及现有编译器（如Cython）的冗长和底层特性，形式化验证在Python中长期受限。本文提出PyVeritas框架，利用大语言模型（LLM）将Python代码高阶转译为C代码，随后在生成的C代码上执行有界模型检测与基于MaxSAT的故障定位。该框架使现有针对C的语言检测工具可用于验证和调试Python程序。在两个Python基准测试上的实证评估表明，基于LLM的转译可达80%~90%的准确率，支持断言驱动验证与可解释的故障诊断，适用于小型但非平凡的Python程序开发环境。
原文摘要 · Abstract (English)
Python has become the dominant language for general-purpose programming, yet it lacks robust tools for formal verification. In contrast, programmers working in languages such as C benefit from mature model checkers, for example CBMC, which enable exhaustive symbolic reasoning and fault localisation. The inherent complexity of Python, coupled with the verbosity and low-level nature of existing transpilers (e.g., Cython), have historically limited the applicability of formal verification to Python programs. In this paper, we propose PyVeritas, a novel framework that leverages Large Language Models (LLMs) for high-level transpilation from Python to C, followed by bounded model checking and MaxSAT-based fault localisation in the generated C code. PyVeritas enables verification and bug localisation for Python code using existing model checking tools for C. Our empirical evaluation on two Python benchmarks demonstrates that LLM-based transpilation can achieve a high degree of accuracy, up to 80--90% for some LLMs, enabling effective development environment that supports assertion-based verification and interpretable fault diagnosis for small yet non-trivial Python programs.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。