Copyright for this paper by its authors. Use permitted under Creative Commons
License Attribution 4.0 International (CC BY 4.0).

SC2 Workshop 2024: Satisfiability Checking and Symbolic Computation

[orcid=0000-0003-3487-784X<EMAIL_ADDRESS>url=http://people.ciirc.cvut.cz/ janotmik/] [orcid=0000-0002-9361-1921]

# Symbolic Computation for All the Fun

Chad E. Brown  Mikoláš Janota  Mirek Olšák  Czech Technical University in
Prague, CIIRC, Czechia  University of Cambridge

(2024)

###### Abstract

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.

###### keywords:

AIMO synthesis quantifier elimination SMT

##  1 Introduction

The _AIMO challenge_ 111https://aimoprize.com/ promises to award $10 million
to an AI model that will be able to win a gold medal at the _International
Mathematical Olympiad (IMO)_ 222https://www.imo-official.org/. In this paper
we draw attention to the fact that symbolic computation tools can give a
significant boost to a system aiming at this challenge. We target a popular
problem encountered in mathematical competitions, which is finding _all_
functions adhering to a certain specification. The task in its generality is
nearly impossible but the problems in the competitions are constructed so that
they have nice solutions. As a motivational example, consider the problem that
asks us to find all functions $f$ from $\mathbb{R}$ to $\mathbb{R}$ satisfying
the following identity.

$\forall xy:\mathbb{R}.f(x+y)=xf(y)+yf(x)$ (1)

Substituting $y$ with $0$ gives $\forall x:\mathbb{R}.f(x)=f(0)x$, which tells
us that $f$ must be linear and that it is fully determined by the value of
$f(0)$. Further, substituting $x$ with $0$ shows that $f$ has to be $0$
everywhere, i.e., the solution is $fx\triangleq 0$. A solution is expected to
give a clear description of how all possible $f$ are calculated, possibly
parametrized by constants. To verify the correctness of the solution, one
needs to prove the following biimplication.

$(\forall xy:\mathbb{R}.f(x+y)=xf(y)+yf(x))\Leftrightarrow(\forall
x:\mathbb{R}.fx=0)\\\ $ (2)

Note that the problem of finding all solutions is not fully formal in the
problem statement, that is, we expect a “reasonable description” of the set of
all the solutions. For example, the following would _not_ be considered a
valid answer: The solution consists of all the functions satisfying
$f(x+y)=xf(y)+yf(x)$ for all $x,y\in\mathbb{R}$.

A problem of such a form “find all solutions satisfying $X$” sparked some
debate within the community about how they should be formally handled. How
exactly we handle such question is explained in Sections 3.

##  2 Problems Description

As a source for our problems we have used a collection compiled by Vít Musil
[1] comprising problems from several sources, including international
competition and some (easier) problems from the The Prague Seminar in
Mathematics333https://prase.cz/info/info_en.php?lang=1. We have transcribed
the problems into SMT2, where each original problem is divided into 3 type of
queries.

  * •

The satisfiability of the specification if there is a solution (problems
find).

  * •

The unsatisfiability of the specification together with the negation of all
proposed solutions (problems prove).

  * •

The check that every proposed solution is indeed a solution to the
specifications (problems check).

This way, we are asking SMT solvers to solve particular steps, although these
steps are not necessarily covering 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). Rather, we
use our own method for finding the set of all solutions of a particular form,
described in Section 3. The SMT2 problems are made available as a github
repository444https://github.com/MikolasJanota/FuncProbs describing 87
problems. In some cases, the check query is split into multiple SMT2 files, if
there are multiple distinct solutions.

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 U9 (Cvičení 9) was unsatisfiable
in the original [1] and we created two versions of the problem as two
different ways of correcting it (C9 and C9a).

###  2.1 Solutions of Selected Problems

We show here three more 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.

Example Problem U24 (Baltic Way 1998-7): Find all functions
$f:\mathbb{R}\to\mathbb{R}$ such that for any pair of real numbers $x,y$, the
following identity holds

$f(x)+f(y)=f(f(x)f(y)).$

Solution: First we notice that the image of $f$ is closed under addition: if
$a,b$ are the values of $f$ at points $x$, $y$, then also $a+b$ is a value of
$f$, in particular at point $f(x)f(y)=ab$. Fix arbitrary $x_{1}$, and denote
$a=f(x_{1})$. By the previous observation, we can find also $x_{2}$ and
$x_{4}$ such that $f(x_{2})=2a$, and $f(x_{4})=4a$.

Now, we plug into the functional equation the assignments $(x=x_{2},y=x_{2})$,
and $(x=x_{1},y=x_{4})$.

$\displaystyle 4a=f(x_{2})+f(x_{2})$
$\displaystyle=f(f(x_{2})f(x_{2}))=f(4a^{2})$ $\displaystyle
5a=f(x_{1})+f(x_{4})$ $\displaystyle=f(f(x_{1})f(x_{4}))=f(4a^{2})$

We conclude $4a=5a$, and consequently $a=0$. Since we started with arbitrary
$f(x)=a$, the function must be constant zero, which indeed satisfies the
equation.

Example Problem C12 (IMO 1992-2): Find all functions
$f:\mathbb{R}\to\mathbb{R}$ such that for any pair of real numbers $x,y$, the
following identity holds

$f(x^{2}+f(y))=y+f(x)^{2}.$

Solution: Setting $x=0$ gives $f(f(y))=y+f(0)^{2}.$ The right-hand side
$y+f(0)^{2}$ is a bijection, so also the left hand side $f\circ f$ is a
bijection $\mathbb{R}\to\mathbb{R}$, and that can only happen when $f$ itself
is a bijection.

Since $f$ is a bijection, we can consider an argument $b$ such that $f(b)=0$.
Let us substitute $(x=b,y=0)$ and $(x=-b,y=0)$ to the original equation.

$0=0+f(b)^{2}=f(b^{2}+f(0))=f((-b)^{2}+f(0))=0+f(-b)^{2}=f(-b)^{2}.$

We obtained $f(-b)=0$. By injectivity, $-b=b$, so $b=0$, and $f(0)=0$. This
also simplifies our first observation to $f(f(y))=y$.

Now we prove that the function is increasing. Any pair of numbers $a<b$ can be
expressed as $a=f(y),b=x^{2}+f(y)$ for some $x,y$, $x\neq 0$. Combining the
original equation with the same equation having substituted $x=0$, we get

$f(a)=f(f(y))=y<y+{f(x)}^{2}=f(x^{2}+f(y))=f(b),$

concluding that $f$ is increasing.

Consider any $y$ where $y\leq f(y)$. Since $f$ is increasing, also $f(y)\leq
f(f(y))=y$. Analogously, if $f(y)\leq y$, we obtain $y=f(f(y))\leq f(y)$. Thus
the statements $y\leq f(y)$ and $f(y)\leq y$ are equivalent for any $y$,
leaving the only option $f(y)=y$, which is a function satisfying the given
equation.

Example Problem U2 (Cauchy equation): Find all increasing functions
$f:\mathbb{R}\to\mathbb{R}$ such that for any pair of real numbers $x,y$, the
following identity holds

$f(x)+f(y)=f(x+y).$

Proof sketch: By fixing $x=1$, and setting $y=0,1,2,\ldots$, we obtain by
induction that $f(nx)=n\cdot f(x)$ for every non-negative integer $n$, in
particular $f(0)=0$, and if we denote $f(1)=c$, we obtain the following
equation for all non-negative integers $x$.

$f(x)=cx.$ ($\clubsuit$)

We gradually extend the domain for which we know this equation. First,
substitution $(x=x,y=-x)$ into the original equation gives $f(x)=-f(-x)$ which
extends ($\clubsuit$ ‣ 2.1) to all integers $x$. Let $x$ be an arbitrary
number satisfying ($\clubsuit$ ‣ 2.1), and $n$ be a positive integer. Then

$cx=f(x)=f\left(n\cdot\frac{x}{n}\right)=n\cdot f\left(\frac{x}{n}\right)$

leading to

$c\cdot\frac{x}{n}=f\left(\frac{x}{n}\right).$

Therefore, ($\clubsuit$ ‣ 2.1) holds for any rational number $x$.

Finally, we show that ($\clubsuit$ ‣ 2.1) must be satisfied by every real
number. Suppose on the contrary that for some $x$, we have for example
$f(x)<cx$, or $f(x)>cx$. We discuss here the first option, the other one is
analogous. If $f(x)<cx$, there is a rational number $q$ such that
$\frac{f(x)}{c}<q<x$ (note $c>0$ since $f$ is increasing). Then $q<x$ but
$f(x)<qc=f(q)$ contradicting that $f$ is increasing.

