用形式化验证确保统计分析代码正确，防止误用假设。
Why3-py: A Tool for Formal Verification of Hypothesis Testing and Meta-Analysis in Python
- 将Python代码转为可验证的WhyML格式，支持动态类型与多态。
- 发现并验证假设检验与元分析中的隐含假设错误。
- 适合科研人员和数据分析师提升研究可复现性。
科学研究所面临的可复现性危机已广受关注，元分析在整合多个研究的统计结果方面愈发重要。然而，统计方法常存在模糊且未明示的底层假设，易导致误用与误读。为此，我们提出一种针对Python编写统计程序的形式化验证框架。具体而言，本文介绍了Why3-py，即为何3平台的Python前端，可将Python程序转换为适用于形式化验证的、面向验证的WhyML表示，解决了Python动态类型与运行时多态带来的挑战。同时，我们扩展了StatWhy工具，以支持元分析方法的验证。这些工具使用户能够识别被忽略的假设，发现分析误用，并验证假设检验与元分析代码的正确性。
原文摘要 · Abstract (English)
The reproducibility crisis in scientific research has received widespread recognition, thereby increasing the importance of meta-analyses that integrate statistical analyses from multiple studies. However, statistical methods often have ambiguous and implicit underlying assumptions, which can lead to their erroneous applications and interpretations. To address this issue, we propose a formal verification framework for statistical programs written in Python. Specifically, we present Why3-py, a Python front-end for the Why3 verification platform that transforms Python programs into verification-oriented WhyML representations suitable for formal verification, addressing the challenges arising from Python's dynamic typing and runtime polymorphism. Furthermore, we extend the StatWhy tool to support the verification of meta-analysis methods. These tools enable users to identify overlooked assumptions and misuse of analyses, and to verify the correctness of Python programs for hypothesis testing and for meta-analyses.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。