Skip to main content
SpringerLink
Log in

NIL: Learning Nonlinear Interpolants

  • Conference paper
  • First Online:
Automated Deduction – CADE 27 (CADE 2019)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 11716))

Included in the following conference series:

Abstract

Nonlinear interpolants have been shown useful for the verification of programs and hybrid systems in contexts of theorem proving, model checking, abstract interpretation, etc. The underlying synthesis problem, however, is challenging and existing methods have limitations on the form of formulae to be interpolated. We leverage classification techniques with space transformations and kernel tricks as established in the realm of machine learning, and present a counterexample-guided method named NIL for synthesizing polynomial interpolants, thereby yielding a unified framework tackling the interpolation problem for the general quantifier-free theory of nonlinear arithmetic, possibly involving transcendental functions. We prove the soundness of NIL and propose sufficient conditions under which NIL is guaranteed to converge, i.e., the derived sequence of candidate interpolants converges to an actual interpolant, and is complete, namely the algorithm terminates by producing an interpolant if there exists one. The applicability and effectiveness of our technique are demonstrated experimentally on a collection of representative benchmarks from the literature, where in particular, our method suffices to address more interpolation tasks, including those with perturbations in parameters, and in many cases synthesizes simpler interpolants compared with existing approaches.

This work has been supported through grants by NSFC under grant No. 61625206 and 61732001, by the CAS Pioneer Hundred Talents Program under grant No. Y9RC585036, and by the National Science Foundation Award DMS-1217054.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 89.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Available at http://lcs.ios.ac.cn/~chenms/tools/NIL.tar.bz2.

  2. 2.

    As can be also observed at https://github.com/Z3Prover/z3/issues/1765.