##  3 Template-and-QE

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 anymore. 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. 1.

_Identify_ a template for the solution, e.g. $fx\triangleq ax+b$.

  2. 2.

_Prove_ that all solutions must fall into this template (_template
verification_)

  3. 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.

###  3.1 Template Verification

We run cvc5 [2], z3 [3], Vampire [4] and Waldmeister [5] to attempt to prove
all solutions to a problem necessarily fit a certain template. Since
Waldmeister does not support theories directly, it needs to special treatment
and we elaborate on this below. The other solvers support natively the SMT2
syntax [6] enabling us to use the combination of quantified non-linear reals
with unintepreted functions.555The standard does not list UFNRA as one of the
logics, therefore the files indicate AUFNIRA as the closest superset.

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 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 SMT2 solver if all solutions must be linear, we add the
assertion that the function is not linear. An obvious way to state that $f$ is
linear is via the formula $\exists ab:\mathbb{R}.\forall
x:\mathbb{R}.f(x)=ax+b$. We call the problem resulting from including the
properties of the original problem along with the negation of $\exists
ab:\mathbb{R}.\forall x:\mathbb{R}.f(x)=ax+b$ the _first variant of the linear
template verification_. We had more success using a different test for
linearity. A function $f$ is linear if and only if $\forall
x:\mathbb{R}.f(x)=(f(1)-f(0))x+f(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 $\forall
x:\mathbb{R}.f(x)=(f(1)-f(0))x+f(0)$ _the second variant of the linear
template verification_. If any SMT2 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 coefficients. For the second variants we use the following properties:

  * •

_constant_ : $\forall x:\mathbb{R}.f(x)=f(0)$

  * •

_monomial linear_ : $\forall x:\mathbb{R}.f(x)=f(1)x$

  * •

_linear_ : $\forall x:\mathbb{R}.f(x)=(f(1)-f(0))x+f(0)$

  * •

_monomial quadratic_ : $\forall x:\mathbb{R}.f(x)=f(1)x^{2}$

  * •

_quadratic_ : $\forall
x:\mathbb{R}.2f(x)=((f(1)+f(-1))-2f(0))x^{2}+(f(1)-f(-1))x+2f(0)$

####  3.1.1 Using Waldmeister

In addition to using SMT2 solvers, we also used Waldmeister [5]. 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 $f$ satisfying some
properties must be contained within the class given by a template, we first
declare a sort $R$ along with constants $0,1:R$ and operations $+$, $-$,
$\cdot$ 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 $\mathbb{R}$ is a field). 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 $f$ 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 $f$ given in the problem.

In addition to the assumed unit equations, Waldmeister expects a unit equation
a as goal to prove. The goal varies based on the template we are targeting and
corresponds to the second variant of the problems for the SMT2 solver. In each
case we fix a constant $d$ of type $R$ (not mentioned in the assumptions). For
each template, the goal unit equation is as follows:

  * •

_constant_ : $f(d)=f(0)$

  * •

_monomial linear_ : $f(d)=f(1)d$

  * •

_linear_ : $f(d)=(f(1)-f(0))d+f(0)$

  * •

_monomial quadratic_ : $f(d)=f(1)d^{2}$

  * •

_quadratic_ : $2f(d)=((f(1)+f(-1))-2f(0))d^{2}+(f(1)-f(-1))d+2f(0)$

Waldmeister uses Knuth-Bendix style completion [7] on the assumed unit
equations finding a proof of the goal when both sides of the goal rewrite to a
common term.

Waldmeister can prove 8 of the problems only have solutions 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 $f$ satisfying
$f(xf(x)+f(y))=y+{f(x)}^{2}$. Musil [1] gives a proof that the only two
solutions are $f(x)=x$ and $f(x)=-x$. Waldmeister’s goal is to prove
$f(d)=f(1)d$ from the ring identities and the equation above. It is difficult
to directly compare the aforementioned human proof to the proof found by
Waldmeister. However, there are some interesting common intermediate results.
Both proofs prove $f$ is involutive (i.e., $f(f(x))=x$), ${f(x)}^{2}=x^{2}$
and $f(0)=0$. On the other hand, there are several identities in each proof
that do not appear in the other. Musil’s proof [1] proves $f$ is surjective
and uses this fact, while the Waldmeister proof cannot directly represent the
concept of surjectivity.

The other problem Waldmeister can prove only has linear monomial solutions is
U87. The problem U87 asks for all real functions $f$ satisfying
$f(x+y^{2}+z)=f(f(x))+yf(y)+f(z)$. The (only) two solutions are $f(x)=x$ and
$f(x)=0$. In this case there is no corresponding proof in [1] as a point of
comparison. A number of intermediate identities derived by Waldmeister stand
out, e.g., $f(f(0))=0$ and $f(f(x))=f(x)$.

###  3.2 Quantifier Elimination

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
$\exists x\in\mathbb{R}.a<x<b$, the quantified variable $x$ is eliminated as
$a<b$. 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 [8, 9, 10, 11, 12, 13, 14]. In our work, quantifier
elimination is used in a practical way to reveal the particular solutions
within a class given by a template.

We assume the original problem only has one uninterpreted function, $f$, and
it is a unary function from reals to reals. If we want to determine all
functions $f$ of the form $f(x)=ax+b$, we can simply inline $f$ in the
properties, replacing each occurrence $f(t)$ by $at+b$. 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 [3] and Tarski [15]. In z3, QE is invoked by applying the qe tactic,
with the qe-nonlinear parameter turned on. The Tarski system is highly
configurable but since QE is not a bottle-neck for us, we use the qepcad-qe
[16] function in its default setting. For each system, quantifier elimination
should result in a quantifier-free formula involving the uninterpreted
constants (e.g., the coefficients $a$ and $b$ of the linear template $ax+b$).
One might expect this formula to be in a solved form, e.g., $a=1\lor a=0\land
b=1$, from which one can read of the precise class of linear functions
satisfying the original property. However, this is generally not the case. A
separate postprocessing step attempts to convert the quantifier-free formula
into such a solved form. In practice the postprocessing does not always
succeed. In the case of z3, we also call the tactics simplify and propagate-
values to have z3 simplify the formula before applying the postprocessing to
attempt to find a solved form.

Problem U91 asks for all functions satisfying
$f((x-y)^{2})={f(x)}^{2}-2xf(y)+y^{2}$. Using the techniques of Section 3.1,
we can prove all solutions $f$ must be linear. After replacing $f(x)$ with
$ax+b$ and calling z3 to do quantifier elimination, we obtain the quantifier-
free formulas $a=1$ and $b=0\lor b=1$. In general, z3 returns several formulas
whose conjunction should be equivalent to the original formula. The formula
$a=1\land(b=0\lor b=1)$ is almost in solved form, and we can easily obtain the
two solutions $f(x)=x$ and $f(x)=x+1$ via postprocessing. Tarski’s quantifier
elimination returns the more complicated formula

$-1+a=0\land b\geq 0\land-1+b\leq 0\land(b=0\lor-1+b=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 $f(x+y)=f(x)+y$. The techniques of
Section 3.1 determine all solutions are linear. After inlining $f(x)=ax+b$ we
call quantifier elimination. Both Z3 and Tarski produce the formula $-1+a=0$.
From this the postprocesser can determine $a=1$ and $b$ is unconstrained. This
gives the class of solutions $f(x)=x+b$ where $b$ is a real number. Indeed,
this is the class of all solutions, as desired.

####  3.2.1 Lazy Verification

An alternative to the approach outlined above, the template of the solution
does not have to be verified all at once. 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 $f$ such that

$f(x+y)+2f(x-y)-4f(x)+xf(y)=3y^{2}-x^{2}-2xy+xy^{2}.$

The only solution is $f(x)=x^{2}$.

In this case, the solvers listed in Section 3.1 are unable to prove 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+a=0$ (yielding the solution $a=1$,
i.e., $x^{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 $f(x)=x^{2}$ we can ask
an SMT2 solver to prove this is the only solution by assuming the equation and
also the negation of $\forall x:\mathbb{R}.f(x)=x^{2}$. The solver cvc5 is
easily able to show this is unsatisfiable, so that we know $f(x)=x^{2}$ is the
only solution.

##  4 Experiments

Table 1: Result summary. Problems without any result are omitted.

Problem | $c$ | $ax$ | $ax+b$ | $ax^{2}$ | $ax^{2}+bx+c$
---|---|---|---|---|---
C2 | $\times$ | $\times$ | $\checkmark$ | $\times$ | $\checkmark$
C6 | $\times$ | $\times$ | - | $\times$ | -
C9a | - | - | - | $\checkmark$ | -
C10 | $\times$ | $\checkmark$ | $\checkmark$ | $\times$ | $\checkmark$
C12 | $\times$ | - | - | $\times$ | -
C13 | $\times$ | $\times$ | $\times$ | $\times$ | $\times$
U2 | $\times$ | - | - | $\times$ | -
U3 | $\times$ | $\times$ | $\checkmark$ | $\times$ | $\checkmark$
U5 | $\times$ | $\checkmark$ | $\checkmark$ | $\times$ | $\checkmark$
U7 | $\times$ | $\times$ | - | $\times$ | -
U9 | $\times$ | $\times$ | $\checkmark$ | $\times$ | $\checkmark$
U13 | $\times$ | $\checkmark$ | $\checkmark$ | $\times$ | $\checkmark$
U16 | $\times$ | $\times$ | $\checkmark$ | $\times$ | -
U20 | $\times$ | $\times$ | - | $\times$ | -
U23 | - | $\times$ | - | $\times$ | -
U24 | $\checkmark$ | $\checkmark$ | $\checkmark$ | $\checkmark$ | $\checkmark$
U25 | $\times$ | $\checkmark$ | $\checkmark$ | $\times$ | -
U26 | $\times$ | - | - | $\times$ | -
U27 | $\times$ | $\times$ | $\times$ | $\times$ | $\times$
U41 | - | $\times$ | - | $\times$ | -
U42 | $\times$ | $\times$ | - | $\times$ | -
U44 | $\times$ | - | - | - | -
U45 | $\times$ | - | - | $\times$ | -
U48 | $\times$ | - | - | $\times$ | -
U49 | $\times$ | - | - | $\times$ | -
U50 | $\times$ | - | - | $\times$ | -
U51 | $\times$ | $\times$ | - | $\times$ | -
U54 | $\times$ | $\times$ | $\times$ | $\times$ | $\times$
U56 | $\times$ | $\times$ | - | $\times$ | -
U62 | $\times$ | - | - | $\times$ | -
U64 | $\times$ | - | - | $\times$ | -
U67 | $\times$ | $\times$ | $\times$ | $\times$ | $\times$
U68 | $\times$ | - | - | $\times$ | -
U71 | $\checkmark$ | $\checkmark$ | $\checkmark$ | $\checkmark$ | $\checkmark$
U72 | - | $\times$ | - | $\times$ | -
U87 | $\times$ | $\checkmark$ | $\checkmark$ | $\times$ | $\checkmark$
U90 | $\times$ | $\times$ | $\times$ | $\times$ | -
U91 | $\times$ | $\times$ | $\checkmark$ | $\times$ | $\checkmark$
U92 | $\times$ | - | - | $\times$ | -
(a)

Problem | Prove | Check
---|---|---
C1 | $\checkmark$ | $\checkmark$
C2 | $\checkmark$ | $\checkmark$
C3 | - | $\checkmark$
C4 | - | $\checkmark$
C5 | $\checkmark$ | $\checkmark$
C6 | - | $\checkmark$
C9 | $\checkmark$ | $\checkmark$
C9a | $\checkmark$ | $\checkmark$
C10 | $\checkmark$ | $\checkmark$
C12 | - | $\checkmark$
C13 | - | $\checkmark$
U2 | - | $\checkmark$
U3 | $\checkmark$ | $\checkmark$
U4 | $\checkmark$ | $\checkmark$
U5 | $\checkmark$ | $\checkmark$
U6 | - | $\checkmark$
U7 | - | $\checkmark$
U8 | - | $\checkmark$
U9 | $\checkmark$ | $\checkmark$
U10 | - | $\checkmark$
U11 | $\checkmark$ | $\checkmark$
U12 | - | $\checkmark$
U13 | $\checkmark$ | $\checkmark$
U14 | - | $\checkmark$
U16 | $\checkmark$ | $\checkmark$
U17 | $\checkmark$ | $\checkmark$
U19 | - | $\checkmark$
U20 | - | $\checkmark$
U23 | - | $\checkmark$
U24 | $\checkmark$ | $\checkmark$
U25 | - | $\checkmark$
U26 | - | $\checkmark$
U27 | - | $\checkmark$
U39 | - | $\checkmark$
U41 | - | $\checkmark$
U42 | - | $\checkmark$
U44 | - | $\checkmark$
U45 | - | $\checkmark$
U46 | - | $\checkmark$
U48 | - | $\checkmark$
U49 | - | $\checkmark$
U50 | - | $\checkmark$
U51 | - | $\checkmark$
U53 | - | $\checkmark$
U54 | - | $\checkmark$
U56 | - | $\checkmark$
U57 | $\checkmark$ | $\checkmark$
U61 | - | $\checkmark$
U62 | - | $\checkmark$
U64 | - | $\checkmark$
U66 | - | $\checkmark$
U67 | - | $\checkmark$
U68 | - | $\checkmark$
U71 | $\checkmark$ | $\checkmark$
U72 | - | $\checkmark$
U75 | - | $\checkmark$
U76 | - | $\checkmark$
U79 | $\checkmark$ | $\checkmark$
U81 | $\checkmark$ | $\checkmark$
U82 | $\checkmark$ | $\checkmark$
U87 | - | $\checkmark$
U89 | - | $\checkmark$
U90 | - | $\checkmark$
U91 | - | $\checkmark$
U92 | - | $\checkmark$
U93 | - | $\checkmark$
(b)

We report results of the template-and-qe method (Section 3) on the benchmark
presented in Section 2. The lazy extension of our approach (Section 3.2.1) was
left for future work.

The template verification (Section 3.1) has proven to be the most difficult
task. Table LABEL:tab:gencov 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 $\times$ symbol in
Table LABEL:tab:gencov). These satisfiable problems are nontrivial because
they involve creating a counterexample to the template. For this purpose, we
also ran the SyGuS approach666option \--sygus-inference of cvc5 and its linear
model builder [17].

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. Table 0(b) 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.777https://sat.inesc-id.pt/~mikolas/sc2_2024/

##  5 Conclusions and Future Work

This paper joins the effort of rising up to the challenge of making computers
as powerful as are the golden medalist at the International Math Olympics
(IMO). Efforts such as AlphaGeometry [18], 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 [19]. 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 difficulty 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 [20]. 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 different synthesis
approaches, e.g., such as those that are realized in saturation-based solvers
[21, 22] or inside SMT solvers [23, 24, 25] or inductive logic programming
[26]. The challenge here would be how to come up with all the solutions.

###### Acknowledgements.

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.

## References

  * Musil [2024] V. Musil, Funkcionální rovnice, 2024\. URL: https://prase.cz/library/FunkcionalniRovniceVM/FunkcionalniRovniceVM.pdf, downloaded 8 March 2024.
  * Barbosa et al. [2022] H. Barbosa, C. W. Barrett, M. Brain, G. Kremer, H. Lachnitt, M. Mann, A. Mohamed, M. Mohamed, A. Niemetz, A. Nötzli, A. Ozdemir, M. Preiner, A. Reynolds, Y. Sheng, C. Tinelli, Y. Zohar,  cvc5: A versatile and industrial-strength SMT solver,  in: Tools and Algorithms for the Construction and Analysis of Systems, TACAS, volume 13243 of LNCS, Springer, 2022, pp. 415–442. doi:10.1007/978-3-030-99524-9_24.
  * de Moura and Bjørner [2008] L. M. de Moura, N. Bjørner,  Z3: an efficient SMT solver,  in: Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, volume 4963, Springer, 2008, pp. 337–340. doi:10.1007/978-3-540-78800-3_24.
  * Kovács and Voronkov [2013] 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 Lecture Notes in Computer Science, Springer, 2013, pp. 1–35. doi:10.1007/978-3-642-39799-8_1.
  * Hillenbrand and Löchner [2002] 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.
  * Barrett et al. [2017] 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.
  * Bachmair et al. [1989] L. Bachmair, N. Dershowitz, D. A. Plaisted,  Completion without failure,  in: Rewriting Techniques, Elsevier, 1989, pp. 1–30.
  * Collins [1975] 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, Berlin, Heidelberg, 1975, pp. 134–183.
  * Cooper [1972] D. C. Cooper,  Theorem proving in arithmetic without multiplication,  Machine intelligence 7 (1972) 300.
  * Ferrante and Rackoff [1975] J. Ferrante, C. Rackoff,  A decision procedure for the first order theory of real addition with order,  SIAM Journal on Computing 4 (1975) 69–76. URL: https://doi.org/10.1137/0204006. doi:10.1137/0204006.
  * Loos and Weispfenning [1993] R. Loos, V. Weispfenning,  Applying linear quantifier elimination,  Comput. J. 36 (1993) 450–462. doi:10.1093/COMJNL/36.5.450.
  * Davenport et al. [1993] J. H. Davenport, Y. Siret, E. Tournier, Computer algebra - systems and algorithms for algebraic computation (2. ed.), Academic Press, 1993.
  * Bradley and Manna [2007] 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.
  * Bjørner and Janota [2015] N. S. Bjørner, M. Janota,  Playing with quantified satisfaction,  in: LPAR, EasyChair, 2015, pp. 15–27. doi:10.29007/VV21.
  * Vale-Enriquez and Brown [2018] 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 2018 - 6th International Conference, South Bend, IN, USA, July 24-27, 2018, Proceedings, volume 10931 of Lecture Notes in Computer Science, Springer, 2018, pp. 466–474. doi:10.1007/978-3-319-96418-8_55.
  * Collins and Hong [1991] 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.
  * Janota et al. [2023] 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.
  * Trinh et al. [2024] 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.
  * Sinha et al. [2024] 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.
  * Srivastava et al. [2013] 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.
  * Hozzová et al. [2023] P. Hozzová, L. Kovács, C. Norman, A. Voronkov,  Program synthesis in saturation,  in: B. Pientka, C. Tinelli (Eds.), Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings, volume 14132 of Lecture Notes in Computer Science, Springer, 2023, pp. 307–324. doi:10.1007/978-3-031-38499-8_18.
  * Hozzová et al. [2024] P. Hozzová, D. Amrollahi, M. Hajdu, L. Kovács, A. Voronkov, E. M. Wagner,  Synthesis of recursive programs in saturation,  in: International Joint Conference on Automated Reasoning IJCAR, 2024.
  * Reynolds et al. [2019] 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.
  * Abate et al. [2023] 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.
  * Barbosa et al. [2019] H. Barbosa, A. Reynolds, D. Larraz, C. Tinelli,  Extending enumerative function synthesis via SMT-driven classification,  in: C. W. Barrett, J. Yang (Eds.), 2019 Formal Methods in Computer Aided Design, FMCAD 2019, San Jose, CA, USA, October 22-25, 2019, IEEE, 2019, pp. 212–220. doi:10.23919/FMCAD.2019.8894267.
  * Cerna and Cropper [2024] D. M. Cerna, A. Cropper,  Generalisation through negation and predicate invention,  Proceedings of the AAAI Conference on Artificial Intelligence 38 (2024) 10467–10475. URL: https://ojs.aaai.org/index.php/AAAI/article/view/28915. doi:10.1609/aaai.v38i9.28915.


[a]Giuseppe De Laurentis

# Constructing Compact Ansätze for Scattering Amplitudes

Ben Page

###### Abstract

In these proceedings, we discuss the recent approach of Ref. [1] for the
construction of compact Ansätze for scattering amplitudes. The method builds
powerful constraints on the analytic structure of the rational functions in
amplitudes from numerical tests of their behavior close to singularity
surfaces. We discuss how we systematically understand these surfaces and how
the singular behavior of the rational function can be incorporated into an
Ansatz using techniques from algebraic geometry. To perform the numerical
sampling, we make use of $p$-adic numbers, a number-theoretical field that can
be considered a cousin of finite fields. The $p$-adic numbers admit a non-
trivial absolute value, as well as analytic functions such as the $p$-adic
logarithm. We provide a detailed example of the approach applied to an NMHV
tree amplitude and discuss the efficacy when applied to the two-loop leading-
color amplitude for three-photon production at hadron colliders.

##  1 Introduction

Meeting the calculational requirements of modern hadron collider experiments
is theoretically very demanding. Due to the high precision projected at the
LHC, it is necessary to push fixed-order cross-section computations to NNLO
QCD precision for a variety of multi-scale observables, see e.g. [2]. Many
such predictions require the computation of two-loop QCD scattering amplitudes
with five external particles. In recent years, we have seen impressive
advances in computational techniques that have allowed the calculation of many
two-loop amplitudes involving five massless particles [3, 4, 5, 6, 7, 8, 9,
10, 11, 12, 13, 14, 15, 16, 17, 18] as well as a number involving four
massless and a single massive particle [19, 20, 21, 22].

In the modern approach, scattering amplitudes are computed in a divide-and-
conquer fashion, where they are broken down into a linear combination of
special functions, whose coefficients depend rationally on the external
kinematics. The special functions and rational coefficients are then computed
separately. In recent multi-scale loop calculations, this is often considered
at the level of the finite remainder. Specifically, after ultra-violet
renormalization, one can subtract away the infra-red poles to define a finite
remainder $\mathcal{H}_{n}^{(l)}$ [23, 24, 25, 26]

$\mathcal{A}^{(l)}_{n,R}=\sum_{l^{\prime}=0}^{l-1}{\bf
I}^{(l-l^{\prime})}_{\epsilon}\mathcal{A}^{(l^{\prime})}_{n,R}+\mathcal{H}_{n}^{(l)}+\mathcal{O}(\epsilon)\,.$
(1)

This finite remainder admits a decomposition into a basis of special functions
as

$\mathcal{H}_{n}^{(l)}=\sum_{i}\;{\mathcal{C}_{i}(\lambda,\tilde{\lambda})}\;\times\;F_{i}(\lambda,\tilde{\lambda})\,.$
(2)

The special functions $F_{i}$ can be constructed in a way that depends only on
the kinematics of the process under study, see, e.g. the recent development of
sets of pentagon functions [27, 28, 29]. However, the coefficients
$\mathcal{C}_{i}$ are complicated process-dependent rational functions. In
recent years, a new paradigm has emerged which has enabled an explosion of
computations of multi-scale amplitudes. In short, one writes an Ansatz for the
$\mathcal{C}_{i}$, and fixes the unknown parameters from numerical evaluations
over finite fields [30, 31].

As we look towards amplitudes which depend on an increased number of scales,
we see that the number of unknowns in the frequently used “common denominator”
Ansatz is growing significantly, as one can see in Table 1. This has motivated
us to search for a strategy for constructing improved Ansätze for the rational
coefficients in QCD scattering amplitudes.

| $\mathcal{H}^{(2)}_{pp\rightarrow jjj}$ | $\mathcal{H}^{(2)}_{pp\rightarrow\gamma\gamma\gamma}$ | $\mathcal{H}^{(2)}_{pp\rightarrow W+2j}$ | $\mathcal{A}^{(1)}_{0\rightarrow 6g}+\mathcal{O}(\epsilon)$
---|---|---|---|---
Ref. | [9] | [12, 13] | [19] | [32]
Ansatz size | $\mathcal{O}(10^{5})$ | $\mathcal{O}(10^{5})$ | $\mathcal{O}(10^{7})^{(*)}$ | $\mathcal{O}(10^{9})$

Table 1: Ansatz size for the numerators when written in common denominator
form.
(∗) Reduced to $\mathcal{O}(10^{6})$ after the univariate partial-fraction
decomposition of Ref. [20].

In recent years, it has been observed that if the rational prefactors
$\mathcal{C}_{i}$ are cast in a multivariate partial fractions decomposition,
significant cancellations occur (see e.g. Ref. [33]). However, in practice,
these simplifications are achieved after first reconstructing the result in a
less compact form. In this talk, we discuss the approach of Ref. [1], where an
Ansatz inspired by the structure of a partial fractions decomposition is
constructed from numerical evaluations in singular limits. In practice, these
Ansätze exhibit a reduced number of free parameters in comparison to the
corresponding common denominator form and thereby significantly reduce the
computational cost of analytic reconstruction.

##  2 Ansatz Construction Approach

To introduce our strategy, let us consider the 6-point NMHV tree amplitude
$A_{0\rightarrow q^{+}g^{+}g^{+}\bar{q}^{-}g^{-}g^{-}}$. We work with the
assumption that we do not know its analytical form, as if we were numerically
computing a loop-integral coefficient. The least common denominator is easily
obtained from numerical evaluations, thus we can write

$A_{0\rightarrow
q^{+}g^{+}g^{+}\bar{q}^{-}g^{-}g^{-}}=\frac{\mathcal{N}}{\langle
12\rangle\langle 23\rangle\langle 34\rangle[45][56][61]s_{345}}\,,$ (3)

where $\mathcal{N}$ is an unknown polynomial in spinor brackets. That is,
$\mathcal{N}$ belongs to a vector space $\mathcal{M}_{d,\vec{\phi}}$ spanned
by spinor-bracket monomials of appropriate mass dimension $d$ and little-group
weights $\vec{\phi}$. The mass dimension (6) as well as the little-group
weights (-1, 0, 0, 1, 0, 0) of $\mathcal{N}$ are easily obtained, thus we have

$\mathcal{N}\in\mathcal{M}_{6,[-1,0,0,1,0,0]}\,,\quad\text{where}\quad\text{dim}(\mathcal{M}_{6,[-1,0,0,1,0,0]})=143\,.$
(4)

We aim to construct an Ansatz for $\mathcal{N}$, based on the expectation that
the result can be cast in some partial-fractioned form, where the numerator
has been partially cancelled against the denominator. For example, if we are
able to show that $\mathcal{N}$ can be written in the form

$\mathcal{N}=n_{12}\langle 12\rangle+n_{23}\langle 23\rangle\,,$ (5)

then we can cancel this against factors of $\langle 12\rangle$ and $\langle
23\rangle$ in the denominator. In Ref. [32], it was suggested that the
validity of such a decomposition can be deduced from evaluations of the
amplitude on phase-space points where $\langle 12\rangle$ and $\langle
23\rangle$ are $\mathcal{O}(\epsilon)$, for some small quantity $\epsilon$.
Note that there are actually two separate possibilities to achieve this,
either the spinor $\lambda_{2}$ is nearly soft, or the spinors $\lambda_{1}$,
$\lambda_{2}$ and $\lambda_{3}$ are simultaneously almost collinear. In
practice, for $A_{0\rightarrow q^{+}g^{+}g^{+}\bar{q}^{-}g^{-}g^{-}}$ one
finds that

$\displaystyle\begin{split}\lambda_{2}&\sim\epsilon\Rightarrow\mathcal{N}\sim\epsilon^{0},\\\
\langle 12\rangle\sim\langle 23\rangle\sim\langle
13\rangle&\sim\epsilon\Rightarrow\mathcal{N}\sim\epsilon^{1}.\end{split}$ (6)

Therefore, the tentative decomposition of Eq. (5) does not hold. Nevertheless,
we still have found a constraint from the vanishing of the numerator on the
simultaneously collinear surface. It can be shown that the subspace of
$\mathcal{M}_{d,\vec{\phi}}$ that satisfies this constraint has dimension 84,
i.e. 1 evaluation fixed 59 parameters. We naturally wish to incorporate this
style of constraint into an Ansatz. To systematize this strategy, we therefore
find ourselves needing to answer a number of questions:

  * •

How do we understand the different ways in which we can set the denominators
small?

  * •

How do we numerically obtain the degree of vanishing for the $\mathcal{C}_{i}$
in two-loop amplitudes?

  * •

How do we incorporate into an Ansatz the constraints provided by the vanishing
of $\mathcal{N}$?

Let us consider these problems one by one.

###  2.1 Branching of singular varieties

First, we interpret the task of numerically setting a pair of denominators
$\mathcal{D}_{i}$ and $\mathcal{D}_{j}$ to be small as finding phase-space
points which are close to the surfaces where the denominators are zero. That
is, we are interested in understanding the solutions of

$\mathcal{D}_{i}=\mathcal{D}_{j}=0.$ (7)

These are surfaces defined by the zero sets of polynomials and are known as
algebraic varieties. The fact that there are different ways of setting the
denominators small corresponds to the fact that these varieties may have
multiple branches. More mathematically, varieties associated to pairs of
denominator factors may be reducible.

A variety is said to be irreducible if it cannot be written as the union of
simpler varieties, i.e. $U$ is irreducible if $U=U_{1}\cup U_{2}$ implies
$U_{1}=U$ or $U_{2}=U$. A variety $U$ admits a minimal decomposition in terms
of irreducible varieties $U_{k}$,

$U=\bigcup_{k=1}^{n_{B}(U)}U_{k}\quad\text{s.t.}\quad U_{i}\not\subseteq
U_{j}\;\forall\;i\neq j.$ (8)

In Fig. 1 we provide simple, graphical examples of irreducible and reducible
varieties in $\mathbb{R}^{3}$.

(a) $V(\langle xy^{2}+y^{3}-z^{2}\rangle)$

(b) $V(\langle x^{3}+y^{3}-z^{2}\rangle)$

(c) $V(\langle xy^{2}+y^{3}-z^{2},x^{3}+y^{3}-z^{2}\rangle)$

Figure 1: Two irreducible codimension-one varieties in Fig. 1(a) and Fig.
1(b),
and the three branches of their reducible codimension-two intersection in Fig.
1(c).

In higher dimensions, the reducibility of a given variety may be non-trivial
to detect from its defining polynomials. In order to systematically approach
the problem of determining the branches of a variety, we formulate the problem
algebraically. Specifically, to the varieties $U$ and $U_{k}$ in the
decomposition in Eq. (8), we associate the algebraic ideals, $I(U)$ and
$I(U_{k})$ respectively. In this language, the decomposition is translated to

$I(U)=\bigcap_{k=1}^{n_{B}(U)}I(U_{k}).$ (9)

The task of describing the branching of $U$ now becomes the task of finding
generators for each of the $I(U_{k})$. As described in Ref. [1], this can be
achieved by applying primary decomposition techniques to the ideal
$\langle\mathcal{D}_{i},\mathcal{D}_{j}\rangle_{R_{n}}$, making use of the
computer algebra system Singular [34].

Returning to the motivating example, we see that the fact that there are two
ways to make $\langle 12\rangle$ and $\langle 23\rangle$ simultaneously small
algebraically corresponds to the primary decomposition

$\big{\langle}\langle 12\rangle,\langle
23\rangle\big{\rangle}_{R_{6}}=\big{\langle}\langle 12\rangle,\langle
23\rangle,\langle
13\rangle\big{\rangle}_{R_{6}}\cap\langle\lambda_{2}^{\alpha}\rangle_{R_{6}}.$
(10)

To be able to numerically check if numerator decompositions of the form of Eq.
(5) apply for any pair of denominators, it is necessary to compute the primary
decompositions of all ideals generated by such pairs. In Ref. [1] we perform
this for all singularities arising from symbol letters for two-loop five-point
massless processes.

###  2.2 $\boldsymbol{p}$-adic numbers

Next, we discuss our approach for the sampling of the rational functions
$\mathcal{C}_{i}$ close to varieties where a pair of denominators are zero. To
this end we make use of the $p$-adic numbers $\mathbb{Q}_{p}$, which can be
thought of as a close cousin of a finite field $\mathbb{F}_{p}$ and inherit
some of their stability properties. A $p$-adic number $x$ can be defined in
terms of a formal series in powers of a prime number $p$,

$x=\sum_{i=\nu_{p}(x)}^{\infty}a_{i}p^{i}=a_{\nu_{p}(x)}p^{\nu_{p}(x)}+\cdots+a_{-1}p^{-1}+a_{0}+a_{1}p+a_{2}p^{2}+\cdots\,,$
(11)

where $\nu_{p}(x)$ is called the valuation of $x$, and $a_{\nu_{p}(x)}\neq 0$.
The subset of $\mathbb{Q}_{p}$ with $\nu_{p}(x)=0$ is known as the set of
$p$-adic integers $\mathbb{Z}_{p}$.

An important feature of $\mathbb{Q}_{p}$ is that it admits a non-trivial
absolute value,

$|x|_{p}=p^{-\nu_{p}(x)}\quad\Longrightarrow\quad|p|_{p}<|1|_{p}<\left|\frac{1}{p}\right|_{p}.$
(12)

In contrast to $\mathbb{F}_{p}$, this allows one to find numerical
configurations such that the a pair of denominators are small by building a
$p$-adic phase-space point near varieties. In practice, we first find a
finite-finite-valued phase-space point on the variety exactly. Then, we lift
the $\mathbb{F}_{p}$ solution to an approximate $p$-adic solution. Further
details are described in Ref. [1].

With the non-trivial absolute value on $\mathbb{Q}_{p}$, one can also
introduce functions defined through power series. As an example, let us
discuss the $p$-adic logarithm. This can be defined from the Taylor expansion
around $x=1$, that is

$\log_{p}(1+x)=\sum_{k=1}^{\infty}\frac{(-1)^{k+1}x^{k}}{k}\,,$ (13)

which converges for $|x|_{p}<1$, that is for $p$-adic numbers $x$ with
$\nu_{p}(x)\geq 1$. To continue the logarithm outside of the radius of
convergence of Eq. (13), we can make use of the following trick. We first
recall that the logarithm relates products to sums. That is, for any $a,b$ in
$\mathbb{Q}_{p}$

$\log_{p}(ab)=\log_{p}(a)+\log_{p}(b)\,.$ (14)

Next, we remind ourselves of Fermat’s little theorem: for an integer $w$, one
can show that

$w^{p-1}=1\;\,\text{mod}\;\,p\,.$ (15)

In $\mathbb{Z}_{p}$ we see that this implies that $|w^{p-1}-1|_{p}<1$. We can
therefore apply the identity of Eq. (14) to rewrite

$\log_{p}(w)=\frac{\log_{p}(w^{p-1})}{p-1}.$ (16)

Now the argument of the logarithm on the right hand side of Eq. (16) is within
the radius of convergence. We observe that computing the $p$-adic logarithm to
low precision can be implemented efficiently by computing the exponentiation
in Eq. (16) by the approach of repeated squaring. Given that, for large $p$,
linear algebra modulo $p^{k}$ is very stable, we expect applications to
efficiently find linear relations between logarithms of products of functions,
e.g. as often required in applications of the symbol calculus.

###  2.3 Constructing Compact Ansätze

Given the ability to classify all irreducible singular varieties associated to
the amplitude, and to $p$-adically evaluate the rational functions close to
these varieties, it remains to mathematically understand the constraint that
this places for us on the numerator. We will then use these constraints to
construct compact Ansätze for the rational functions.

First, we note that we make the assumption that if the numerator vanishes to a
given degree on a single such configuration, that this is a property of the
numerator on the entire variety, not just this point. This allows us to make
use of a tool from algebraic geometry: the so-called “Zariski-Nagata” theorem
[35, 36, 37]. Schematically, the theorem states that the set of polynomials
which vanish to $k^{\text{th}}$ order on a variety $U$ is given by the
$k^{\mathrm{th}}$ “symbolic power” of the ideal associated to the variety,
$I(U)^{\langle k\rangle}$. That is, for a point
$(\eta^{(\epsilon)},\tilde{\eta}^{(\epsilon)})$ near a variety $U$ one has
that

$\mathcal{N}(\eta^{(\epsilon)},\tilde{\eta}^{(\epsilon)})=\mathcal{O}(\epsilon^{k})\;\;\Rightarrow\;\;\mathcal{N}\in
I(U)^{\langle k\rangle}.$ (17)

The symbolic power of an ideal is strongly related to the standard power of an
ideal, and in Ref. [1] we give a number of strategies for computing a
generating set of symbolic powers.

Given a collection of varieties $\mathcal{V}=\\{U_{1},\ldots,U_{n}\\}$, we
determine $\kappa(\mathcal{N},U_{i})$, the degree of vanishing of
$\mathcal{N}$ on each of these varieties. This tells us that the numerator is
a member of the ideal

$\mathcal{N}\in\mathfrak{J},\quad\text{where}\quad\mathfrak{J}=\bigcap_{U\in\mathcal{V}}I(U)^{\langle\kappa(\mathcal{N},U)\rangle}.$
(18)

From knowledge of the mass dimension and little group weights of the
numerator, we now know that
$\mathcal{N}\in\mathcal{M}_{d,\vec{\phi}}\cap\mathfrak{J}$. This is a finite-
dimensional vector space, in which every element has the same vanishing
properties as $\mathcal{N}$. Therefore, we take a basis of this space to be
our Ansatz for the numerator $\mathcal{N}$. In Ref. [1] we constructed a basis
of this vector space using Gröbner basis and linear algebra techniques.

##  3 Examples

In order to demonstrate the details of our approach, as well as its impact
when constructing compact Ansätze for two-loop amplitudes, we will now discuss
two examples. First we describe in detail an application to the color-ordered
tree amplitude $A_{0\rightarrow q^{+}g^{+}g^{+}\bar{q}^{-}g^{-}g^{-}}$
introduced in Eq. (3). Second, we will summarize the result of an analogous
procedure applied to two-loop finite reminders for the process
$q\bar{q}\rightarrow\gamma\gamma\gamma$.

###  3.1 A six-point NMHV tree from its poles and zeros

Returning to $A_{0\rightarrow q^{+}g^{+}g^{+}\bar{q}^{-}g^{-}g^{-}}$ of Eq.
(3), we examine the behavior of $\mathcal{N}$ on irreducible codimension-two
varieties where pairs of invariants vanish. Specifically, we consider those
corresponding to physical singularities, that is $\langle ij\rangle$, $[ij]$
and $s_{ijk}$. Up to permutations and parity, there are 8 inequivalent pairs
of these invariants. In other words, there are 8 inequivalent, possibly
reducible, codimension-two varieties. The corresponding ideals are given by

$\displaystyle J_{1}\overset{!}{=}\big{\langle}\langle 12\rangle,\langle
13\rangle\big{\rangle}_{R_{6}}=P_{1}\cap P_{2}\,,$ $\displaystyle
J_{5}\overset{!}{=}\big{\langle}\langle
12\rangle,[34]\big{\rangle}_{R_{6}}=P_{6}\,,$ (19) $\displaystyle
J_{2}\overset{!}{=}\big{\langle}\langle 12\rangle,\langle
34\rangle\big{\rangle}_{R_{6}}=P_{3}\,,$ $\displaystyle
J_{6}\overset{!}{=}\big{\langle}\langle
12\rangle,s_{123}\big{\rangle}_{R_{6}}=P_{1}\cap P_{7}\,,$ $\displaystyle
J_{3}\overset{!}{=}\big{\langle}\langle
12\rangle,[12]\big{\rangle}_{R_{6}}=P_{4}\,,$ $\displaystyle
J_{7}\overset{!}{=}\big{\langle}\langle
12\rangle,s_{134}\big{\rangle}_{R_{6}}=P_{8}\,,$ $\displaystyle
J_{4}\overset{!}{=}\big{\langle}\langle
12\rangle,[13]\big{\rangle}_{R_{6}}=P_{5}\,,$ $\displaystyle
J_{8}\overset{!}{=}\big{\langle}s_{123},s_{124}\big{\rangle}_{R_{6}}=P_{9}\,.$

The right-hand sides provide primary decompositions for the $J_{i}$ and all
ideals denoted as $P_{i}$ are prime. The ones which do not directly correspond
to the $J_{i}$ ideals are

$\displaystyle P_{1}=\big{\langle}\langle 12\rangle,\langle 13\rangle,\langle
23\rangle\big{\rangle}_{R_{6}}\,,\quad
P_{2}=\big{\langle}\lambda_{1}^{\alpha}\big{\rangle}_{R_{6}}\,,\quad
P_{7}=\big{\langle}\langle
12\rangle,\lambda_{1}^{\alpha}[13]+\lambda_{2}^{\alpha}[23]\big{\rangle}_{R_{6}}\,.$
(20)

We now sample the numerator of the NMHV amplitude on phase space points near
to the set of codimension-two varieties. In practice, we observe that on 28 of
these varieties the numerator vanishes. On 2 of these 28 it vanishes
quadratically, while on the remaining ones it vanishes linearly. By
application of Eq. (18), we have $\mathcal{N}\in\mathfrak{J}$, where
$\mathfrak{J}$ is

$\displaystyle\mathfrak{J}=\Big{[}P_{1}\\!\cap\\!\overline{P}_{1}^{\langle
2\rangle}\\!\\!\cap\\!P_{1}(216543)\\!\cap\\!\overline{P}_{1}(216543)\\!\cap\\!P_{1}(432165)\\!\cap\\!\overline{P}_{2}\\!\cap\\!P_{3}\\!\cap\\!P_{5}(126345)\\!\cap\\!P_{6}(432165)$
$\displaystyle\phantom{\Big{[}}\\!\cap\\!P_{7}\\!\cap\\!\overline{P}_{7}\\!\cap\\!P_{7}(321654)\\!\cap\\!P_{7}(543216)\\!\cap\\!P_{8}(231654)\Big{]}\cap\Big{[}123456\rightarrow\overline{456123}\Big{]}\,,$
(21)

where we have made use of the anti-symmetry of the amplitude
($\overline{456123}$) to write the intersection of 28 ideals in terms of two
related sets of 14. The arguments of the ideals denote permutations of the
external legs in the one-line notation $(\sigma(1)\dots\sigma(6))$, and an
overline denotes the swap
$\lambda_{i,\alpha}\leftrightarrow\bar{\lambda}_{i,\dot{\alpha}}$. The only
second symbolic power that is needed is of the prime ideal $P_{1}$ (or
permutations thereof). In this case, it can be shown that $P_{1}^{\langle
2\rangle}=P_{1}^{2}$, i.e. the second symbolic power is easily computed as it
coincides with the second (standard) power.

It is useful to write $\mathfrak{J}$ in terms of ideals generated by two
polynomials to see the connection to partial fractions. Specifically, we can
write $\mathfrak{J}$ as111We note that the argument of each square bracket is
not in one-to-one correspondence with that of Eq. (21).

$\displaystyle\mathfrak{J}=\;$
$\displaystyle\Big{[}\big{\langle}[12],[13],[23]\big{\rangle}_{R_{6}}^{2}\cap\big{\langle}\langle
12\rangle,\langle 34\rangle\big{\rangle}_{R_{6}}\cap\big{\langle}\langle
12\rangle,[16]\big{\rangle}_{R_{6}}\cap\big{\langle}\langle
34\rangle,[12]\big{\rangle}_{R_{6}}\cap\big{\langle}[12],[13]\big{\rangle}_{R_{6}}$
$\displaystyle\phantom{\Big{[}}\cap\big{\langle}[15],[16]\big{\rangle}_{R_{6}}\cap\big{\langle}\langle
23\rangle,s_{345}\big{\rangle}_{R_{6}}\cap\big{\langle}\langle
12\rangle,s_{123}\big{\rangle}_{R_{6}}\cap\big{\langle}[12],s_{123}\big{\rangle}_{R_{6}}\cap\big{\langle}[12],s_{345}\big{\rangle}_{R_{6}}$
$\displaystyle\phantom{\Big{[}}\cap\big{\langle}\langle
4|2+3|1],s_{123}\big{\rangle}_{R_{6}}\cap\big{\langle}\langle
6|1+2|3],s_{345}\big{\rangle}_{R_{6}}\Big{]}\cap\Big{[}123456\rightarrow\overline{456123}\Big{]}\,,$
(22)

where we have also used the primary decomposition

$\big{\langle}\langle 1|3+4|2],s_{134}\big{\rangle}_{R_{6}}=P_{1}(134256)\cap
P_{1}(\overline{256134})\cap P_{7}(\overline{341562})\cap P_{7}(562341)\,.$
(23)

Interestingly, this involves a spinor chain despite it not being part of the
initial set of singularities. Some of these intersections can be further
carried out compactly,

$\displaystyle\mathfrak{J}=\;$
$\displaystyle\Big{[}\big{\langle}[12],[13],[23]\big{\rangle}_{R_{6}}^{2}\cap\big{\langle}s_{12},\langle
34\rangle[16][12],\langle 34\rangle\langle 12\rangle[13],\langle
34\rangle[13][16],[16][23]\langle 34\rangle\big{\rangle}_{R_{6}}$
$\displaystyle\phantom{\Big{[}}\cap\big{\langle}\langle 23\rangle[15],\langle
23\rangle[16],[16]s_{345},[15]s_{345}\big{\rangle}_{R_{6}}\cap\big{\langle}\langle
12\rangle[12],[12]s_{123},s_{123}s_{345}\big{\rangle}_{R_{6}}$
$\displaystyle\phantom{\Big{[}}\cap\big{\langle}\langle
4|2+3|1],s_{123}\big{\rangle}_{R_{6}}\cap\big{\langle}\langle
6|1+2|3],s_{345}\big{\rangle}_{R_{6}}\Big{]}\cap\Big{[}123456\rightarrow\overline{456123}\Big{]}\,.$
(24)

Importantly, such a representation would allow the approach of Ref. [1] to
compute $\mathcal{M}_{d,\vec{\phi}}\cap\mathfrak{J}$ more efficiently.

Nevertheless, in this simple example, we can compute the intersection
$\mathcal{M}_{d,\vec{\phi}}\cap\mathfrak{J}$ directly by explicitly computing
$\mathfrak{J}$ from one of the above Eqs. (21), (3.1) or (3.1) up to the
required mass dimension $d=6$. This can be done with Singular by setting an
appropriate degree bound (degBound). The resulting Ansatz is completely fixed,
up to an overall numerical prefactor $c_{0}$,

$\displaystyle\mathcal{M}_{d,\vec{\phi}}\cap\mathfrak{J}=c_{0}\big{(}\langle
12\rangle[12]\langle 45\rangle[45]\langle 4|2+3|1]+[16]\langle
34\rangle\langle 6|1+2|3]s_{123}\big{)}\,.$ (25)

