[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Transforming Optimization Problems into Disciplined Convex Programming Form

  • Conference paper
  • First Online:
Intelligent Computer Mathematics (CICM 2024)

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

Included in the following conference series:

  • 326 Accesses

Abstract

Disciplined convex programming (Dcp) is a popular framework for systematically reducing convex optimization problems to the low-level conic form commonly used by convex solvers. An arbitrary convex problem may not immediately be in a Dcp-compliant form, and several manual and error-prone steps are often needed to transform it into an equivalent form that is accepted by Dcp frameworks. We automate this process in CvxLean, a convex optimization modeling framework embedded in the Lean theorem prover. While the steps can be described using rewrite rules, there are not clear heuristics for orienting and applying them. Instead, we carry out an efficient breadth-first search for a suitable sequence of steps by making use of the egg e-graph-based term rewriting system. When egg finds a suitable sequence, we automatically prove it correct in Lean. This procedure is the first generic, proof-producing approach to transform a wide range of optimization problems into Dcp-compliant forms. Moreover, it is an important step towards a fully-verified and user-friendly convex programming environment.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    https://github.com/verified-optimization/CvxLean/.

  2. 2.

    https://leanprover.github.io/theorem_proving_in_lean4/conv.html.

  3. 3.

    Here, “X or better” means “X or any element below X in the relevant order”.

  4. 4.

    We use a def rather than lemma declaration here for constructive type-theoretic reasons; it enables us to extract from equivalence proofs functions for mapping solutions to initial problem domains.

References

  1. Agrawal, A., Boyd, S.: Disciplined quasiconvex programming. Optim. Lett. 14, 1643–1657 (2020). https://doi.org/10.1007/s11590-020-01561-8

    Article  MathSciNet  Google Scholar 

  2. Agrawal, A., Diamond, S., Boyd, S.: Disciplined geometric programming. Optim. Lett. 13, 961–976 (2019). https://doi.org/10.1007/s11590-019-01422-z

    Article  MathSciNet  Google Scholar 

  3. Andersen, E.D., Andersen, K.D.: The MOSEK interior point optimizer for linear programming: an implementation of the homogeneous algorithm. In: Frenk, H., Roos, K., Terlaky, T., Zhang, S. (eds.) High Performance Optimization, pp. 197–232. Springer, Heidelberg (2000). https://doi.org/10.1007/978-1-4757-3216-0_8

  4. Bentkamp, A., Fernández Mir, R., Avigad, J.: Verified reductions for optimization. In: Sankaranarayanan, S., Sharygina, N. (eds.) International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 74–92. Springer, Heidelberg (2023). https://doi.org/10.1007/978-3-031-30820-8_8

  5. Boyd, S.P., Vandenberghe, L.: Convex Optimization. Cambridge University Press, Cambridge (2004). https://doi.org/10.1017/CBO9780511804441

    Book  Google Scholar 

  6. Mathlib Community, T.: The Lean mathematical library. In: CPP 2020, pp. 367–381. Association for Computing Machinery, New York (2020). https://doi.org/10.1145/3372885.3373824

  7. De Moura, L., Bjørner, N.: Efficient e-matching for SMT solvers. In: Pfenning, F. (ed.) Automated Deduction–CADE-21: 21st International Conference on Automated Deduction, Bremen, Germany, 17–20 July 2007, Proceedings 21, pp. 183–198. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73595-3_13

  8. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  9. Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM (JACM) 52(3), 365–473 (2005). https://doi.org/10.1145/1066100.1066102

    Article  MathSciNet  Google Scholar 

  10. Diamond, S., Boyd, S.: CVXPY: a python-embedded modeling language for convex optimization. J. Mach. Learn. Res. 17(83), 1–5 (2016)

    MathSciNet  Google Scholar 

  11. Domahidi, A., Chu, E., Boyd, S.: ECOS: an SOCP solver for embedded systems. In: 2013 European Control Conference (ECC), pp. 3071–3076. IEEE (2013). https://doi.org/10.23919/ECC.2013.6669541

  12. Flatt, O., Coward, S., Willsey, M., Tatlock, Z., Panchekha, P.: Small proofs from congruence closure. In: 2022 Formal Methods in Computer-Aided Design (FMCAD), pp. 75–83. IEEE (2022). https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_13

  13. Fu, A., Narasimhan, B., Boyd, S.: CVXR: an R package for disciplined convex optimization. J. Stat. Softw. 94, 1–34 (2020). https://doi.org/10.18637/jss.v094.i14

  14. Gjørup, E.H., Spitters, B.: Congruence closure in cubical type theory. In: Workshop on Homotopy Type Theory/Univalent Foundations (2020). https://www.cs.au.dk/~spitters/Emil.pdf

  15. Grant, M., Boyd, S.: CVX: MATLAB software for disciplined convex programming, version 2.1 (2014). http://cvxr.com/cvx

  16. Grant, M., Boyd, S., Ye, Y.: Disciplined convex programming. In: Global Optimization: From Theory to Implementation, pp. 155–210 (2006). https://doi.org/10.1007/0-387-30528-9_7

  17. Harrison, J.: Verifying nonlinear real formulas via sums of squares. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 102–118. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74591-4_9

    Chapter  Google Scholar 

  18. Härter, V., Jansson, C., Lange, M.: VSDP: A MATLAB toolbox for verified semidefinite-quadratic-linear programming. Optimization Online (2012). https://optimization-online.org/?p=12271

  19. Hickey, T.J., Ju, Q., van Emden, M.H.: Interval arithmetic: from principles to implementation. J. ACM 48(5), 1038–1068 (2001). https://doi.org/10.1145/502102.502106

    Article  MathSciNet  Google Scholar 

  20. Limperg, J., From, A.H.: Aesop: white-box best-first proof search for Lean. In: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 253–266 (2023). https://doi.org/10.1145/3573105.3575671

  21. Martin-Dorel, É., Roux, P.: A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations. In: Bertot, Y., Vafeiadis, V. (eds.) Certified Programs and Proofs (CPP) 2017, pp. 90–99. ACM (2017). https://doi.org/10.1145/3018610.3018622

  22. Moura, L., Ullrich, S.: The lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 625–635. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-79876-5_37

    Chapter  Google Scholar 

  23. Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM (JACM) 27(2), 356–364 (1980). https://doi.org/10.1145/322186.322198

    Article  MathSciNet  Google Scholar 

  24. Nieuwenhuis, R., Oliveras, A.: Proof-producing congruence closure. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 453–468. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-32033-3_33

    Chapter  Google Scholar 

  25. Panchekha, P., Sanchez-Stern, A., Wilcox, J.R., Tatlock, Z.: Automatically improving accuracy for floating point expressions. ACM SIGPLAN Not. 50(6), 1–11 (2015). https://doi.org/10.1145/2813885.2737959

    Article  Google Scholar 

  26. Paulson, L.C.: A higher-order implementation of rewriting. Sci. Comput. Program. 3(2), 119–149 (1983). https://doi.org/10.1016/0167-6423(83)90008-4

    Article  MathSciNet  Google Scholar 

  27. Selsam, D., de Moura, L.: Congruence closure in intensional type theory. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 99–115. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40229-1_8

    Chapter  Google Scholar 

  28. Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. J. ACM (JACM) 22(2), 215–225 (1975). https://doi.org/10.1145/321879.321884

    Article  MathSciNet  Google Scholar 

  29. Tate, R., Stepp, M., Tatlock, Z., Lerner, S.: Equality saturation: a new approach to optimization. In: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 264–276 (2009). https://doi.org/10.1145/1480881.1480915

  30. Udell, M., Mohan, K., Zeng, D., Hong, J., Diamond, S., Boyd, S.: Convex optimization in Julia. In: 2014 First Workshop for High Performance Technical Computing in Dynamic Languages, pp. 18–28. IEEE (2014). https://doi.org/10.1109/HPTCDL.2014.5

  31. Ullrich, S., de Moura, L.: Beyond notations: hygienic macro expansion for theorem proving languages. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 167–182. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-51054-1_10

    Chapter  Google Scholar 

  32. VanHattum, A., Nigam, R., Lee, V.T., Bornholt, J., Sampson, A.: Vectorization for digital signal processors via equality saturation. In: Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 874–886 (2021). https://doi.org/10.1145/3445814.3446707

  33. Wang, Y.R., Hutchison, S., Suciu, D., Howe, B., Leang, J.: SPORES: sum-product optimization via relational equality saturation for large scale linear algebra. Proc. VLDB Endow. 13(11), 1919–1932 (2020). https://doi.org/10.14778/3407790.3407799. http://www.vldb.org/pvldb/vol13/p1919-wang.pdf

  34. Willsey, M., Nandi, C., Wang, Y.R., Flatt, O., Tatlock, Z., Panchekha, P.: Egg: fast and extensible equality saturation. Proc. ACM Program. Lang. 5(POPL), 1–29 (2021). https://doi.org/10.1145/3434304

  35. Wright, M.: The interior-point revolution in optimization: history, recent developments, and lasting consequences. Bull. Am. Math. Soc. 42(1), 39–56 (2005). https://doi.org/10.1090/S0273-0979-04-01040-7

    Article  MathSciNet  Google Scholar 

  36. Yamashita, M., Fujisawa, K., Kojima, M.: Implementation and evaluation of SDPA 6.0 (semidefinite programming algorithm 6.0). Optim. Methods Softw. 18(4), 491–505 (2003). https://doi.org/10.1080/1055678031000118482

  37. Yang, Y., Phothilimthana, P., Wang, Y., Willsey, M., Roy, S., Pienaar, J.: Equality saturation for tensor graph superoptimization. Proc. Mach. Learn. Syst. 3, 255–268 (2021). https://proceedings.mlsys.org/paper_files/paper/2021/file/cc427d934a7f6c0663e5923f49eba531-Paper.pdf

  38. Zhang, Y., et al.: Better together: unifying datalog and equality saturation. Proc. ACM Program. Lang. 7(PLDI), 468–492 (2023). https://doi.org/10.1145/3591239

Download references

Author information

Authors and Affiliations

  1. University of Edinburgh, Edinburgh, UK

    Ramon Fernández Mir & Paul B. Jackson

  2. University of Cambridge, Cambridge, UK

    Siddharth Bhat & Tobias Grosser

  3. Universiteit van Amsterdam, Amsterdam, The Netherlands

    Andrés Goens

Authors
  1. Ramon Fernández Mir
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Paul B. Jackson
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Siddharth Bhat
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Andrés Goens
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Tobias Grosser
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Ramon Fernández Mir or Paul B. Jackson .

Editor information

Editors and Affiliations

  1. Neu-Ulm University of Applied Sciences, Neu-Ulm, Germany

    Andrea Kohlhase

  2. TU Wien, Vienna, Austria

    Laura Kovács

Rights and permissions

Reprints and permissions

Copyright information

© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Fernández Mir, R., Jackson, P.B., Bhat, S., Goens, A., Grosser, T. (2024). Transforming Optimization Problems into Disciplined Convex Programming Form. In: Kohlhase, A., Kovács, L. (eds) Intelligent Computer Mathematics. CICM 2024. Lecture Notes in Computer Science(), vol 14960. Springer, Cham. https://doi.org/10.1007/978-3-031-66997-2_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-66997-2_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-66996-5

  • Online ISBN: 978-3-031-66997-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation