A library of Taylor models for PVS automatic proof checker

Francisco Cháves; Marc Daumas

Home/Archive/arXiv

arXiv · cs/0602005

A library of Taylor models for PVS automatic proof checker

Francisco Cháves·Marc Daumas

View original source ↗Read source document ↗Export metadata ↓

Abstract

We present in this paper a library to compute with Taylor models, a technique extending interval arithmetic to reduce decorrelation and to solve differential equations. Numerical software usually produces only numerical results. Our library can be used to produce both results and proofs. As seen during the development of Fermat's last theorem reported by Aczel 1996, providing a proof is not sufficient. Our library provides a proof that has been thoroughly scrutinized by a trustworthy and tireless assistant. PVS is an automatic proof assistant that has been fairly developed and used and that has no internal connection with interval arithmetic or Taylor models. We built our library so that PVS validates each result as it is produced. As producing and validating a proof, is and will certainly remain a bigger task than just producing a numerical result our library will never be a replacement to imperative implementations of Taylor models such as Cosy Infinity. Our library should mainly be used to validate small to medium size results that are involved in safety or life critical applications.

Explore related subjects

cs.MS

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Francisco Cháves, Marc Daumas. 2006-02-03. A library of Taylor models for PVS automatic proof checker. https://arxiv.org/abs/cs/0602005

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Extensible Programmatic Specification of Finite Element Methods

Finite element methods (FEMs) are a powerful and ubiquitous tool for solving engineering problems. Experimenting with different finite elements can improve the quality and efficiency of solutions. In some cases, the wrong (but nonetheless most common) choice of finite element will produce solutions which converge to the wrong answer regardless of mesh resolution. However, in practice, the choice of finite element is not explored due to the complexity of re-deriving and re-implementing finite element methods. Trying a new finite element is challenging because practitioners must manually deduce formulas to use these elements and implement them within a potentially complex system. We address this problem by introducing ElementForge, a finite element system that is parametric over the literate mathematical specification of a finite element in a domain-specific language (DSL). The ElementForge compiler reasons about tensor spaces, tensors, and tensor bases from first principles to derive implementations of finite elements. The ElementForge compiler is able to automatically derive implementations of finite elements previously only derived by hand. Further, ElementForge minimally couples several key mathematical concepts, mainly tensor fields, mesh topologies, sparse tensors, and assembled finite element operators, to produce a complete finite element system that is parametric over the choice of element. Consequently, the elements derived by the compiler can be applied parametrically to new meshes, PDEs, and boundary conditions. We evaluate our system by implementing several simulations with different finite elements, demonstrating that our system can explore tradeoffs in generality, accuracy, speed, and representational complexity. For example, we are able to implement the Morley, Bell, Argyris, and Hermite like elements with less than 50 lines of code and use them all in a single simulation.

cs.MS↗

arXiv2026

Streaming Right Multiplication over Grammar-Compressed Matrices: A Memory-Bounded GPU Engine for Genotype and Graph Data

Grammar-compressed matrices store a matrix's non-zero structure as a RePair straight-line program (SLP), supporting matrix-vector products in time and space proportional to the compressed size. We target the regime where this is decisive on a GPU: when the uncompressed matrix exceeds device memory, so footprint (not floating-point throughput) is the binding constraint. Our SLP is a directed acyclic graph (DAG) of out-degree 2, and the right product $y=Mx$ is a single bottom-up sweep (leaves to roots): a conflict-free gather. We make the grammar properly layered (every nonterminal child one level below its parent) via pass-through completion, which inserts identity nodes to carry values upward until consumed. This yields a streaming evaluation in which each level reads only the level below and writes the next, so the live set fits in two alternating read-only/write-only buffers instead of scaling with the whole grammar. On genotype matrices, where a polygenic score is exactly the right product $y=Gβ$, a CUDA implementation shows a clear space advantage: a device footprint 3.5 to 8 times smaller than a materialized cuSPARSE CSR baseline, single-vector times within a small factor of cuSPARSE, and consistently lower GPU energy. Because the sweep needs only an associative and commutative combine, the same engine evaluates any homomorphism into a commutative monoid over the grammar by swapping a small leaf/combine/emit policy; the same reachability sweep scales to a billion-edge Software Heritage graph (261 TB dense, 21 times smaller serialized than cuSPARSE's CSR). We frame this as an algorithm-engineering case study: structural metrics (depth, live-set width, completion cost) are measured, architecture-independent grammar properties, whereas time and energy are profiled on a single board.

cs.MS↗

arXiv2026

The Rise of Low Precision Floating Point

Floating point computing has dominated scientific computations since the 1950s because of its versatile ability to approximate real numbers with both sufficiently high precision and sufficiently great range. Since 1985, two specific formats have become standard across the industry, one with 32 bits which is adequate for many purposes and one with 64 bits which allows numbers with both much higher precision and much greater range for applications where these are needed. However, during the past decade, deep learning has come to dominate computation, and narrower floating point formats with lower precision and reduced range have steadily become more common. In this article we discuss this phenomenon, why it is happening, how various 16-bit, 8-bit and even 4-bit floating point formats have been developed, and efforts to standardize these formats.

cs.MS↗