Interestingly, we have shown that $A^{(0)}_{0\rightarrow
q^{+}g^{+}g^{+}\bar{q}^{-}g^{-}g^{-}}$ is in fact the unique function with the
given zeros and poles in complex phase space. In general, when considering
rational coefficients of master integrals or of special transcendental
functions, the ansatz obtained from $\mathcal{M}\cap\mathfrak{J}$ may still
contain several terms, rather than a single one. Nevertheless, the imposed
constraints are significant.

###  3.2 Application to Leading-Color Two-Loop Tri-Photon Production
Amplitudes

The strategy of Ref. [1] was constructed in order to decrease the number of
samples required when computing two-loop multi-scale scattering amplitudes. In
order to show the benefits of our approach in a two-loop five-point context,
we applied it to the finite remainders of the two-loop three-photon production
amplitudes of Ref. [13]. Working with the analytic form of these results, we
sampled them close to all codimension-two varieties where the amplitude
exhibits a (potentially spurious) singularity. We therefore used $317$
$p$-adic evaluations to construct the Ansätze. In Table 2, we characterize the
improvements that our strategy provides in terms of the number of free
parameters of the Ansatz. Comparing the size of the Ansatz used in Ref. [13],
$\mathrm{dim}(\mathcal{M}_{\tilde{d},\vec{0}})$, with the size of Ansatz in
spinor variables taking into account numerator vanishing constraints,
$\mathrm{dim}(\mathcal{M}_{d,\vec{\phi}})\cap\mathfrak{J}$, we see an
improvement of a factor of $73$ in the worst case.

