Implementation and Synthesis of Math Library Functions
summary
A domain specific language called MegaLibm implements, tests, and tunes exp sin log etc by embedding semantic types and semantic wellformedness checks that call out to tools like Sollya and type-directed synthesis, compiling down to C and running in Jupyter for interactive tuning. The system reproduces 8 implementations with comparable speed and accuracy, synthesizes 5 faster/more accurate variations and 3 from‑scratch implementations, supports range reduction, Horner/Estrin tradeoffs, and catches real bugs in existing libs.
AI-written summary · about
chapters (6)
- 0:00The challenges of math libs
- 2:55The motivation for MegaLibm
- 5:15The core design of MegaLibm
- 8:48Advanced range reduction
- 11:23Compilation and workflow
- 15:16Q&A session
related talks
22mThe Lean Mathematical Library
53mSemantics-based program manipulation in the age of LLMs
42mProgramming with Math
26mGenerating Correctly Rounded Math Libraries for New Floating Point Variants
45mLogic Meta Programming for Functional Languages
30mAnalyzing Programs with SMT Solvers
15mFormulog: Datalog for SMT-Based Static Analysis
19mA General Library of Legal Components