References

  1. Bennett, K.P., Bredensteiner, E.J.: Duality and geometry in SVM classifiers. In: ICML 2000, pp. 57–64 (2000)

    Google Scholar 

  2. Bishop, C.M.: Pattern Recognition and Machine Learning, pp. 326–328. Springer, New York (2006)

    MATH  Google Scholar 

  3. Boser, B.E., Guyon, I., Vapnik, V.: A training algorithm for optimal margin classifiers. In: COLT 1992, pp. 144–152 (1992)

    Google Scholar 

  4. Bourbaki, N.: Topological Vector Spaces. Elements of Mathematics. Springer, Heidelberg (1987). https://doi.org/10.1007/978-3-642-61715-7

    Book  MATH  Google Scholar 

  5. Chang, C., Lin, C.: LIBSVM: a library for support vector machines. ACM TIST 2(3), 27:1–27:27 (2011)

    Google Scholar 

  6. Chen, M., Wang, J., An, J., Zhan, B., Kapur, D., Zhan, N.: NIL: learning nonlinear interpolants (full version). http://lcs.ios.ac.cn/~chenms/papers/CADE-27_FULL.pdf

  7. Cimatti, A., Griggio, A., Sebastiani, R.: Efficient interpolant generation in satisfiability modulo theories. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 397–412. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_30

    Chapter  Google Scholar 

  8. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_15

    Chapter  Google Scholar 

  9. Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975). https://doi.org/10.1007/3-540-07407-4_17

    Chapter  Google Scholar 

  10. Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Log. 22(3), 250–268 (1957)

    Article  MathSciNet  Google Scholar 

  11. Dai, L., Xia, B., Zhan, N.: Generating non-linear interpolants by semidefinite programming. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 364–380. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_25

    Chapter  Google Scholar 

  12. Dathathri, S., Arechiga, N., Gao, S., Murray, R.M.: Learning-based abstractions for nonlinear constraint solving. In: IJCAI 2017, pp. 592–599 (2017)

    Google Scholar 

  13. D’Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant strength. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 129–145. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11319-2_12

    Chapter  Google Scholar 

  14. Gan, T., Dai, L., Xia, B., Zhan, N., Kapur, D., Chen, M.: Interpolant synthesis for quadratic polynomial inequalities and combination with EUF. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 195–212. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40229-1_14

    Chapter  Google Scholar 

  15. Gao, S., Zufferey, D.: Interpolants in nonlinear theories over the reals. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 625–641. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_41

    Chapter  MATH  Google Scholar 

  16. Gilbert, S.: A nullstellensatz and a positivstellensatz in semialgebraic geometry. Math. Ann. 207(2), 87–97 (1974)

    Article  MathSciNet  Google Scholar 

  17. Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63166-6_10

    Chapter  Google Scholar 

  18. Gulavani, B.S., Chakraborty, S., Nori, A.V., Rajamani, S.K.: Automatically refining abstract interpretations. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 443–458. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_33

    Chapter  Google Scholar 

  19. Hastie, T., Tibshirani, R., Friedman, J.: The Elements of Statistical Learning: Data Mining, Inference, and Prediction. SSS, 2nd edn. Springer, New York (2009). https://doi.org/10.1007/978-0-387-84858-7

    Book  MATH  Google Scholar 

  20. Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL 2004, pp. 232–244 (2004)

    Google Scholar 

  21. Hong, H., Din, M.S.E.: Variant quantifier elimination. J. Symb. Comput. 47(7), 883–901 (2012)

    Article  MathSciNet  Google Scholar 

  22. Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: ICSE 2010, pp. 215–224 (2010)

    Google Scholar 

  23. Jhala, R., Podelski, A., Rybalchenko, A.: Predicate abstraction for program verification. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 447–491. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-10575-8_15

    Chapter  Google Scholar 

  24. Jung, Y., Lee, W., Wang, B.-Y., Yi, K.: Predicate generation for learning-based quantifier-free loop invariant inference. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 205–219. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19835-9_17

    Chapter  Google Scholar 

  25. Kapur, D., Majumdar, R., Zarba, C.G.: Interpolation for data structures. In: FSE 2006, pp. 105–116 (2006)

    Google Scholar 

  26. Kovács, L., Voronkov, A.: Interpolation and symbol elimination. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 199–213. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02959-2_17

    Chapter  Google Scholar 

  27. Krajíček, J.: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. J. Symb. Log. 62(2), 457–486 (1997)

    Article  MathSciNet  Google Scholar 

  28. Kupferschmid, S., Becker, B.: Craig interpolation in the presence of non-linear constraints. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 240–255. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24310-3_17

    Chapter  MATH  Google Scholar 

  29. Lang, S.: Introduction to Diophantine Approximations: New Expanded Edition. Springer, New York (2012)

    Google Scholar 

  30. McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45069-6_1

    Chapter  Google Scholar 

  31. McMillan, K.L.: An interpolating theorem prover. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 16–30. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24730-2_2

    Chapter  Google Scholar 

  32. McMillan, K.L.: Quantified invariant generation using an interpolating saturation prover. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 413–427. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_31

    Chapter  Google Scholar 

  33. Okudono, T., Nishida, Y., Kojima, K., Suenaga, K., Kido, K., Hasuo, I.: Sharper and simpler nonlinear interpolants for program verification. In: Chang, B.-Y.E. (ed.) APLAS 2017. LNCS, vol. 10695, pp. 491–513. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-71237-6_24

    Chapter  Google Scholar 

  34. Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96(2), 293–320 (2003)

    Article  MathSciNet  Google Scholar 

  35. Pudlák, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symb. Log. 62(3), 981–998 (1997)

    Article  MathSciNet  Google Scholar 

  36. Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 346–362. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-69738-1_25

    Chapter  Google Scholar 

  37. Sharma, R., Nori, A.V., Aiken, A.: Interpolants as classifiers. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 71–87. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_11

    Chapter  Google Scholar 

  38. Sofronie-Stokkermans, V.: Interpolation in local theory extensions. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 235–250. Springer, Heidelberg (2006). https://doi.org/10.1007/11814771_21

    Chapter  Google Scholar 

  39. Sofronie-Stokkermans, V.: On interpolation and symbol elimination in theory extensions. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 273–289. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40229-1_19

    Chapter  Google Scholar 

  40. Solar-Lezama, A., Rabbah, R.M., Bodík, R., Ebcioglu, K.: Programming by sketching for bit-streaming programs. In: PLDI 2005, pp. 281–294 (2005)

    Google Scholar 

  41. Strzeboński, A.W.: Real root isolation for exp-log functions. In: ISSAC 2008, pp. 303–314 (2008)

    Google Scholar 

  42. Strzeboński, A.W.: Real root isolation for tame elementary functions. In: ISSAC 2009, pp. 341–350 (2009)

    Google Scholar 

  43. Strzeboński, A.W.: Cylindrical decomposition for systems transcendental in the first variable. J. Symb. Comput. 46(11), 1284–1290 (2011)

    Article  MathSciNet  Google Scholar 

  44. Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley (1951)

    Book  Google Scholar 

  45. Vladimir, V.: Pattern recognition using generalized portrait method. Autom. Remote Control 24, 774–780 (1963)

    Google Scholar 

  46. Yorsh, G., Musuvathi, M.: A combination method for generating interpolants. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 353–368. Springer, Heidelberg (2005). https://doi.org/10.1007/11532231_26

    Chapter  Google Scholar 

  47. Zhang, J., Feng, Y.: Obtaining exact value by approximate computations. Sci. China Ser. A Math. 50(9), 1361 (2007)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. State Key Laboratory of Computer Science, Institute of Software, CAS, Beijing, China

    Mingshuai Chen, Jian Wang, Bohua Zhan & Naijun Zhan

  2. University of Chinese Academy of Sciences, Beijing, China

    Mingshuai Chen, Jian Wang, Bohua Zhan & Naijun Zhan

  3. School of Software Engineering, Tongji University, Shanghai, China

    Jie An

  4. Department of Computer Science, University of New Mexico, Albuquerque, USA

    Deepak Kapur

Authors
  1. Mingshuai Chen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jian Wang
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jie An
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Bohua Zhan
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Deepak Kapur
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Naijun Zhan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Mingshuai Chen , Bohua Zhan or Naijun Zhan .

Editor information

Editors and Affiliations

  1. University of Lorraine, Villers-lès-Nancy, France

    Pascal Fontaine

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Chen, M., Wang, J., An, J., Zhan, B., Kapur, D., Zhan, N. (2019). NIL: Learning Nonlinear Interpolants. In: Fontaine, P. (eds) Automated Deduction – CADE 27. CADE 2019. Lecture Notes in Computer Science(), vol 11716. Springer, Cham. https://doi.org/10.1007/978-3-030-29436-6_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-29436-6_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-29435-9

  • Online ISBN: 978-3-030-29436-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation