Plotting in a Formally Verified Way
Guillaume Melquiond

TL;DR
This paper explores formal verification of function plots to ensure correctness, utilizing Coq proof assistant and polynomial approximations within the CoqInterval library to improve reliability.
Contribution
It introduces a method to formally verify the correctness of plots in computer algebra systems using Coq and polynomial approximations.
Findings
Verified plotting ensures accurate visual representations
Integration of formal methods into plotting libraries
Enhanced reliability of mathematical function visualizations
Abstract
An invaluable feature of computer algebra systems is their ability to plot the graph of functions. Unfortunately, when one is trying to design a library of mathematical functions, this feature often falls short, producing incorrect and potentially misleading plots, due to accuracy issues inherent to this use case. This paper investigates what it means for a plot to be correct and how to formally verify this property. The Coq proof assistant is then turned into a tool for plotting function graphs using reliable polynomial approximations. This feature is provided as part of the CoqInterval library.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
