ML4PG in Computer Algebra verification
ML4PG is a machine-learning extension that provides statistical proof hints during the process of Coq/SSReflect proof development. In this paper, we use ML4PG to find proof patterns in the CoqEAL library -- a library that was devised to verify the correctness of Computer Algebra algorithms. In particular, we use ML4PG to help us in the formalisation of an efficient algorithm to compute the inverse of triangular matrices.
Code (0)
등록된 구현이 없습니다.
Tasks
BIG-bench Machine LearningSimilar Papers 제목 키워드 기반
Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down
The coincidence between initial algebras (IAs) and final coalgebras (FCs) is a phenomenon that underpins various important results in theoretical computer science. In this paper, we identify a general fibrational conditi…
More Efficient Identifiability Verification in ODE Models by Reducing Non-Identifiability
Structural global parameter identifiability indicates whether one can determine a parameter's value from given inputs and outputs in the absence of noise. If a given model has parameters for which there may be infinitely…
Voltage-Controlled Oscillator and Memristor-Based Analog Computing for Solving Systems of Linear Equations
Matrix computations have become increasingly significant in many data-driven applications. However, Moores law for digital computers has been gradually approaching its limit in recent years. Moreover, digital computers e…
O-Forge: An LLM + Computer Algebra Framework for Asymptotic Analysis
Large language models have recently demonstrated advanced capabilities in solving IMO and Putnam problems; yet their role in research mathematics has remained fairly limited. The key difficulty is verification: suggested…
ReVEAL: GNN-Guided Reverse Engineering for Formal Verification of Optimized Multipliers
We present ReVEAL, a graph-learning-based method for reverse engineering of multiplier architectures to improve algebraic circuit verification techniques. Our framework leverages structural graph features and learning-dr…