Remainder |  | vector space:
---
Mandelstam Ansatz
| dim. of
---
$\mathcal{M}_{\tilde{d},\vec{0}}$
| vector space:
---
spinor Ansatz
| dim. of
---
$\mathcal{M}_{d,\vec{\phi}}$
| dim. of
---
$\mathcal{M}_{d,\vec{\phi}}\cap\mathfrak{J}$
ratio
$R^{\\{2,0\\}}_{\gamma^{-}\gamma^{+}\gamma^{+}}$ | $\mathcal{M}_{\\{50,\vec{0}\\}}$ | 41301 | $\mathcal{M}_{35,\\{3,0,6,-3,-2\\}}$ | 7358 | 566 | 73
$R^{\\{2,N_{f}\\}}_{\gamma^{-}\gamma^{+}\gamma^{+}}$ | $\mathcal{M}_{\\{24,\vec{0}\\}}$ | 2821 | $\mathcal{M}_{15,\\{-2,-2,0,-3,-3\\}}$ | 378 | 20 | 141
$R^{\\{2,0\\}}_{\gamma^{+}\gamma^{+}\gamma^{+}}$ | $\mathcal{M}_{\\{32,\vec{0}\\}}$ | 7905 | $\mathcal{M}_{20,\\{-2,-4,-2,-2,-2\\}}$ | 1140 | 18 | 439
$R^{\\{2,N_{f}\\}}_{\gamma^{+}\gamma^{+}\gamma^{+}}$ | $\mathcal{M}_{\\{18,\vec{0}\\}}$ | 1045 | $\mathcal{M}_{8,\\{1,3,1,1,2\\}}$ | 44 | 6 | 174
Table 2: Characterizing data for Mandelstam, spinor and refined spinor
Ansätze. Spinor helicity variables alone can be seen to reduce the size of the
Ansatz by almost an order of magnitude. The size is reduced by a further order
of magnitude by imposing the numerator vanishing constraints on codimension-
two varieties.

