Motivated by the recent 10 million dollar AIMO challenge, this paper targets the problem of finding all functions conforming to a given specification. This is a popular problem at mathematical competitions and it brings about a number of challenges, primarily, synthesizing the possible solutions and proving that no other solutions exist. Often, there are infinitely many solutions and then the set of solutions has to be captured symbolically. We propose an approach to solving this problem and evaluate it on a set of problems that appeared in mathematical competitions and olympics.
(2)
As a source for our problems we have used a collection compiled by Vít Musil [
• The satisfiability of the specification if there is a solution (problems find); for the example above: ∀ : R. ( + ) = () + () • The unsatisfiability of the specification together with the negation of all proposed solutions (problems prove); for the example above:
∀ : R. ( + ) = () + () ∧ ∃ : R. () ̸= 0 • The check that every proposed solution is indeed a solution to the specifications (problems check), i.e., the unsatisfiability of the proposed solution together with the negation of the specification; for the example above: 4
∃ : R. ( + ) ̸= () + () ∧ ∀ : R. () = 0
This way, we are asking SMT solvers to solve particular steps, although these steps do not necessarily
cover the full solution of a functional equation. We are not providing a formal description of what a
valid solution is allowed to consist of (that could be further work using for example SyGuS [
We remark that during this work we uncovered several bugs in our translation to SMT from the
source material. But also, we have found an issue in the original source material. Namely the problem
C9 (Cvičení 9) was unsatisfiable in the original [
Section 3 describes our approach to solving the problem by trying to prove that it fits a fixed template, in particular, we focus on functions that can be expressed as polynomials. In most cases, this is probably not how a human would solve it. It is the subject of future work to make this connection. For comparison, we show here three example problems together with their original (human) solutions: • Problem U24, which is among the most interesting ones that we were able to fully solve; • Problem C12, which we were not able to solve but it does not require any advanced technique, so it could be feasible to solve it; • Problem U2, which showcases a problem requiring induction to be solved, and we assume is currently out of reach.
of real numbers , , the following identity holds
() + () = ( () ()). 3https://prase.cz/info/info_en.php?lang=1 4In most cases, the SMT solver can get rid of completely by macro detection. 5https://github.com/MikolasJanota/FuncProbs Solution: First, we notice that the image of is closed under addition: if , are the values of at points , , then also + is a value of , in particular at point () () = . Fix arbitrary 1, and denote = (1). By the previous observation, we can find also 2 and 4 such that (2) = 2, and (4) = 4.
Now, we plug into the functional equation the assignments ( = 2, = 2), and ( = 1, = 4).
4 = (2) + (2) = ( (2) (2)) = (42)
5 = (1) + (4) = ( (1) (4)) = (42)
We conclude 4 = 5, and consequently = 0. Since we started with arbitrary () = , the function
must be constant zero, which indeed satisfies the equation. For this problem, the SMT solver cvc5 was
able to demonstrate that must be constantly 0 by the enumerative strategy [
Example Problem C12 (IMO 1992-2): Find all functions : R → R such that for any pair of real numbers , , the following identity holds
(2 + ()) = + ()2.
Solution: Setting = 0 gives ( ()) = + (0)2. The right-hand side + (0)2 is a bijection, so also the left-hand side ∘ is a bijection R → R, and that can only happen when itself is a bijection.
Since is a bijection, we can consider an argument such that () = 0. Let us substitute ( = , = 0) and ( = − , = 0) to the original equation.
0 = 0 + ()2 = (2 + (0)) = ((− )2 + (0)) = 0 + (− )2 = (− )2.
We obtained (− ) = 0. By injectivity, − = , so = 0, and (0) = 0. This also simplifies our first observation to ( ()) = .
Now we prove that the function is increasing. Any pair of numbers < can be expressed as = (), = 2 + () for some , , ̸= 0. Combining the original equation with the same equation having substituted = 0, we get
() = ( ()) = < + ()2 = (2 + ()) = (), concluding that is increasing.
Consider any where ≤ (). Since is increasing, also () ≤ ( ()) = . Analogously, if () ≤ , we obtain = ( ()) ≤ (). Thus the statements ≤ () and () ≤ are equivalent for any , leaving the only option () = , which is a function satisfying the given equation.
any pair of real numbers , , the following identity holds
() + () = ( + ). 6To obtain instantiations from cvc5, use –no-e-matching –enum-inst –dump-instantiations –produce-proof. Proof sketch: By setting = 0, , 2, 3, . . ., we obtain by induction that () = () for every non-negative integer , in particular (0) = 0, and if we fix = 1 and denote (1) = , we obtain the following equation for all non-negative integers .
() = . ( ) ♣ We gradually extend the domain for which we know this equation. First, substitution ( = , = − ) into the original equation gives () = − (− ) which extends (♣) to all integers . Let be an arbitrary number satisfying (♣), and be a positive integer. Then leading to = ︁( )︁ .
Therefore, (♣) holds for any rational number .
Finally, we show that (♣) must be satisfied by every real number. Suppose on the contrary that for some , we have for example () < , or () > . We discuss here the first option, the other one is analogous. If () < , there is a rational number such that () < < (note > 0 since is assumed to be increasing). Then < but () < = () contradicting that is increasing.
This proof goes beyond the abstraction level of SMT solvers. Notably, it uses induction, which SMT
solvers can do [
One could see the problem as quantifier elimination in the theory of uninterpreted functions, accompanied by the theory required for describing the problem itself — in our case, the theory of reals or rationals. Due to the undecidability of such a problem, quantifier elimination algorithms cannot be used directly. A possible approach would be to synthesize one function adhering to the specification and then strengthen the specification so that the individual solution is not admitted any more. Then, one would have to repeat this process with the hope that there are finitely many solutions, or, observe the solutions and generalize them into a more compact description. All these steps are highly nontrivial. Instead, we propose an approach that tries a fixed template and then performs quantifier elimination: template-and-QE, which comprises the following subtasks.
1. Identify a template for the solution, e.g. () ≜ + . 2. Prove that all solutions must fall into this template (template verification ) 3. Perform quantifier elimination over input variables of the function(s).
Note that in the case of reals, all tasks are computable, except for task 2. The remainder of this section elaborates on the individual steps.
We run cvc5 [
We consider the following set of templates for solutions: constant, (monomial) linear, (monomial) quadratic. All these are subclasses of the quadratic form but we consider these to simplify the task for 7The standard does not list UFNRA as one of the logics, therefore the files indicate AUFNIRA as the closest superset. the solvers—it is conceivable that it is easier to prove that the function must be constant than to prove that it must be arbitrary quadratic. Since the set of templates is small, we always try all of them.
In order to ask an SMT solver if all solutions must be linear, we add the assertion that the function is not linear. An obvious way to state that is linear is via the formula ∃ : R.∀ : R. () = + . We call the problem resulting from including the properties of the original problem along with the negation of ∃ : R.∀ : R. () = + the first variant of the linear template verification . We had more success using a diferent test for linearity. A function is linear if and only if ∀ : R. () = ( (1) − (0)) + (0). Note that this formulation avoids the use of existential quantifiers. We call the problem resulting from including the properties of the original problem along with the negation of ∀ : R. () = ( (1) − (0)) + (0) the second variant of the linear template verification . If any SMT solver can determine either variant is unsatisfiable, then we know all solutions must be linear.
We likewise have two variants for each of the other templates. The formulations for the first variants simply use existential quantification for the coeficients. For the second variants, we use the following properties: • constant: ∀ : R. () = (0) • monomial linear: ∀ : R. () = (1) • linear: ∀ : R. () = ( (1) − (0)) + (0) • monomial quadratic: ∀ : R. () = (1)2 • quadratic: ∀ : R.2 () = (( (1) + (− 1)) − 2 (0))2 + ( (1) − (− 1)) + 2 (0)
In addition to using SMT solvers, we also used Waldmeister [15]. Waldmeister is an automated theorem prover specializing in first-order unit equality. Unlike SMT solvers, Waldmeister has no information about integers or reals. Consequently, in order to ask Waldmeister if all functions satisfying some properties must be contained within the class given by a template, we first declare a sort along with constants 0, 1 : and operations +, − , · satisfying properties of a commutative ring with identity. Each of these properties is given by a unit equation. We purposely use rings instead of fields (although R is a ifeld). This allows us to ignore division since the side condition that the denominator is not zero would result in a clause that is not a unit equation. We only generate such a problem for Waldmeister when all the properties stated for in the problem are unit equations, only quantify over reals (as opposed to integers), and do not use division. Furthermore, we require that all specific real numbers mentioned in the properties correspond to integers (e.g., 0.0, 1.0, -1.0, etc.). These restrictions allow us to formulate a unit equation to give Waldmeister corresponding to each property of given in the problem.
In addition to the assumed unit equations, Waldmeister expects a unit equation as a goal to prove. The goal varies based on the template we are targeting and corresponds to the second variant of the problems for the SMT solver. In each case we fix a constant of type (not mentioned in the assumptions). For each template, the goal unit equation is as follows: • constant: () = (0) • monomial linear: () = (1) • linear: () = ( (1) − (0)) + (0) • monomial quadratic: () = (1)2 • quadratic: 2 () = (( (1) + (− 1)) − 2 (0))2 + ( (1) − (− 1)) + 2 (0) Waldmeister uses Knuth-Bendix style completion [17] on the assumed unit equations finding a proof of the goal when both sides of the goal rewrite to a common term.
For 8 of the problems, Waldmeister can prove all solutions are within the expected class. Two of these problems were not covered by SMT solvers: U25 and U87. In both of these problems, the least template class is linear monomials. We briefly discuss these two problems.
The problem U25 asks for all real functions satisfying ( () + ()) = + ()2. Musil [
Waldmeister also proves all solutions to the problem U87 are linear monomials. The problem U87 asks
for all real functions satisfying ( + 2 + ) = ( ()) + () + (). The (only) two solutions
are () = and () = 0. In this case, there is no corresponding proof by Musil [
Quantifier elimination (QE) is a method to take a general formula in a theory and produce an equivalent quantifier-free formula. So for instance, in ∃ ∈ R. < < , the quantified variable is eliminated as < . In many cases, quantifier elimination serves as a theoretical tool to show that a theory is decidable but also has a long tradition of improvements at the algorithmic level [18, 19, 20, 21, 22, 23, 24]. In our work, QE is used to reveal the particular solutions within a class given by a template.
We assume the original problem only has one uninterpreted function, , and it is a unary function from reals to reals. If we want to determine all functions of the form () = + , we can simply inline in the properties, replacing each occurrence () by + . The resulting problem has no uninterpreted functions and is usually in the theory of the reals. (Exceptional cases are when the properties mention integers as well as reals.) When the problem and template result in such an inlined problem in the theory of reals, we can apply quantifier elimination.
We have made use of two implementations of quantifier elimination for the reals: Z3 [
Problem U91 asks for all functions satisfying (( − )2) = ()2 − 2 () + 2. Using the techniques of Section 3.1, we can prove all solutions must be linear. After replacing () with + and calling Z3 to do quantifier elimination, we obtain the quantifier-free formulas = 1 and = 0 ∨ = 1. In general, Z3 represents the result of QE as a conjunction of several subformulas. The formula = 1 ∧ ( = 0 ∨ = 1) is almost in solved form, and we can easily obtain the two solutions () = and () = + 1 via postprocessing. Tarski’s quantifier elimination returns the more complicated formula
− 1 + = 0 ∧ ≥ 0 ∧ − 1 + ≤ 0 ∧ ( = 0 ∨ − 1 + = 0).
The postprocessor is also able to obtain the two solutions from this formula.
Sometimes there is a parameterized class of solutions. Problem U3, for example, asks for all functions satisfying ( + ) = () + . The techniques of Section 3.1 determine all solutions are linear. After inlining () = + , we call quantifier elimination. Both Z3 and Tarski produce the formula − 1 + = 0. From this the postprocessor can determine = 1 and is unconstrained. This gives the class of solutions () = + where is a real number. Indeed, this is the class of all solutions, as desired.
We say a quantifier-free formula is in solved form8 if it is a disjunctive normal form where all the literals are of the form = where is a coeficient of the template and is a real number. We call a formula of the form = an assignment atom. The postprocessor is given a list of formulas (thought of conjuctively) and attempts to generate a solved form equivalent to 1 ∧ · · · ∧ . As auxiliary values, a list of equations of the form = and a list of other literals are generated, so that generally we are working with a triple (, , ) of lists of formulas, with and initially empty. Suppose is nonempty, with 1 being the first formula on the list. If 1 is a conjunction or a disjunction, we can simply make recursive calls to the preprocessor to ask for solved forms of the decomposed formulas. In the case of disjunction, we make two recursive calls (one for each disjunct) and combine the results as a disjunction of the two solved forms (or fail if one call fails). If 1 is an equation = , we add this to the equation list . If 1 is of the form ≤ , ≥ , < or > , then we add this to the other list . In every other case for 1, we simply fail to return a solved form. We are nfially left with the case where there are no remaining formulas in . The hope in this case is that contains suficient information to obtain assignment atoms, and we only need to verify that the assignments satisfy the other formulas from . If the assignment atoms satisfy the other formulas, the conjunction of the assignment atoms will be the solved form. If the assignment atoms do not satisfy the other formulas, the empty disjunction ⊥ will be the solved form. It is also possible (e.g., if 2 = 1 is in the list ) a solved form with more than one disjunct. At this point, the algorithm transforms a triple (, , ) where is the list of assignment atoms (initially empty). We will also call an assignment.
We say a term can be evaluated under an assignment if every constant occurring in is associated with a real number via . We say an atom = , ≤ , ≥ , < or > can be evaluated under an assignment if both terms and can be evaluated under an assignment . Clearly, if a term can be evaluated under an assignment , the term evaluates to a specific real number. Likewise, if an atom can be evaluated under an assignment , the atom evaluates to true or false.
Assume is nonempty and = is the first equation on . We consider the following cases (in order), dropping the equation from : 1. Assume both and can be evaluated under . We drop the equation if they evaluate to the same reals and return ⊥ otherwise. 2. Assume is a coeficient and can be evaluated to the real . We add = to . 3. Assume can be evaluated under and is one of a number of special forms which make use of an unassigned coeficient and all other subterms that can be evaluated under . Examples of these special forms are 1 + , 1 + 2 and 2. In each case we solve for values of and add = to (or fail). If there are no solutions, we return ⊥. If there are multiple solutions, we recursively call with both assignments and return the disjunction of the resulting solved forms. 4. Assume the first equation = is of the form + 1 = and there is a second equation ′ = ′ on the list of the form + = ′ where and are unassigned coeficients and 1, and ′ can all be evaluated under . Then we solve these two linear equations for and (if possible) and add these to the assignment , dropping both equations from .
We finally assume is empty. If some formula in cannot be evaluated via the assignment , then we fail to return a solved form. Assume every can be evaluated via the assignment . If every evaluates to true, then we return the conjunction of the assignment atoms in as the solved form. Otherwise, we return ⊥ as the solved form.
The postprocessor included suficiently many cases to obtain a solved form from either the output of Z3 or Tarski (or preferably both) in each of the problems we considered. There are many cases in which it will fail to compute a solved form. Easy examples are 3 = 1 and 2 + = 2 ∧ + = 1. 8One may imagine loosening the concept but the general idea is to provide a specific solution as possible.
We now briefly consider an alternative to the approach outlined above. When considering a template, we do not need to verify that all solutions are in the template class in advance. Instead, we could use QE to find a class of solutions for a fixed template and then prove there are no other solutions. The advantage of this approach is illustrated by the following example. Problem C1 asks for all functions such that the following holds
( + ) + 2 ( − ) − 4 () + () = 32 − 2 − 2 + 2.
The only solution is () = 2.
In this case, the solvers listed in Section 3.1 are unable to prove that all solutions are a monomial quadratic (or that they must be quadratic). However, we can still apply quantifier elimination to find all monomial quadratic solutions. For this example, Z3 timed out even when given 10 minutes. On the other hand, Tarski returned the formula − 1 + = 0 (yielding the solution = 1, i.e., 2) in less than a second. Since we were unable to prove all solutions must belong to the monomial quadratic template class, it is still possible there are more solutions outside the monomial quadratic template class. However, now that we have the specific solution () = 2 we can ask an SMT solver to prove this is the only solution by assuming the equation and also the negation of ∀ : R. () = 2. The solver cvc5 is easily able to show this is unsatisfiable, so we know that () = 2 is the only solution.
We report the results of the template-and-qe method (Section 3) on the benchmark presented in Section 2. The lazy extension of our approach (Section 3.3.1) was left for future work. The template verification (Section 3.1) has proven to be the most dificult task. Table 1a summarizes the obtained results for template verification. For all these, we were able to solve the QE task. Thirteen instances were solved completely by the automated method. Out of these thirteen, two can be traced to a competition event. Problem U24 comes from Baltic Way competition—see Section 2 for “human” solution. Problem U71 comes from The Prague Seminar (PraSe-18-6-1). In both cases, the only solution is a function that is constantly 0.
The verification tasks results often in satisfiable problems, namely if there exists a solution outside of the proposed template (the × symbol in Table 1a). These satisfiable problems are nontrivial because they involve creating a counterexample to the template. For this purpose, we also ran the SyGuS approach of cvc5 (option –sygus-inference) and its linear model builder [27].
We also report on the verification of the correctness of the handwritten solutions, which comprises two components: prove — show that all possible solutions are covered by the suggested solutions; check — check that all suggested solutions are indeed solutions to the problem (see Section 2). Table 1b summarizes the obtained results. Sixty-five of the provided handwritten solutions were successfully checked, i.e., the individual solutions satisfy the original specifications. Twenty of the handwritten solutions were shown to cover all the individual solutions. Unsurprisingly, the proving task is harder than the checking task. We remark that checking solutions for U79 is trivial because there are no individual solutions. More detailed results can be found on the authors’ web page [28].
This paper joins the efort of rising to the challenge of making computers as powerful as the golden medalists at the International Math Olympics (IMO). Eforts such as AlphaGeometry [ 29], show that machine learning models are useful for the task but at the same time, further research shows that they benefit from existing symbolic methods [ 30]. Here we show that symbolic methods are indeed already powerful in solving a highly nontrivial task of finding all functions fulfilling a certain specification. Besides the task leading to undecidable questions, its dificulty also lies in the fact it is not a decision problem but the response is a description of a class of mathematical objects.
The method we employ is anchored in templates, which is a well-known technique in function and program synthesis [31]. The templates we consider are rather simple and they could be made more powerful by adding conditionals (if-then-else). However, the templates need to be kept simple if we wish to be able to apply quantifier elimination.
An alternative to templates would be to attempt extending diferent synthesis approaches, e.g., such
as those that are realized in saturation-based solvers [
The results were supported by the Ministry of Education, Youth and Sports within the dedicated program ERC CZ under the project POSTMAN no. LL1902 and co-funded by the European Union under the project ROBOPROX (reg. no. CZ.02.01.01/00/22_008/0004590). C. Brown was supported by CORESENSE: the European Union’s Horizon Europe research and innovation programme under grant agreement no. 101070254 CORESENSE. This article is part of the RICAIP project that has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 857306. [14] L. Kovács, A. Voronkov, First-order theorem proving and Vampire, in: N. Sharygina, H. Veith (Eds.), Computer Aided Verification - 25th International Conference, CAV, volume 8044 of LNCS, Springer, 2013, pp. 1–35. doi:10.1007/978-3-642-39799-8\_1. [15] T. Hillenbrand, B. Löchner, The next Waldmeister loop, in: A. Voronkov (Ed.), Automated Deduction - CADE-18, 18th International Conference on Automated Deduction, volume 2392 of Lecture Notes in Computer Science, 2002, pp. 486–500. doi:10.1007/978-3-540-45085-6_27. [16] C. Barrett, P. Fontaine, C. Tinelli, The SMT-LIB Standard: Version 2.6, Technical Report, Department of Computer Science, The University of Iowa, 2017. Available at www.SMT-LIB.org. [17] L. Bachmair, N. Dershowitz, D. A. Plaisted, Completion without failure, in: Rewriting Techniques,
Elsevier, 1989, pp. 1–30. [18] G. E. Collins, Quantifier elimination for real closed fields by cylindrical algebraic decompostion, in: H. Brakhage (Ed.), Automata Theory and Formal Languages, Springer, Berlin, Heidelberg, 1975, pp. 134–183. [19] D. C. Cooper, Theorem proving in arithmetic without multiplication, Machine intelligence 7 (1972) 300. [20] J. Ferrante, C. Rackof, A decision procedure for the first order theory of real addition with order,
SIAM Journal on Computing 4 (1975) 69–76. doi:10.1137/0204006. [21] R. Loos, V. Weispfenning, Applying linear quantifier elimination, Comput. J. 36 (1993) 450–462.
doi:10.1093/COMJNL/36.5.450. [22] J. H. Davenport, Y. Siret, E. Tournier, Computer algebra - systems and algorithms for algebraic computation (2. ed.), Academic Press, 1993. [23] A. R. Bradley, Z. Manna, The calculus of computation - decision procedures with applications to verification, Springer, 2007. doi: 10.1007/978-3-540-74113-8. [24] N. S. Bjørner, M. Janota, Playing with quantified satisfaction, in: LPAR, EasyChair, 2015, pp. 15–27.
doi:10.29007/VV21. [25] F. Vale-Enriquez, C. W. Brown, Polynomial constraints and unsat cores in Tarski, in: J. H. Davenport, M. Kauers, G. Labahn, J. Urban (Eds.), Mathematical Software - ICMS - 6th International Conference, volume 10931 of LNCS, Springer, 2018, pp. 466–474. doi:10.1007/978-3-319-96418-8\_55. [26] G. E. Collins, H. Hong, Partial cylindrical algebraic decomposition for quantifier elimination, J.
Symb. Comput. 12 (1991) 299–328. doi:10.1016/S0747-7171(08)80152-6. [27] M. Janota, B. Piotrowski, K. Chvalovský, Towards learning infinite SMT models, 2023. URL: http://people.ciirc.cvut.cz/~janotmik/, 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC. [28] M. Janota, 2024. URL: https://sat.inesc-id.pt/~mikolas/sc2_2024/. [29] T. H. Trinh, Y. Wu, Q. V. Le, H. He, T. Luong, Solving olympiad geometry without human demonstrations, Nature 625 (2024) 476–482. doi:10.1038/s41586-023-06747-5. [30] S. Sinha, A. Prabhu, P. Kumaraguru, S. Bhat, M. Bethge, Wu’s method can boost symbolic AI to rival silver medalists and AlphaGeometry to outperform gold medalists at IMO geometry, 2024. arXiv:2404.06405. [31] S. Srivastava, S. Gulwani, J. S. Foster, Template-based program verification and program synthesis,
Int. J. Softw. Tools Technol. Transf. 15 (2013) 497–518. doi:10.1007/S10009-012-0223-4. [32] A. Reynolds, V. Kuncak, C. Tinelli, C. W. Barrett, M. Deters, Refutation-based synthesis in SMT,
Formal Methods Syst. Des. 55 (2019) 73–102. doi:10.1007/S10703-017-0270-2. [33] A. Abate, H. Barbosa, C. W. Barrett, C. David, P. Kesseli, D. Kroening, E. Polgreen, A. Reynolds, C. Tinelli, Synthesising programs with non-trivial constants, J. Autom. Reason. 67 (2023) 19. doi:10.1007/S10817-023-09664-4. [34] H. Barbosa, A. Reynolds, D. Larraz, C. Tinelli, Extending enumerative function synthesis via SMT-driven classification, in: C. W. Barrett, J. Yang (Eds.), Formal Methods in Computer Aided Design, FMCAD, IEEE, 2019, pp. 212–220. doi:10.23919/FMCAD.2019.8894267. [35] D. M. Cerna, A. Cropper, Generalisation through negation and predicate invention, in: Proceedings of the AAAI Conference on Artificial Intelligence, volume 38, 2024, pp. 10467–10475. doi: 10.1609/ aaai.v38i9.28915.