Interpolants in Linear Arithmetic: A New Approach
Explore the use of interpolants in linear arithmetic to separate positive and negative examples, with a focus on utilizing state-of-the-art classification algorithms like SVMs for computation. Discover the connection between interpolants and classifiers, as well as their practical applications in proof generation and generalization.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Rahul Sharma Joint work with Aditya Nori (MSR India) and Alex Aiken (Stanford)
If ? ? = then an interpolant ? satisfies: ? ? ? ? = ? contains only the variables common to ? and ? An interpolant is a simple proof Quantifier free formulas in linear arithmetic have quantifier free interpolants.
? = ? ? y ? = ? ? + 1 ? = 2? + 1 2? x
Input: labeled examples Positive examples: ? Negative examples: ? Find ?:???????? {true,false} For all positives, ? ? = true For all negatives, ? ? = false
Interpolant: separates ? from ? Classifier: separates positive examples from negative examples Is there a connection?
Consider the common variables of ? and ?: ? Interpolant ?( ?) if ? = {???(?)}:? ? = true If ? = {???(?)}: ? ? = false ?( ?) separates ? s from ? s
Main result: view interpolants as classifiers ? as positive example ? asnegativeexample Use state-of-the-art classification algorithms (SVMs) for computing interpolants Encouraging empirical results
Unroll the loops Find interpolants Get general proofs (loop invariants) Get positive and negative examples Find a classifier Get a predicate which generalizes
positive examples + + + negative examples + +
Separators Separators Separators Separators + + + + + All separators are good candidates for interpolants
Optimal Margin Classifier + + + +
x = y = 0; while(*) x++; y++; while(x != 0) x--; y--; assert (y == 0); if(x != 0) x--; y--; if(x == 0) assert (y == 0); x = y = 0; if(*) x++; y++; p: ? ?1= 0 ?1= 0 ???(?, ? = ?1+ 1 ? = ?1+ 1, ? = ?1 ? = ?1) ? ???(? = 0, ?2= ? 1 ?2= ? 1, ?2= ? ?2= ?) ?2= 0 ?2 0 ? ? = ? ?,? ? = ?
? ?1= 0 ?1= 0 ???(?, ? = ?1+ 1 ? = ?1+ 1, ? = ?1 ? = ?1) y + (1,1) ? ???(? = 0, ?2= ? 1 ?2= ? 1, ?2= ? ?2= ?) ?2= 0 ?2 0 + x (0,0) ? 2? 2? + 1
Let ? be the common variables of ? and ? Generate ?+ from satisfying assignments of ? Generate ? from satisfying assignments of ? Call SVM with ?+ and ? Return predicate containing ?+
Data is not linearly separable The candidate interpolant is not an interpolant y + + x
For each ? ? ?=SVM( ?+,{?} ) return ? ? y + (1,1) (0,1) Cannot generate linear separators with both and . + x (1,0) (0,0) ? 2? 2? + 1 2? 2? 1
???????????(?,?) Theorem: ???????????(?,?) terminates iff output ? is an interpolant between ? and ? (?+,? ) = ????(?,?) while(true) { ? = ????(?+,? ) Find candidate interpolant if ( ??? ? ? ) ? ? Add ? to ?+and continue; if ( ??? ? ? ) Add ? to ? and continue; ? ? = break; Exit if interpolant found } return ?;
? ?1= 0 ?1= 0 ???(?, ? = ?1+ 1 ? = ?1+ 1, ? = ?1 ? = ?1) y + (1,1) ? ???(? = 0, ?2= ? 1 ?2= ? 1, ?2= ? ?2= ?) ?2= 0 ?2 0 + x (0,0) ?1 2? 2? + 1 ?2 2? 2? + 1 2? 2? 1 Interpolant!
1000 lines of C++ LIBSVM for SVM queries Z3 theorem prover
Interpolants used in tools BLAST, IMPACT Interpolants from proofs Kraj cek[97], Pudl k[97], McMillan[05], Interpolants from constraint solving ARMC, Rybalchenko et al. [07]
Connect interpolants and classifiers A sound interpolation procedure Future work: non-linear interpolants Integrate with a verification tool EUF, arrays, bit-vectors, etc.