##  4 Conclusion and Summary

Modern methods for multi-scale two-loop scattering-amplitude computation
employ Ansätze and numerical sampling to determine rational coefficients of
special functions. The major bottleneck in this approach is the number of
numerical samples required, which is dictated by the number of free parameters
in the Ansätze. In this talk we discussed a strategy for building compact
Ansätze. Specifically, we build Ansätze that match the behavior of the
rational coefficients near varieties where amplitudes exhibit (potentially
spurious) singularities. It turns out that these varieties may branch, and so
we discussed a set of computational tools that one can use to describe this
branching. We determine the behavior of the coefficients near irreducible
varieties from numerical evaluations. To perform these evaluations we
introduced the $p$-adic numbers, a cousin of finite fields which allow one to
construct phase-space points close to a given variety. Interestingly, the
$p$-adic numbers admit a theory of calculus, allowing one to discuss functions
defined through power series such as the $p$-adic logarithm. With the behavior
of the coefficients in singular regions in hand, we then discussed how to
interpret the degree of vanishing on the numerator on such varieties
algebraically. This then allows us to construct a complete Ansatz matching
this behavior. To discuss our approach in practice, we looked at the example
of a six-point NMHV tree amplitude and built an Ansatz that required only one
sample to determine the full analytic result. Thereafter, we demonstrated the
impact of our strategy on a proof-of-concept two-loop example, the leading-
color amplitudes for three-photon production at hadron colliders. We look
forward to applying this approach to scattering amplitudes involving an
increasingly higher number of scales in the future.

