Why3-py: 用于 Python 中假设检验与元分析的形式化验证工具

Jul 16, 2026

Upload by Hazel

The document addresses the reproducibility crisis by targeting the trustworthiness of statistical analyses, especially meta-analyses that combine results across studies. It proposes a formal verification framework for statistical programs written in Python, where assumptions and interpretations are made explicit. The tool Why3-py converts annotated Python code into WhyML for Why3-based verification, coping with Python’s dynamic typing and runtime polymorphism. It also extends StatWhy to verify meta-analysis methods, helping users detect overlooked assumptions and misuse, and verify program correctness under proper assumptions.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages9

Reading Time23 min

Introduction

Contributions

Related Work

Background

Statistical Hypothesis Testing

arXiv :2607 .0395 1v 1 [ cs . SE] 4 Jul 2026 Why3-py: A Tool for Formal Verification of Hypothesis Testing and Meta-Analysis in Python⋆ Akira Tanaka and Yusuke Kawamoto National Institute of Advanced Industrial Science and Technology (AIST), Tokyo, Japan Abstract. 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. Keywords: Formal method · automated verification · program verification · Why3 · Python · statistical hypothesis testing · meta analysis. 1 Introduction The reproducibility crisis in scientific research has drawn increasing attention to the trustworthiness of statistical analyses, particularly meta-analyses that aggregate evidence from multiple studies. However, the correctness of statistical analyses is fundamentally different from that of conventional programs. Statistical methods crucially rely on assumptions about data-generating processes, such as distributional properties on unobservable true populations, which cannot be verified solely from the program and observed data. As a result, statistical programs may produce seemingly plausible outputs while being based on inappropriate or missing assumptions, leading to incorrect scientific conclusions. This issue is exacerbated in practice by the widespread use of Python and its scientific libraries, which make it easy to apply statistical methods without explicitly stating their assumptions. However, existing program verification techniques focus on functional correctness and do not capture the assumptiondependent nature of statistical reasoning or the usage of external libraries.⋆ The artifact of the paper is available at [https://github.com/fm4stats/why3-py](https://github.com/fm4stats/why3-py). 2 A. Tanaka and Y. Kawamoto To address this gap, we propose a formal verification framework for Python statistical programs, based on explicit specifications of assumptions and interpretations. Specifically, we present Why3-py, a Python front end for the Why3 platform that transforms annotated Python code into WhyML, and an extension of StatWhy for specifying and verifying meta-analysis code. Importantly, our goal is not to verify implementations, but to ensure correct use under appropriate assumptions and interpretations, e.g., detecting incorrect integration of p-values in meta-analysis. Contributions. Our main contributions are summarized as follows: – We present Why3-py, a formal verification tool for Python statistical code. – We extend StatWhy with specifications for meta-analysis methods and show how our approach detects missing assumptions and misuse of meta-analyses. These tools are available with a range of examples and documentation [11, 22] . To the best of our knowledge, this is the first approach to formally verifying Python statistical code. Furthermore, this approach is not limited to specific branch of statistics, but can be applied to any situation where analysts and meta-analysts wish to verify the use of statistical methods in python code. This would be the first

FAQs

Why does the document treat statistical program correctness differently from ordinary program correctness?

Statistical analyses depend on assumptions about data-generating processes and unobservable true populations, which cannot be verified from code and observed data alone. As a result, outputs may look plausible while relying on inappropriate or missing assumptions.

What is Why3-py and what does it do?

Why3-py is a Python front-end for the Why3 verification platform. It transforms annotated Python statistical programs into WhyML representations suitable for formal verification, addressing challenges from Python’s dynamic typing and runtime polymorphism.

How does the framework support verification of meta-analysis methods?

It extends the StatWhy tool with specifications for meta-analysis methods. This enables users to verify correct use under appropriate assumptions and to detect issues such as incorrect integration of p-values in meta-analysis.

Jul 16, 2026

Upload by Hazel