Why3-py: A Tool for Formal Verification of Hypothesis Testing and Meta-Analysis in Python

• URL: http://arxiv.org/abs/2607.03951v1
• Date: Sat, 04 Jul 2026 16:53:39 GMT
• Title: Why3-py: A Tool for Formal Verification of Hypothesis Testing and Meta-Analysis in Python
• Abstract summary: We propose a formal verification framework for statistical programs written in Python.<n>We present Why3-py, a Python front-end for the Why3 verification platform.<n>We extend the StatWhy tool to support the verification of meta-analysis methods.
• Score: 0.47267770920095525
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• PyVeritas: On Verifying Python via LLM-Based Transpilation and Bounded Model Checking for C [18.52519530244078]
  Python has become the dominant language for general-purpose programming, yet it lacks robust tools for formal verification.<n>We propose PyVeritas, a novel framework that leverages Large Language Models (LLMs) for high-level transpilation from Python to C.
  arXiv  Detail & Related papers  (2025-08-11T16:49:07Z)
• Examining False Positives under Inference Scaling for Mathematical Reasoning [83.97128486951999]
  We systematically examine the prevalence of false positive solutions in mathematical problem solving for language models.<n>Our experimental results reveal that: (1) false positive solutions persist across different models, datasets, and decoding methods, (2) sampling-based inference time scaling methods do not alleviate the problem, and (3) the pass@N evaluation metric is more susceptible to false positives.
  arXiv  Detail & Related papers  (2025-02-10T07:49:35Z)
• PyPulse: A Python Library for Biosignal Imputation [58.35269251730328]
  We introduce PyPulse, a Python package for imputation of biosignals in both clinical and wearable sensor settings.<n>PyPulse's framework provides a modular and extendable framework with high ease-of-use for a broad userbase, including non-machine-learning bioresearchers.<n>We released PyPulse under the MIT License on Github and PyPI.
  arXiv  Detail & Related papers  (2024-12-09T11:00:55Z)
• RobPy: a Python Package for Robust Statistical Methods [1.2233362977312945]
  RobPy offers a wide range of robust methods in Python, built upon established libraries including NumPy, SciPy, and scikit-learn. This paper presents the structure of the RobPy package, demonstrates its functionality through examples, and compares its features to existing implementations in other statistical software.
  arXiv  Detail & Related papers  (2024-11-04T10:27:30Z)
• PoTo: A Hybrid Andersen's Points-to Analysis for Python [3.6793233203143743]
  PoTo is an Andersen-style context-insensitive and flow-insensitive points-to analysis for Python. PoTo+ is a static type inference for Python built on the points-to analysis.
  arXiv  Detail & Related papers  (2024-09-05T21:26:25Z)
• StatWhy: Formal Verification Tool for Statistical Hypothesis Testing Programs [0.9886108751871757]
  We propose a tool-assisted method for formally specifying and automatically verifying the correctness of statistical programs.<n> programmers are required to annotate the source code of the statistical programs with the requirements for these methods.<n>Our software tool StatWhy automatically checks whether programmers have properly specified the requirements for the statistical methods.
  arXiv  Detail & Related papers  (2024-05-25T05:07:33Z)
• FauxPy: A Fault Localization Tool for Python [4.366130138560774]
  FauxPy is a fault localization tool for Python programs. The paper showcases how to use FauxPy on two illustrative examples, and then discusses its main features and capabilities from a user's perspective.
  arXiv  Detail & Related papers  (2024-04-29T11:11:26Z)
• Scikit-dimension: a Python package for intrinsic dimension estimation [58.8599521537]
  This technical note introduces textttscikit-dimension, an open-source Python package for intrinsic dimension estimation. textttscikit-dimension package provides a uniform implementation of most of the known ID estimators based on scikit-learn application programming interface. We briefly describe the package and demonstrate its use in a large-scale (more than 500 datasets) benchmarking of methods for ID estimation in real-life and synthetic data.
  arXiv  Detail & Related papers  (2021-09-06T16:46:38Z)
• QuaPy: A Python-Based Framework for Quantification [76.22817970624875]
  QuaPy is an open-source framework for performing quantification (a.k.a. supervised prevalence estimation) It is written in Python and can be installed via pip.
  arXiv  Detail & Related papers  (2021-06-18T13:57:11Z)
• DoWhy: An End-to-End Library for Causal Inference [16.764873959182765]
  We describe DoWhy, an open-source Python library that is built with causal assumptions as its first-class citizens. DoWhy presents an API for the four steps common to any causal analysis. In particular, DoWhy implements a number of checks including placebo tests, bootstrap tests, and tests for unoberved confounding.
  arXiv  Detail & Related papers  (2020-11-09T06:22:11Z)
• GO FIGURE: A Meta Evaluation of Factuality in Summarization [131.1087461486504]
  We introduce GO FIGURE, a meta-evaluation framework for evaluating factuality evaluation metrics. Our benchmark analysis on ten factuality metrics reveals that our framework provides a robust and efficient evaluation. It also reveals that while QA metrics generally improve over standard metrics that measure factuality across domains, performance is highly dependent on the way in which questions are generated.
  arXiv  Detail & Related papers  (2020-10-24T08:30:20Z)
• Meta-Learned Confidence for Few-shot Learning [60.6086305523402]
  A popular transductive inference technique for few-shot metric-based approaches, is to update the prototype of each class with the mean of the most confident query examples. We propose to meta-learn the confidence for each query sample, to assign optimal weights to unlabeled queries. We validate our few-shot learning model with meta-learned confidence on four benchmark datasets.
  arXiv  Detail & Related papers  (2020-02-27T10:22:17Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.