## References

  * [1] G. De Laurentis and B. Page, _Ansätze for Scattering Amplitudes from $p$-adic Numbers and Algebraic Geometry_, 2203.04269.
  * [2] A. Huss, J. Huston, S. Jones and M. Pellen, _Les Houches 2021: Physics at TeV Colliders: Report on the Standard Model Precision Wishlist_ , 2207.02122.
  * [3] S. Abreu, L. J. Dixon, E. Herrmann, B. Page and M. Zeng, _The two-loop five-point amplitude in $\mathcal{N}=4$ super-Yang-Mills theory_, _Phys. Rev. Lett._ 122 (2019) 121603 [1812.08941].
  * [4] D. Chicherin, T. Gehrmann, J. M. Henn, P. Wasser, Y. Zhang and S. Zoia, _Analytic result for a two-loop five-particle amplitude_ , _Phys. Rev. Lett._ 122 (2019) 121602 [1812.11057].
  * [5] S. Abreu, L. J. Dixon, E. Herrmann, B. Page and M. Zeng, _The two-loop five-point amplitude in $\mathcal{N}$ = 8 supergravity_, _JHEP_ 03 (2019) 123 [1901.08563].
  * [6] D. Chicherin, T. Gehrmann, J. M. Henn, P. Wasser, Y. Zhang and S. Zoia, _The two-loop five-particle amplitude in $\mathcal{N}$ = 8 supergravity_, _JHEP_ 03 (2019) 115 [1901.05932].
  * [7] S. Badger, C. Brønnum-Hansen, H. B. Hartanto and T. Peraro, _Analytic helicity amplitudes for two-loop five-gluon scattering: the single-minus case_ , _JHEP_ 01 (2019) 186 [1811.11699].
  * [8] S. Abreu, J. Dormans, F. Febres Cordero, H. Ita and B. Page, _Analytic Form of Planar Two-Loop Five-Gluon Scattering Amplitudes in QCD_ , _Phys. Rev. Lett._ 122 (2019) 082002 [1812.04586].
  * [9] S. Abreu, J. Dormans, F. Febres Cordero, H. Ita, B. Page and V. Sotnikov, _Analytic Form of the Planar Two-Loop Five-Parton Scattering Amplitudes in QCD_ , _JHEP_ 05 (2019) 084 [1904.00945].
  * [10] S. Abreu, F. F. Cordero, H. Ita, B. Page and V. Sotnikov, _Leading-color two-loop QCD corrections for three-jet production at hadron colliders_ , _JHEP_ 07 (2021) 095 [2102.13609].
  * [11] S. Badger, D. Chicherin, T. Gehrmann, G. Heinrich, J. M. Henn, T. Peraro et al., _Analytic form of the full two-loop five-gluon all-plus helicity amplitude_ , _Phys. Rev. Lett._ 123 (2019) 071601 [1905.03733].
  * [12] H. A. Chawdhry, M. L. Czakon, A. Mitov and R. Poncelet, _NNLO QCD corrections to three-photon production at the LHC_ , _JHEP_ 02 (2020) 057 [1911.00479].
  * [13] S. Abreu, B. Page, E. Pascual and V. Sotnikov, _Leading-Color Two-Loop QCD Corrections for Three-Photon Production at Hadron Colliders_ , _JHEP_ 01 (2021) 078 [2010.15834].
  * [14] H. A. Chawdhry, M. Czakon, A. Mitov and R. Poncelet, _Two-loop leading-color helicity amplitudes for three-photon production at the LHC_ , _JHEP_ 06 (2021) 150 [2012.13553].
  * [15] B. Agarwal, F. Buccioni, A. von Manteuffel and L. Tancredi, _Two-loop leading colour QCD corrections to $q\bar{q}\to\gamma\gamma g$ and $qg\to\gamma\gamma q$_, _JHEP_ 04 (2021) 201 [2102.01820].
  * [16] B. Agarwal, F. Buccioni, A. von Manteuffel and L. Tancredi, _Two-Loop Helicity Amplitudes for Diphoton Plus Jet Production in Full Color_ , _Phys. Rev. Lett._ 127 (2021) 262001 [2105.04585].
  * [17] H. A. Chawdhry, M. Czakon, A. Mitov and R. Poncelet, _Two-loop leading-colour QCD helicity amplitudes for two-photon plus jet production at the LHC_ , _JHEP_ 07 (2021) 164 [2103.04319].
  * [18] S. Badger, C. Brønnum-Hansen, D. Chicherin, T. Gehrmann, H. B. Hartanto, J. Henn et al., _Virtual QCD corrections to gluon-initiated diphoton plus jet production at hadron colliders_ , _JHEP_ 11 (2021) 083 [2106.08664].
  * [19] S. Abreu, F. Febres Cordero, H. Ita, M. Klinkert, B. Page and V. Sotnikov, _Leading-color two-loop amplitudes for four partons and a W boson in QCD_ , _JHEP_ 04 (2022) 042 [2110.07541].
  * [20] S. Badger, H. B. Hartanto and S. Zoia, _Two-Loop QCD Corrections to Wbb¯ Production at Hadron Colliders_ , _Phys. Rev. Lett._ 127 (2021) 012001 [2102.02516].
  * [21] S. Badger, H. B. Hartanto, J. Kryś and S. Zoia, _Two-loop leading-colour QCD helicity amplitudes for Higgs boson production in association with a bottom-quark pair at the LHC_ , _JHEP_ 11 (2021) 012 [2107.14733].
  * [22] S. Badger, H. B. Hartanto, J. Kryś and S. Zoia, _Two-loop leading colour helicity amplitudes for $W^{\pm}\gamma+j$ production at the LHC_, 2201.04075.
  * [23] S. Catani, _The Singular behavior of QCD amplitudes at two loop order_ , _Phys. Lett. B_ 427 (1998) 161 [hep-ph/9802439].
  * [24] T. Becher and M. Neubert, _Infrared singularities of scattering amplitudes in perturbative QCD_ , _Phys. Rev. Lett._ 102 (2009) 162001 [0901.0722].
  * [25] E. Gardi and L. Magnea, _Factorization constraints for soft anomalous dimensions in QCD scattering amplitudes_ , _JHEP_ 03 (2009) 079 [0901.1091].
  * [26] T. Becher and M. Neubert, _On the Structure of Infrared Singularities of Gauge-Theory Amplitudes_ , _JHEP_ 06 (2009) 081 [0903.1126].
  * [27] T. Gehrmann, J. M. Henn and N. A. Lo Presti, _Pentagon functions for massless planar scattering amplitudes_ , _JHEP_ 10 (2018) 103 [1807.09812].
  * [28] D. Chicherin and V. Sotnikov, _Pentagon Functions for Scattering of Five Massless Particles_ , _JHEP_ 20 (2020) 167 [2009.07803].
  * [29] D. Chicherin, V. Sotnikov and S. Zoia, _Pentagon functions for one-mass planar scattering amplitudes_ , _JHEP_ 01 (2022) 096 [2110.10111].
  * [30] A. von Manteuffel and R. M. Schabinger, _A novel approach to integration by parts reduction_ , _Phys. Lett. B_ 744 (2015) 101 [1406.4513].
  * [31] T. Peraro, _Scattering amplitudes over finite fields and multivariate functional reconstruction_ , _JHEP_ 12 (2016) 030 [1608.01902].
  * [32] G. Laurentis and D. Maître, _Extracting analytical one-loop amplitudes from numerical evaluations_ , _JHEP_ 07 (2019) 123 [1904.04067].
  * [33] M. Heller and A. von Manteuffel, _MultivariateApart: Generalized partial fractions_ , _Comput. Phys. Commun._ 271 (2022) 108174 [2101.08283].
  * [34] W. Decker, G.-M. Greuel, G. Pfister and H. Schönemann, “Singular 4-2-1 — A computer algebra system for polynomial computations.” http://www.singular.uni-kl.de, 2021.
  * [35] O. Zariski, _A fundamental lemma from the theory of holomorphic functions on an algebraic variety_ , _Annali di Matematica Pura ed Applicata_ 29 (1949) 187.
  * [36] M. Nagata, _Local rings_ , _Interscience Publishers_ .
  * [37] D. Eisenbud and M. Hochster, _A nullstellensatz with nilpotents and zariski’s main lemma on holomorphic functions_ , _Journal of Algebra_ 58 (1979) 157.