Further author information, send correspondence to N.Blind
<EMAIL_ADDRESS>
# Modal noise in few-mode fibers

N. Blind  Observatoire astronomique de l’Université de Genève, 51 Chemin de
Pegasi, CH-1290 Sauverny, Switzerland

###### Abstract

NIRPS (Near Infra-Red Planet Searcher) is an AO-assisted and fiber-fed
spectrograph for high precision radial velocity measurements in the YJH-bands.
NIRPS also has the specificity to be an SCAO assisted instrument, enabling the
use of few-mode fibers for the first time. This choice offers an excellent
trade-off by allowing to design a compact cryogenic spectrograph, while
maintaining a high coupling efficiency under bad seeing conditions and for
faint stars. The main drawback resides in a much more important modal-noise, a
problem that has to be tackled for allowing 1m/s precision radial velocity
measurements.

We present in this paper the result of a semi-empirical work that allowed to
validate the scrambling device and strategies to mitigate modal noise. It is
based at first on a complete set of lab measurements of the final fibers.
Second, such measurements are injected in the spectrograph design to study in
particular the impact of grating and optics illumination on derived RVs.

###### keywords:

adaptive optics, few-mode fiber, modal noise, spectroscopy

##  1 INTRODUCTION

Since its 1st light in 2002, HARPS has been setting the standard in the exo-
planet detection by precision radial velocity (pRV) measurements. Based on
this experience, our consortium is developing a high accuracy near-infrared RV
spectrograph covering YJH bands to detect and characterize low-mass planets in
the habitable zone of M dwarfs. It will allow RV measurements at the 1-m/s
level and will look for habitable planets around M- type stars by following up
the candidates found by the upcoming space missions TESS, CHEOPS and later
PLATO. Although several similar instruments are already operated (CARMENES,
GIANO, SPIROU), NIRPS is the only one of its kind in the Southern hemisphere.
NIRPS and HARPS, working simultaneously on the ESO 3.6m will become a single
powerful high-resolution spectrograph covering from 0.4 to 1.8 micron. NIRPS
will complement HARPS in validating earth-like planets found around G and
K-type stars whose signal is at the same order of magnitude than the stellar
noise. A complete description of the system can be found in [1].

Being an AO-assisted fiber-fed NIR spectrograph, NIRPS fibers works in a so-
called few-mode regime, that is in-between the usual multi-mode regime (where
1000s of modes propagate) and the single-mode. Although few-mode fibers are
prone to higher modal noise, we present in this paper our work to characterize
and manage it. We show that it shall not preclude the pRV performance to be
achieved. This choice nevertheless allowed for designing a much more compact
spectrograph and grating (with a linear dimension gain of $\sim$2.5), a
serious advantage in the NIR, where the instrument must be cooled.

###  1.1 Few-mode fibers coupling

The number of modes that can transport a circular waveguide is roughly equal
to $V^{2}/4$, where V is the fiber parameter:

$V=2\pi\>\mathrm{NA}\>a/\lambda$ (1)

where $NA$ is the fiber numerical aperture, $a$ the core radius and $\lambda$
the wavelength. The NIRPS High Accuracy fiber (Sect. 1.2.1) has a core size
diameter of 29$\mu m$ (0.4” on sky) and only transports 10 to 35 modes, hence
working in the so-called few-mode regime. This must be compared to the
standard seeing-limited, visible fibers containing 1000s of modes. In this
regime, geometrical optics does not apply so easily anymore, regarding
coupling $\rho$ or scrambling properties.

Thanks to partial AO correction, a fiber of size 0.4” on-sky can reach
coupling $\rho$ of up to 70% in median seeing condition on a bright target
(and $\rho\geq 50\%$ for I$\leq 12$) [2]. Such fibers can couple light within
0.5” in this regime, because modes are not totally constrained into the fiber
core but are guided through a small section of the fiber cladding. While AO-
assisted spectrograph generally push towards the use of modal-noise-free
single-mode fibers, such fibers are very sensitive to wave-front errors and AO
correction. Few-mode fibers allow to relax constraints on optical design as
well as on the AO, allowing fainter limiting magnitude. As a rule of thumb, it
appears that 5% coupling loss is achieved for low-order aberrations amounting
to 100 nm RMS.

Modal noise is the main drawback of using few-mode fibers. Because of the
limited number of modes (a.k.a. speckles in the multi-mode case), each has a
stronger wait in pRV stability when they evolve, due to change in injection
conditions, external stress, temperature drifts, etc. Such fibers also have
much higher inter-modal dispersion, making inter-modal coupling (i.e. exchange
of energy between modes) more difficult: the usual scrambling strategies, like
fiber agitation, is a lot less effective. This also makes the far-field a lot
more dependent on the near-field properties, which led us to question the
efficiency of the double scrambler (Sect. 3.4).

In this paper, we focus on the tests and results obtained for the final fibers
of NIRPS. We do not present the many preliminary stability and FRD tests we
performed on a larger octagonal fiber ($50\mu m$ core), or a smaller round
fiber ($25\mu m$ core). Although we performed analysis at constant V-number
(i.e. shorter wavelength for larger fibers), to keep modal properties as close
as possible from the final ones, the results are not 100% transposable to the
final fiber.

Figure 1: Pictures of NIRPS fiber bench. Light for testing fibers is shown in
red, from top right to bottom. The blue optical path is the back-reflection
alignment path, allowing bench focus and pupil imaging, and fiber near- and
far-field alignment. In green, we zoom on aperture stop, exit OAP, and the 5
axis alignment stages.

###  1.2 NIRPS fibers

We give here a short description of the fiber-link fibers. More details can be
found in [3] (these proceedings).

####  1.2.1 High accuracy fiber (HAF) - OCT29

The standard high resolution fiber of NIRPS is a custom octagonal fiber from
Ceramoptec, with core and cladding size of 29$\mu m$ and 116 $\mu m$
respectively, and NA=0.22. We measured its core size to 29 $\pm$ 0.3 $\mu m$.
The core size corresponds to 0.4” on sky, and it is fed with an f/4.2 beam. It
is used for the main science fiber (HAF), as well as for the 2 simultaneous
reference / sky fiber. It allows for spectral resolution of R$\sim$100.000.

####  1.2.2 High efficiency fiber (HEF) - OCT66 & REC33x132

The HEF fiber is a seeing-sized fiber of 0.9”, planned to be used on fainter
targets, when the AO cannot perform optimally. At the front-end injection
level, it is a Ceramoptec octagonal fiber with core / cladding size 66$\mu$ /
264$\mu m$ respectively (drawn from the same preform as the OCT29), and fed
with f/4.2 beam. In the double scrambler, a Bowen-Walraven slicer cuts the
far-field in 2 halves, reimaged on a rectangular fiber of size 33x132 $\mu m$,
also from Ceramoptec. Hence the rectangular fiber is illuminated on its whole
surface in a pretty constant way. This slicing operation (which was meaningful
thanks to the large size of the focal plane detector) allowed to preserve a
rather high spectral resolution R$\sim$80.000.

##  2 Method

We adopted a semi-empirical approach to study the performance of the few-mode
fibers and the different scrambling device. The fibers and scrambling device
are first characterized on a bench, in the Near-Field (NF) and Far-Field (FF).

Because of the few-mode nature of this fiber, in-fiber far-field scrambling is
rather poor and double scrambler proves to be of limited interest (see Sect.
3.4). Therefore, the far-field illumination of the grating and optics can
significantly vary with injection conditions (AO guide star magnitude, seeing,
etc). This effect cannot be studied simply by near-field measurement on a
bench. The previous measurements were therefore also injected into the Zemax
optical model of the spectrograph to study the impact of optical aberrations
when pupil/grating illumination varies.

Figure 2: Example of spectrograph simulation with only 20.000 rays here. Left
and middle: rays, colored by intensity in the pupil (weight). Half the fiber
core is hidden in this example. Right: Resulting image at the focal plane at a
particular wavelength (black). Red is the image formed using all rays
(covering the fiber core and the complete grating).

###  2.1 Fiber test bench

We set-up an achromatic bench (Fig. 1), made of 2 OAPs and two folding mirrors
(initially planed to allow for integrating the NIRPS AO system). The
magnification of the bench is x0.2. While the input is fixed, the output is
motorized, with 3-axis linear piezostage from Attocube, and a 2 rotational
axis Gimbal mount from Zaber. The exit aperture can be varied from f/2.5 to
less than f/22 for Focal Ratio Degradation (FRD) measurements. Apart from such
tests the bench was used at f/4.2, the NIRPS fiber aperture. A pellicle
beamsplitter allows to visualize the bench exit focal plane and pupil via back
reflection, for fiber alignment via retroinjection.

The fibers under test are mounted on the 5-axis motorized stage. For each, the
procedure consists in recording NF and FF data for multiple positions across
the core, typically leading to more than 200 measurements. We generally use an
halogen lamp as primary light source, and have at disposal different narrow
band filters ($\Delta\lambda\sim 10nm$), centered at 908, 1200, 1310, 1400,
1550 and 1650 nm.

The bench has proven a stability better than 1m/s over time scale of 10-20
minutes, necessary to perform a complete XY scan of the fiber tip.

###  2.2 Spectrograph simulations

To study the behavior of the spectrograph in varying conditions, we first used
its Zemax model to randomly generate 1.000.000 rays that uniformly cover the
input focal (X/Y) and pupil planes (angle $\alpha$/$\beta$), and record their
arrival position on the detector. We repeat the operation for 5 wavelengths
along each order of the spectrograph, and for each of the 69 orders (Fig. 2).
The same set of rays was used in all cases to not add noise from the random
sampling.

We then load those rays in a python script, with which we are able to
reproduce the near- and far-field intensity measured on the bench by playing
on the weight of each ray. One limitation is of course the broadband nature of
our measurements ($\Delta\lambda=10nm$). To cover the full spectral range of
the spectrograph, we adopted two extrapolation methods:

  1. 1.

We take each measurement sets and make a linear interpolation of the profile
with wavelength;

  2. 2.

We average the profiles of the different sets and inject it as an achromatic
illumination.

Both methods showed rather similar behavior.

We also made more fundamental studies. As an example, we changed the grating
(pupil) illumination, e.g. by varying the fiber far-field illumination size in
Fig. 3, considering a theoretical gaussian illumination of the grating, and a
fixed near-field illumination. This test demonstrates that far-field
variations generates significant RV drift along every single order, but the
symmetrical design allows to balance from one side to the other of each
orders, so that average drift is nearly 0.

Figure 3: Impact of a change in the grating illumination on the RV value.
Left: illustrative example of RV offset along all orders, with 5 points per
order (dots, colored proportionnal to wavelength), and RV averaged over each
order (black line). A line between the color dots would have a sawtooth shape.
Right: summary of average RV offset (average of black curve in left plot) when
varying the grating FWHM illumination for a fiber far-field with gaussian
shape.

##  3 Scrambling performance of the HAF / OCT29 fiber

The HAF fiber was identified as the most problematic fiber, especially
regarding the AO-corrected injection, and was therefore thoroughly studied.

###  3.1 Natural behavior

Fig. 4 shows near- and far-field of a single OCT29 fiber at $\lambda$=1600nm,
when scanning the entrance with a point source. Conversely to multi-mode
fibers where the scrambling properties allow clear distinction between near-
and far-fields, this is much more difficult here: there is a very strong
correlation between near- and far-field illuminations. This is also indicative
that in the case of NIRPS, stabilizing the spectrograph pupil illumination is
equivalent to stabilizing the fiber near-field. We discuss the interest of the
double scrambler in Sec. 3.4.

When scanning the fiber tip of the OCT29 fiber alone, we observe a photocenter
motion of the order of 10m/s RMS (Fig. 4 (top) and Fig. 5) with narrow band
filters. FRD of the fibers is pretty good, with 90% at f/4.2, although the
definition of FRD might be questionable given the extension of the modes (Fig.
4, bottom). The RV ’noise’ for varying injection positions is presented in
Fig. 10, together with performance after considering some of our scrambling
device. The stability is computed for all injection position presenting a
coupling higher than 50% of the maximum.

Figure 4: A few images of the OCT29 fiber NF and FF illumination. From left to
right the fiber entrance is scanned with a point source, with 1310nm filter.

###  3.2 Scrambling with adaptive optics

Given the presence of an AO system in NIRPS, it is only natural to consider
using the DM for scrambling. We demonstrated in [2] that mode-selective
coupling is possible to some degree, by playing on the DM phase to match the
phase of some specific modes. But the coupling losses are generally
unacceptable. It appeared that the most efficient scrambling strategy with the
AO of NIRPS is, by far, tip-tilt scan of the fiber tip: it preserves coupling
into fiber and is able to couple to any given mode of the fiber, conversely to
other classical optical aberrations. For instance, aberrations with azimutal
symmetry like focus or sphericity are the worst aberrations: due to their
symmetric nature, those terms reduce coupling in all modes, but are not able
to excite new ones.

In practice, the AO-corrected PSF is describing a rose curve generated by
updating the reference slopes at each AO loop iteration. The radial position
is scanned with sine or triangular modulation at $\sim$20 Hz, while the
azimutal modulation is performed at a constant angular speed. It is possible
to limit the capability of the fiber to hit the most central part of the fiber
and to describe a ring pattern instead of a full disk.

The measurements on the fiber bench are performed with a diffraction-limited
source. The collect of scanned data allows a-posterior averaging of NF images
to simulate different scrambling strategies (Fig. 5). We compared 3 basic
weighting laws across the fiber tip: ’uniform’ (triangular modulation), ’r’
(more weight in the outside of the fiber core, close from sine modulation) or
’1-r’ (more weight in the center of the fiber core). From one measurement to
the other or different filter / wavelength band, only the ’1-r’ shows a
slightly lower performance. We notice RV residuals are naturally much lower
than without this scanning, allowing for fiber centring error of the order of
$\pm$ 0.1” to keep $\leq$ 0.5m/s NF stability.

Measurements performed in the far-field show how the scrambling strategy can
influence the grating illumination (Fig. 6), primarily the center of the far-
field illumination, and almost not the external. The uniform law tends to
deliver flatter far-field over 50% of the fiber NA cone (but this is does not
constitute a criterion). Very similar profiles are observed with the other
filters, down to 1000 nm. This behavior is nevertheless observed only in the
case of a single fiber. Far-field illumination with the stretcher is much less
dependent on the scrambling choice thanks to internal scrambling (see Sect.
3.3).

Figure 5: NF photocenter stability for a single OCT29 at 1650nm. Left: scatter
plot of ’natural’ photocenter positions (blue, with error bars), as well as
’AO scrambling’ averaged for different weighting strategies (red, orange,
green). Right (3 images): representation of the photocenter instability for
the 3 modulations, for various guiding offset (’Sky position’ represents the
center of the modulation). Figure 6: Far-field illumination and profile cut
resulting from AO scrambling with different laws at 1650nm. f/4.2 corresponds
to pixel $\sim$100

###  3.3 Stretcher

Figure 7: Picture of the final fiber stretcher of NIRPS during integration.
Fibers are eventually secured on the grooves with glue patches.

The fiber stretcher (Fig. 7) is a device whose primary goal is to decrease the
impact of modal noise in the few mode fibers, by quickly modulating phase
between modes and homogenizing the output illumination. This allows to
significantly reduce the impact of external factors (like varying fiber stress
or temperature gradients) and stabilize the cross-correlation function between
the measured spectrum and the mask from one observation to another, so as to
avoid drifts/noise by more than 1m/s.

  * •

Phase modulation – The working principle of the stretcher is to dynamically
modulate the phase between modes, which present inter-modal dispersion of
$\sim 10^{-4}-10^{-3}$ (or a beat length in the ’few mm range’). Doing so, it
averages the speckle pattern and generate over short periods of time a figure
equivalent to the incoherent sum of the excited modes. A phase modulation of
2$\pi$ between any set of two modes requires a few mm stretching. However, the
beat length between different pairs of modes being different, the higher the
phase modulation amplitude, the better the result.

  * •

Mode scrambling – Because of the fiber routing around two half cylinders,
modes are slightly disturbed and can transfer energy to others. Hence the
stretcher presents scrambler properties by distributing energy over more modes
than at its entrance. Such effect was a lot clearer on the final stretcher
with octagonal fibers, than on the very first prototype on round fibers. The
rotational asymmetry of octagonal fibers leads to finer effective index
difference between modes, hence facilitating transfer of energy between modes,
as well as making them more sensitive to external disturbance (the cylinder
routing here).

Fig. 8 shows a few images of the stretcher NF and FF. The benefit of the two
previously described effects is clearly visible when compared to Fig 4,
although it does not allow to uniformly fill all the modes of the fiber.

The final stretcher (Fig. 7) is made of 20 spools, assembled on half-cylinders
(R=75mm) on which grooves have been drawn to keep the fiber in place. The
stretch is performed with a piezo-amplified actuator, allowing up to 250 $\mu
m$ of stretch per section. We end up with a total of 7mm stretch for the whole
assembly, due to a few loose sections. This stretch is equivalent to a
temperature change of $\geq$ 50K over 25m fiber. It is modulated at a
frequency of 1 Hz with a sine function to limit shocks and avoid premature use
or breakage of the fiber111Note that the first prototype was operated
continuously for 1 year at a modulation frequency of 30Hz without showing
signs of fatigue. It was stopped when we started to work on the 2nd
prototype.. Also, the stretcher is integrated within a 60m long fiber ($\sim$
20m devoted to the stretcher routing), without connectors, to not introduce
fiber-to-fiber misalignment (lateral or rotational) and break the upstream
scrambling. The transmission of the stretcher (fiber transmission excluded) is
$\geq 90\%$. No additional transmission loss was observed when piezo was
stretching.

Figure 8: A few images of the stretcher fiber illumination, to be compared to
Fig. 4. From left to right the fiber entrance is scanned with a point source,
with 1310nm filter.

###  3.4 Double scrambler

Optical fibers (and even more non-circular ones) are known for their excellent
scrambling properties in the near-field, which led to the very successful
concept of double scrambler to exchange near- and far-field properties, and
scramble both efficiently. We have seen in Fig. 4 that few-mode fibers are not
behaving the same way: changing injection conditions very clearly changes the
output near-field illumination. Also, the near-field and far-field of few-mode
fibers are quite similar in energy distribution and are much less independent
from each other. This observations questioned the benefit of using a double
scrambler in NIRPS. In addition, because of mismatch of modes between the
near- and far-field, it is expected1) to get decreased coupling efficiency
compared to a standard feedthroug: (simulations suggest losses $\sim$20% in
the case of a double scrambler); 2) to actually create some modal noise. To
test this, we designed a double scrambler and a standard feedthrough for
NIRPS, and characterized them both at different wavelengths. Note that the
input of those device was a single fiber, and not the stretcher prototype
presented in previous section, which was still under preparation.

One of the benefit of the double scrambler being the gain in grating
illumination stability, a definitive comparison was to inject the NF and FF
measurements in the spectrograph design, as presented in Sect. 2.2. Fig. 9
compares the performance of both device for different test cases, enumerated
from left to right:

  1. 1.

AO scrambling with ’1-r’ law and scanning radius of 0.2”;

  2. 2.

AO scrambling with ’r’ law and scanning radius of 0.2”;

  3. 3.

AO scrambling with ’uniform’ law and scanning radius of 0.2”;

  4. 4.

AO scrambling with ’uniform’ law and scanning radius of 0.4”. Scanning is
performed outside the fiber core, and might be consider to first order as a
’seeing limited’ case.;

  5. 5.

Same as 3), with guiding error of 0.05”;

  6. 6.

Same as 4), with guiding error of 0.05”;

  7. 7.

Same as 3), with guiding error of 0.1”;

  8. 8.

Same as 3), with pupil illumination change of 10% in diameter (this change was
forced numerically and not the result of a different scrambling for instance);

There is no clear winner here. A standard feedthrough seems to perform better
under smaller modulation radii (tests 1 to 4), but on the other hand appears
more sensitive to guiding errors (tests 5 to 7). Both device react equally to
change in fiber illumination.

The double scrambler was ultimately implemented in NIRPS because at the time
of measurements and simulations, the design was nearly finalized.

Figure 9: Double scrambler performance compared to a standard feedthrough.

###  3.5 Summary for HAF / OCT29

Fig. 10 summarizes the performance of the OCT29 fiber presented in this
section. From the pure RV stability point of view, it appears that the
stretcher or the AO scrambling provide each a gain of $\sim$10 on the
stability, down to about 1m/s. When combined, they accumulate to first order
(thanks to their different action on fiebr modes) and stability drops to the
few 10 cm/s level. The measurements and spectrograph simulations do not point
to a clear benefit of a double scrambler in the few-mode regime.

Figure 10: Summary of near-field stability measurement at different
wavelengths and for different set-up.

##  4 The HEF / REC33x132 fiber

We could not easily make a mock-up of the slicer part to investigate
scrambling performance of the HEF. We instead made a ’worst illumination’
scenario test on the rectangular fiber: we used a 500$\mu m$ fiber (magnified
by x0.2 by the bench, making a 100 $\mu m$ image), which we moved in front of
the rectangular fiber (Fig. 11, middle). We scanned with amplitude
40$\times$150 $\mu m$ to evaluate the level of modal noise under a strongly
varying illumination condition. The test shows a very symmetric photocenter
motion of amplitude $\leq$2 m/s along the small side of the fiber (i.e. the
main dispersion direction) at $\lambda$=1310 nm (Fig. 11, right).

Considering the following stability of the rectangular fiber illumination in
the double-scrambler:

  * •

A scrambling gain $\geq$ 100 at the same wavelength (i.e. illumination
photocenter moving by less than 5 $\mu m$, or $\geq$ 150 m/s);

  * •

A thermal stability of the double scrambler opto-mechanics as bad as 10 $\mu
m$ in the near-field;

would result with photocenter motions at the output of the HEF below 2 m/s ×
(5$\mu$m + 10$\mu$m)/132$\mu$m = 0.23 m/s. The stability requirement for this
fiber was initially set to 5 m/s. Those measurements suggest that such
performance should be easily reached.

Figure 11: Left: illumination in the double-scrambler with slicer. Middle:
moving illumination for the stability test. Right: Photocenter displacement of
REC33x132 at $\lambda=1310\pm 10nm$, with an image of the near-field when the
input source is centered.

##  5 Conclusion

A significant effort was made to understand and characterise modal noise in
few-mode fibers. Those tests validated the envisioned strategies (use of
stretcher and AO scrambling), showing stability better than 0.5m/s.

A limitation of those tests is nevertheless to have focused solely on the RV
stability, averaged over small bandpath (equivalent to one diffraction order
of the spectrograph), assuming a very smooth evolution of the modes over 1-10
nm, given their small number. First commissioning tests on sky have shown the
presence of very high spectral resolution features ($\leq$0.1A), i.e. about
the width of an actual spectral line (see [3], these proceedings). Such
behavior could only have been observed and studied with a high resolution
spectrograph R$\geq$50.000. Such pattern could originate from the double
scrambler alignment.

We also underestimated the importance of the modal noise on calibration fibers
(with large input illumination), as well as on the HEF, and focused on the AO-
fed HA one. The latter, equipped with fiber stretcher and AO scrambling,
demonstrates a higher stability of modal noise pattern over a day and for
varying telescope pointings.

## References

  * [1] Wildi, F. et al., “NIRPS: an adaptive-optics assisted radial velocity spectrograph to chase exoplanets around M-stars,” in [Techniques and Instrumentation for Detection of Exoplanets VIII ], Shaklan, S., ed., 10400, 321 – 335, International Society for Optics and Photonics, SPIE (2017).
  * [2] Blind, N., Conod, U., and Wildi, F., “Few-mode fibers and ao-assisted high resolution spectroscopy: coupling efficiency and modal noise mitigation,” AO4ELT 5 , arXiv:1711.00835 (Nov. 2017).
  * [3] Bouchy, F. et al., “Nirps fiber-link design, performances and modal noise mitigation performances tested on sky,” This proceeding (Aug. 2022).


# What do LLMs need to Synthesize Correct Router Configurations?

Rajdeep Mondal
<EMAIL_ADDRESS>Alan Tang
<EMAIL_ADDRESS>Ryan Beckett
<EMAIL_ADDRESS>Todd Millstein
<EMAIL_ADDRESS>George Varghese
<EMAIL_ADDRESS>
###### Abstract

We investigate whether Large Language Models (e.g., GPT-4) can synthesize
correct router configurations with reduced manual effort. We find GPT-4 works
very badly by itself, producing promising draft configurations but with
egregious errors in topology, syntax, and semantics. Our strategy, that we
call Verified Prompt Programming, is to combine GPT-4 with verifiers, and use
localized feedback from the verifier to automatically correct errors.
Verification requires a specification and actionable localized feedback to be
effective. We show results for two use cases: translating from Cisco to
Juniper configurations on a single router, and implementing no-transit policy
on multiple routers. While human input is still required, if we define the
leverage as the number of automated prompts to the number of human prompts,
our experiments show a leverage of 10X for Juniper translation, and 6X for
implementing no-transit policy, ending with verified configurations.

††conference: Submitted to HotNets 2023

##  1 Introduction

> The limitations of his knowledge were as startling as its profundity – Hardy
> on Ramanujam [1]

While GPT-4 and other language models have shown great success in some domains
(e.g., writing poems, passing the LSAT) they have been shown to have issues in
other domains (e.g,. math, word puzzles) [3]. Language models have had some
success in helping users write sequential programs in systems like CoPilot [6]
and Jigsaw [7]. Our paper examines GPT-4’s ability to write router
configuration files, traditionally written by humans, that help tune routes
and forwarding decisions and are critical for network operation. Our early
experiments show that GPT-4 by itself is an “idiot-savant", capable of
brilliance but also making simple errors that an operator would be fired for
making.

Critics have derided large language models (LLMs) as mere “stochastic parrots”
[2],because they produce text (say of a program) syntactically by predicting
the next word based on a statistical model derived by training on a vast
corpus of text found on the Internet. Our broader goal beyond synthesizing
configs is to see whether LLMs can be combined with other programs (via APIs)
to come closer to a “stochastic owl” that understands program semantics.

A plausible way to introduce semantics is to pair a LLM with an automatic
verifier such as a SAT solver or a model checker. But verification is not a
panacea. First, a verifier cannot prove correctness without a specification.
In practice, specifications are incomplete, so not all solutions are in fact
acceptable to the user. Second, for the verifier to automatically (with
minimal human aid) interact with the LLM, the verifier must provide actionable
feedback. We found it was easier for the LLM to correct itself using feedback
from modular verification of components of a network (individual routers [9]
or even route maps within a router [10]), rather than the network as a whole.

Figure 1: Pair Programming using human correction.

Figure 1 shows the traditional method of pair programming (PP), embodied in
systems like GitHub CoPilot [6], where a human and an AI work together to
author a program. In pair programming, the AI and the human form a tuple
$(A,H)$ and the human $H$ manually checks for correctness of the output of the
AI $A$ and then manually issues correction prompts to $A$ as shown in the
figure. Such manual initial prompting and subsequent manual correction is
often called prompt engineering.

Figure 2: Verified prompt programming.

Figure 2 shows our alternate vision. In what we call Verified Prompt
Programming (VPP), the AI, the human, and a verification suite ($V$) form a
triple $(A,H,V)$. The verification suite checks for correctness and
automatically issues localized corrections. $V$ may abandon automatic
correction after some number of trials, and the human must still correct
manually. However, our hypothesis is that human effort is reduced as the
output grows “closer” to a correct program.

Notice that there is a fast inner loop between $V$ and $A$, where verifier
results are automatically fed back to GPT-4. Since verifier feedback is often
cryptic, we use simple code that we call a humanizer that converts the
feedback to natural language prompts that are given to GPT-4. When $V$ either
determines the final configuration is correct or a time bound elapses, $V$
sends the output back to the user as part of the slow manual loop. We examine
a “reduced work hypothesis": that the work in the manual loop in Figure 2 is
significantly less than then the manual work in Figure 1

To quantify reduced human effort we introduce a simple measure that may be
useful in other VPP contexts. Define leverage as the ratio $L$ of the number
of automated prompts in Figure 2 to the number of human prompts. Leverage
measures the effect of the verifier suite, the potential improvement in going
from $(A,H)$ to $(A,V,H)$, keeping the language model $A$ and the human $H$
the same.

The reader may think the real leverage is the improvement from $H$ to $(A,H)$,
or from $H$ to $(A,V,H)$. But this depends on the capability of the human $H$
and is hard to make uniform or repeatable. Given how error-prone $(A,H)$ is
for configurations, we find it more natural to measure the improvement caused
by VPP. If a future LLM, say GPT-6, produces near-perfect configurations,
leverage will decrease as there is less need for automatic correction. Our
definition also assumes every automatic correction in Figure 2 would otherwise
be be done by a human in Figure 1.

The reduced work hypothesis is that the leverage $L>1$ is high. Even if the
leverage is low (say $1$), since it is crucial that router configurations be
correct, combining with a verifier seems critical. We were happy to find that
in both use cases we did end with verified configurations via GPT-4: this was
not obvious at the outset.

This vision and hypothesis extends beyond synthesizing configs to more general
programs. Prompt programming (as opposed to prompt engineering) also reflects
the use of APIs and automatically generated feedback prompts that may be more
generally useful. However, network configs are a simple enough domain to
experiment with. Further, there exist config verifiers (e.g., Campion [10] and
Lightyear [9]) that provide actionable localized feedback.

For the rest of this paper, we examine the reduced manual work hypothesis and
measure leverage for two use cases: translating a config on a single router
from Cisco to Juniper syntax, and implementing a simple policy (“no transit")
on a network of 7 routers. Section 2 describes the system organization of a
potential system we call CoSynth. Section 3 describes experiments with Cisco
to Juniper translation, while Section 4 describes implementing no-transit on
multiple routers. Section 5 compares our ideas to previous work and Section 6
describes lessons learned.

##  2 System Organization

Figure 3 is a refinement of the more general Verified Pair Programming (VPP)
vision of Figure 2 that we call CoSynth. We emphasize we have not built
CoSynth. While we use GPT-4 we have not been able to access the APIs, and so
manually simulated the API calls with prompts to ChatGPT. Our goal is not to
demonstrate a working system but instead to explore GPT-4’s ability to author
configurations, as in the “Sparks of AGI" paper [3].

Figure 3: Verified prompt programming for Configs

The verification suite shown in Figure 3 consists minimally of two verifiers,
a syntax verifier (we used Batfish [5]) and a semantics verifier (we used
different ones depending on the use case). For our second use case, we used a
third verifier, a topology verifier (that we wrote in Python) as we found that
GPT-4 sometimes missed announcing routes to neighbors. The user provides a
precise natural language description of the context (topology, routers,
interfaces) and the desired task (e.g. the Cisco config and a request to
translate it to Juniper). GPT-4 output is fed first to Batfish to check for
syntax errors. CoSynth sends GPT-4 feedback about erroneous lines, “humanized"
in natural language (see Table 1 for examples). The boxes labelled H in Figure
3 correspond to the humanizer in Figure 2.

If all syntax errors are corrected (if too many syntax correction attempts
occur, CoSynth punts to the user), the output is passed to the semantics
verifier. For our first use case, we use Campion [10] as a verifier. For our
second use case we use Batfish’s symbolic route map analysis as the verifier,
asking it to verify local policies that together ensure the desired global
policy, as in Lightyear [9]. Once again, the semantic verifier feedback is
passed back, suitably humanized, to GPT-4. We found that GPT-4 would sometimes
correct a semantic error while introducing a new syntax error, in which case
we had to return to the syntax verifier. When the semantic verifier attests to
a correct config or too many correction attempts transpire, CoSynth returns to
the human.

When CoSynth works with multiple routers, we used another module called a
“Modularizer" (Figure 3). For network configs, the idea is that we start with
a precise machine readable (we use JSON) description of the “modules" which in
our case is the topology and the connections. The Modularizer outputs a
sequence of Natural Language Prompts that describes the topology to GPT-4
(e.g.,. Router $R1$ is connected to Router $R2$ via interface $I1$ at $R1$ and
$I2$ at $R2$). The Modularizer can also take a general specification of local
policies (e.g. edge routers add a specific community on ingress) and output a
specific local specification for each router for the semantic verifier. The
Composer puts back the pieces (in our case in a folder for Batfish).

The modularizer follows the prompt engineering paradigm "Give the Model Time
to Think" [4], which suggests breaking a complex prompt into simpler sub-
prompts. Exploiting modularity is a way to do so for program synthesis. A
second technique we find useful is what is called single shot prompting [4].
We start each chat with a set of initial instruction prompts (IIP) (Figure 3)
loaded from a database for avoiding common mistakes. The IIP database can be
built and added by experts over time. The I/O examples in Jigsaw [7] are an
IIP, but our IIP contains instructions not examples.

##  3 Cisco to Juniper Translation

We translate a Cisco configuration into an equivalent Juniper one using
Verified Pair Programming. Batfish [5] is used to identify syntax errors.
Campion [10] is used to detect and localize semantic differences that are used
to refine the result. We show examples of the issues encountered, and discuss
success and limitations of the approach.

###  3.1 Method

First, we provide the Cisco configuration, and the prompt: "Translate the
configuration into an equivalent Juniper configuration." GPT-4 will produce a
translation into Junos format that typically contains several errors and
differences. We try to rectify these errors iteratively. First, we use Batfish
[5] and Campion [10]to detect any errors or differences, and then use a simple
script to produce a prompt for GPT-4 (the humanizer $H$ in Figure 3) to try
and fix this error. After GPT-4 attempts to resolve the issue, we ask it to
print the entire configuration and check the result using verification tools
again. For our experiment we focus exclusively on behavior related to routing
and forwarding, ignoring potentially important features such as NTP servers.

To design the humanizer (i.e., automatically generate a prompt informing GPT-4
of the errors present), we distinguish four classes of configuration errors:

Syntax errors: Batfish produces parse warnings identifying relevant lines that
do not use valid Juniper syntax.

Structural mismatch: This is when a component, connection, or named policy is
present in the original configuration but not in the translation (or is
present in the translation but not the original). For example, if the original
configuration defined a BGP neighbor but there is no corresponding neighbor in
the translation, there would be a mismatch in the routing connections.
Similarly, if there are corresponding BGP neighbor definitions in both
configurations, but one configuration has an import policy defined while the
other does not, that would be a mismatch in the named policies present.
Campion is able to detect this, and identify the missing or extra items.

Attribute differences: This is when a numerical attribute has a different
value between the two configurations. An example is OSPF link cost difference
between two corresponding interfaces. Campion detects these and prints the
attributes for corresponding components.

Policy behavior differences: This is when a route map or access control list
has a semantic difference. Route maps are used to filter incoming or outgoing
route advertisements, so a difference would mean that that there are some
route advertisements that are allowed by one router but not allowed by the
other. Campion is able to detect these and output the relevant policy names,
prefixes, and lines for these differences.

The distinction among errors helps for two reasons. First, syntax errors and
structural mismatches have to be handled earlier since they can mask attribute
differences and policy behavior differences. Second, different types of errors
require different humanized prompts, while errors of the same type can reuse
similar prompts. Each type of error can be summarized with a formulaic prompt
with some fields inserted based on the error reported by Batfish or Campion.

Table 1 shows the formulas and examples of generated prompts. Batfish parse
errors and warnings can be reused as prompts for syntax errors. Prompts for
structural mismatches and attribute differences are easily generated from the
relevant components and attributes. Policy behavior differences are more
difficult since it is not always clear how to describe the affected input
space that is treated differently. We opt for the approach of giving an
example prefix.

Type | Generated Prompt |
---|---|---
| Syntax
---
error
| There is a syntax error:
---
‘policy-options prefix-list our-networks 1.2.3.0/24-32’
| Structural
---
mismatch
| In the original configuration,
---
there is an import route map for bgp neighbor 2.3.4.5,
but in the translation,
there is no corresponding route map
| Attribute
---
difference
| In the original configuration,
---
the OSPF link for Loopback0 has cost set to 1,
but in the translation, the corresponding
link to lo0.0 has cost set to 0
| Policy
---
behavior
difference
|  In the original configuration, for the prefix 1.2.3.0/25,
---
the BGP export policy to_provider for BGP neighbor 2.3.4.5
performs the following action: ACCEPT.
But, in the translation,
the corresponding BGP export policy to_provider
performs the following action: REJECT
Table 1: Sample rectification prompts for translation generated using formulas
(non-italicized text), and fields generated from Batfish and Campion
(italicized text).

###  3.2 Experience and Results

Error | Type | Fixed
---|---|---
Missing BGP local-as attribute | Syntax error | Yes
Invalid syntax for prefix lists | Syntax error | Yes
Missing/extra BGP route policy | Structure mismatch | Yes
Different OSPF link cost | Attribute error | Yes
Different OSPF passive interface setting | Attribute error | Yes
Setting wrong BGP MED value | Policy error | Yes
Different prefix lengths match in BGP | Policy error | No
Different redistribution into BGP | Policy error | No
Table 2: Translation errors found and whether GPT-4 was able to fix them with
generated prompts.

We tried translating a Cisco configuration from the Batfish examples [5] into
Juniper format. This configuration was short enough to fit within GPT-4 text
input limits, but used non-trivial features including BGP, OSPF, prefix lists,
and route maps. GPT-4’s synthesized Juniper router configuration had several
errors. In many cases, when an automatically generated prompt, similar to
those in Table 1, is provided to GPT-4, it will produce a response fixing the
issue. In some cases, GPT-4 is unable to edit the translation correctly,
either applying no change or applying an erroneous one. This often requires
manual intervention via more specific prompts in order to fix. Another problem
is that GPT-4 can fix one error, but introduce new errors that were not
previously there. Sometimes it even reintroduces errors that were previously
fixed! However, we were able to reach a point where Campion and Batfish no
longer produced errors.

Leverage: The entire cycle of prompts was around 2 human prompts and 20
automated prompts, for a leverage of 10X. Some of the 20 automatic prompt
correction cycles included minor cycles for syntax correction not just at the
start but also after correcting semantic errors. To be clear, we “simulated”
each API call by feeding our automatically generated prompts manually to
GPT-4.

Table 2 shows errors in the translation at some point and whether GPT-4 was
able to fix them using an automatically generated prompt. In more detail:

Missing BGP local-as attribute: The translated BGP neighbor declarations did
not include a local AS attribute. We label this a syntax error since it
produces a parse warning.

Missing/extra BGP routing policy: An import or export policy is used for a BGP
neighbor in only one configuration.

Different OSPF link attributes: OSPF links have a number of attributes, and
the translation sometimes contains differences in link cost or passive
interface settings.

Setting wrong BGP MED value: The translation of one BGP routing policy did not
update the BGP MED value. This was caused by an error in translating one of
the route map clauses from the original Cisco configuration.

Different Redistribution behavior into BGP: Cisco and Juniper formats handle
route redistribution into BGP differently. Juniper typically does this using
the same routing policies that control importing and exporting BGP routes
while Cisco configurations set a separate route map for route redistribution.
In our case, Campion detected that the Juniper configuration was
redistributing some routes that the Cisco configuration did not. This could be
fixed by adding a "from bgp" condition to a number of locations in the policy.
Unlike the previously described errors, GPT-4 was unable to fix this when
given the automatically generated prompt. Instead it usually does nothing when
asked to fix the error. However, it was able to fix the problem when asked
more directly to add "from bgp" conditions to routing policies.

BGP prefix list issues: Another subtle issue occurred when translating prefix
lists. In the original Cisco configuration, a prefix list was defined to match
prefixes with length 24 or greater where the first 24 bits matched 1.2.3.4. In
Cisco this is done with the command:

ip prefix-list our-networks seq 5 permit 1.2.3.0/24 ge 24

and it was applied with the definition:

route-map from_customer deny 100
match ip address prefix-list private-ips

The noteworthy part is the "ge 24" which says to match prefixes with length 24
or greater. There is no equivalent of this in defining prefix lists in
Juniper, but for our use case, there are at least two methods of getting
similar behavior in Juniper with different syntax. When GPT-4 is asked to
translate the configuration, it often does not translate the "ge 24" part
correctly, often just omitting it, so the space of prefixes matched will
differ in the translation. When asked to fix this problem, it sometimes
generates configurations with incorrect syntax. For example, it can output the
following:

prefix-list our-networks { 1.2.3.0/24-32; }

which is not valid Juniper syntax. However, after informing it of the error,
it does eventually find a correct translation.

##  4 Global Policies via Local Synthesis

Next, we used GPT-4 to generate router configs for a given network topology
based on local policies for each router, inspired by Lightyear [9], which does
control plane verification by verifying local invariants. We limited our scope
to BGP.

For semantic correctness, we use two new modules. The first is a ’topology’
verifier which checks whether the config of a particular router follows the
defined topology. It checks whether GPT-4 sets up all interfaces, declares BGP
neighbors and announces networks correctly. Second, we run Batfish to check
local policies defined in the prompts; the outputs are used to refine the
result.

###  4.1 Method

We begin by specifying the task to GPT in an initial prompt using a couple of
sentences. The intention is to influence the LLM to start ‘thinking’ in a
certain fashion. Our goal is to make the network follow the no-transit policy,
under which no two ISP’s should be able to reach other. However, all ISPs
should be able to reach the CUSTOMER and vice versa.

Figure 4: Star network topology used for local synthesis.

It is difficult to write a natural language description of the topology, a
task prone to human error. We wrote an automated script that generates text
given the topology as input. In our experiments, we limited our scope to star
networks where one router would be attached to a CUSTOMER IP, while the other
routers are connected to different ISPs (Figure 4). All the ISP routers are
directly connected to the first router. The "network generator" therefore only
needs the number of routers as input. It has two outputs: 1) a textual
description and 2) a JSON dictionary for the entire network topology. The
textual description is used as a prompt, while the JSON dictionary is used
later to check whether the generated configs match the topology.

Local versus Global Policy Prompts? We tried specifying to GPT-4 the global
no-transit policy at once. GPT-4 generated two innovative strategies:
filtering routes using AS path regular expressions, and denying ISP prefixes
from being advertised to other routers from the customer router.
Unfortunately, we found after correcting topology and syntax errors, when we
provided feedback in terms of a counterexample packet (as would be provided by
a “global" network verifier like Minesweeper), GPT-4 was confused and kept
oscillating between incorrect strategies. We found that specifying local
policies as in Lightyear [9] gave us better results because it allowed us to
localize verification errors to specific routers and specific route maps
within those routers.

We asked GPT-4 to generate configs for each router using a new prompt each
time, specifying the local policy for each router. Specifically, the policy is
that $R1$ should add a specific community at the ingress to each ISP and then
drop routes based on those communities at the egress to each ISP. The
generated errors fell into three categories:

Syntax errors:  GPT-4 generates a configuration with invalid Cisco syntax
including errors in which certain config lines are misplaced. Batfish produces
parse warnings identifying these errors.

Topology errors:  GPT-4 incorrectly declares or misses some BGP neighbors or
forgets to announce certain networks. For this, we use an automated "topology
verifier" that compares the config against the previously specified JSON
dictionary and outputs inconsistencies.

Semantic errors / Policy errors:  GPT-4 produces configs that do not follow
the intended local policy. We use Batfish "Search Route Policies" for
verification in this step. In case there is a semantic error, Batfish produces
an example where the local policy is not followed. This examples is then fed
to GPT-4 in a fresh prompt.

Classifying into separate categories allowed us to use different tools to
address each one. Table 3 lists examples of the rectifying prompts. Once all
the errors are rectified, we simulate the entire BGP communication using
Batfish as a final step, in order to ensure that the global policy is
satisfied, though the proof technique of Lightyear [9] could instead be used
to ensure that the local policies imply the global one.

###  4.2 Experience and Results

Since some GPT-4 errors were more common, we supplied it an IIP (the Inital
Instruction Prompt) as follows:

CLI prompts: GPT-4 would often generate commands to enter on the Cisco command
line interface, which is undesirable. Thus we specifically asked it to
generate the .cfg files.

Wrong keywords: While generating the configs, it would often use certain
keywords such as ‘exit’, ‘end’, ‘configure terminal’, ‘ip routing’, ‘write’,
‘hostname’ and ‘conf t’. It had a tendency to place some of them in the wrong
locations. Hence, we directed it not to use these keywords. Any extra required
commands for setup were prepended to the final config files, before running
them on Batfish.

Match Community: When trying to match against a community, it sometimes
generates syntax like:
route-map FILTER$\\_$ROUTES permit 10
match community 100:1

This is incorrect. The correct way to match against a community in a route-map
is to first declare a community list that contains the community as in:

ip community-list 1 permit 100:1

and then while matching, make a call to a community list:

route-map FILTER_ROUTES permit 10
match community 1

Thus we included another IIP to define a community list and then in a route-
map, match using only this list.

Adding Communities: While adding communities using a route-map, GPT-4 tends to
generate syntax similar to:
route-map ADD_COUMMUNITY permit 10
set community 100:1

We observed that this happens even when we explicitly ask it to ‘add’ a
community to the route. The above route-map replaces all the communities that
are already present in the route with the community 100:1. So we added an
initial prompt saying that it should always use the ’additive’ keyword when
adding a community to the route.

These initial prompts along with the syntax rectification scheme of Table 3
are able to eliminate common syntax errors produced by GPT-4. Despite this, we
found two egregious cases where human intervention is needed:

Placing neighbor commands in the wrong location: In a config file for BGP, all
network and neighbor commands must be placed under the "router bgp" block. For
example, the neighbor command is used to attach a route-map to the ingress or
egress of an interface. We found that in rare situations, GPT-4 defines a
route-map and then associates it with an interface outside the "router bgp"
block. Batfish is able to catch this syntax error. However, the output is not
informative enough for GPT-4 to be able to fix the issue.

AND/OR Semantics in match statements:  GPT-4 does not understand the semantic
difference between placing multiple match conditions under a single route-map
stanza versus placing them in different stanzas. For no-transit, we had asked
GPT-4 to generate a config for $R1$ that would add a different community to
every route incoming from $R2-R6$ (Figure 4). We also asked it to filter
routes containing any such community on the egress of the interface connecting
$R1$ to $R2-R6$. GPT-4 added the correct communities at the ingress, but at
the egress at $R1$ it incorrectly used AND semantics for filtering routes as
in the following route-map for the $R1-R2$ interface:

⬇

ip community-list 1 permit 100:1

ip community-list 2 permit 101:1

ip community-list 3 permit 102:1

ip community-list 4 permit 103:1

ip community-list 5 permit 104:1

route-map FILTER_COMM_OUT_R2 deny 10

match community 2

match community 3

match community 4

match community 5

route-map FILTER_COMM_OUT_R2 permit 20

Community 100:1 is associated with routes incoming from R2, 101:2 with those
coming from R3 and so on. We desire routes incoming from $R3-R6$ to be
filtered out at the egress to $R2$. The above config will only filter out
routes that have all the communities 101:1, 102:1, 103:1 and 104:1, not any
one of them. When we asked Batfish whether the above route-map filters routes
that have the community 101:1, it produced a counterexample but this
counterexample to GPT-4 failed to rectify the issue. A human prompt was needed
to ask GPT-4 to declare each match statement in a separate route-map stanza.
Our attempts to help GPT-4 distinguish between AND and OR semantics using an
example in the IIP also failed.

Type | Examples |
---|---|---
| Syntax
---
error
|  ‘ip community-list standard
---
COMM_LIST_R2_OUT permit .+’ is wrong syntax.
| Topology
---
error
|  1\. Interface eth0/1 ip address does not match with
---
given config. Expected 2.0.0.1, found 2.0.0.2
2\. Local AS number does not match. Expected 1, found 3
3\. Router ID does not match with given config.
Expected 1.0.0.2, found 1.0.0.1
4\. Neighbor with IP address 1.0.0.1 and
AS 1 not declared
5\. Network 1.0.0.0/24 not declared
6\. Incorrect network declaration. 7.0.0.0/24 is
not directly connected to R1
7\. Incorrect neighbor declaration. No neighbor
with IP address 7.0.0.2 AS 7 found
| Semantic
---
error
|  The route-map DROP_COMMUNITY permits routes
---
that have the community 100:1. However, they should
be denied.
Table 3: Sample rectification prompts for local synthesis. Batfish or the
topology verifier fill in italicized text.

Leverage: The entire cycle took 2 human prompts and 12 automated prompts, for
a leverage of 6X. Note that the AND-OR problem required a final correction
prompt.

##  5 Previous Work

Jigsaw [7] and Copilot [6] use large language models for program synthesis.
While they concentrate on sequential programs, the deeper difference is that
they do not pair the synthesizer with verifiers. Jigsaw [7] does ask users to
provide test cases and tests (but does not verify) the synthesized program.
Jigsaw also does some form of automatic syntax correction doing AST-to-AST
transformations. CoPilot [6] can suggest invariants but does not attempt an
axiomatic proof. Jigsaw and Copilot do not address two questions we do: how to
use a specification, and how to provide localized feedback.

The use of ChatGPT with the Kani Rust verifier [8] comes closest to our
vision; the Kani blog post finesses the specification question (as we do for
Cisco to Juniper) by focusing on program transformations (in their case
optimization) for which the source program is the specification. They also do
not use modularity or local specifications. More fundamentally the Kani [8]
use case does not do prompt programming: the user always manually switches
between the verifier and the LLM, precluding possible leverage.

##  6 Conclusions

Our experiments are very preliminary but suggest:

1\. Ramanujam Effect: As with the mathematician Ramanujam, some of whose
conjectures were incorrect and needed Hardy’s help [1] for proofs, GPT-4 by
itself is not ready for use without a verifier, making elementary errors that
can bring networks down.

2\. Verified Prompt Programming: Using a verifier and automated corrections
via a humanizer, GPT-4 can synthesize reasonable but not completely correct
configurations for simple use cases, but the leverage in reduced human effort
can be high (5X to 10X). Modular verification seems crucial.

4\. Local versus Global Specifications: Modular synthesis is the dual to
modular verification. The search space for the LLM is large, which increases
the chance that it will not be able to correctly complete a synthesis task
based on a global specification. Instead the user needs to decide and describe
the "roles" each node plays in satisfying the global spec.

Much further testing in more complex use cases is needed. Can GPT-4 add a new
policy incrementally without interfering with existing verified policy? While
our paper is set in the context of network configuration, the vision,
definitions (e.g., leverage) and lessons (e.g., the need for actionable local
feedback, modularity, humanizers and IIPs) seem more generally useful to
synthesize other programs.

## References

  * [1] B. Bollobas.  The man who taught infinity: how G.H. Hardy tamed Srinivasa Ramanujan’s genius.  https://theconversation.com/the-man-who-taught-infinity-how-gh-hardy
-tamed-srinivasa-ramanujans-genius-57585, 2023\.
  * [2] E. M. Bender, T. Gebru, A. McMillan-Major, and S. Shmitchell.  On the dangers of stochastic parrots: Can language models be too big?  In Proceedings of the 2021 ACM Conference on Fairness, Accountability, and Transparency, FAccT ’21, page 610–623, New York, NY, USA, 2021. Association for Computing Machinery.
  * [3] S. Bubeck, V. Chandrasekaran, R. Eldan, J. Gehrke, E. Horvitz, E. Kamar, P. Lee, Y. T. Lee, Y. Li, S. Lundberg, H. Nori, H. Palangi, M. T. Ribeiro, and Y. Zhang.  Sparks of artificial general intelligence: Early experiments with GPT-4, 2023.
  * [4] DeepLearning.AI.  ChatGPT Prompt Engineering for Developers.  https://learn.deeplearning.ai/chatgpt-prompt-eng/lesson/1/introduction, 2023\.
  * [5] A. Fogel, S. Fung, L. Pedrosa, M. Walraed-Sullivan, R. Govindan, R. Mahajan, and T. Millstein.  A general approach to network configuration analysis.  NSDI’15, page 469–483, USA, 2015. USENIX Association.
  * [6] github.  Github CoPilot: Your AI Pair Programmer.  https://github.com/features/copilot, 2023.
  * [7] N. Jain, S. Vaidyanath, A. Iyer, N. Natarajan, S. Parthasarathy, S. Rajamani, and R. Sharma.  Jigsaw: Large language models meet program synthesis.  In Proceedings of the 44th International Conference on Software Engineering, ICSE ’22, page 1219–1231, New York, NY, USA, 2022. Association for Computing Machinery.
  * [8] Kani Rust Verifier Blog.  Writing Code with ChatGPT? Improve it with Kani.  https://model-checking.github.io/kani-verifier-blog/2023/05/01/writing-code-with-chatgpt-improve-it-with-kani.html, 2023\.
  * [9] A. Tang, , R. Beckett, K. Jayaraman, T. Millstein, and G. Varghese.  Lightyear: Using modularity to scale BGP control plane verification.  SIGCOMM ’23, to appear. Association for Computing Machinery, 2023.
  * [10] A. Tang, S. K. R. Kakarla, R. Beckett, E. Zhai, M. Brown, T. Millstein, and G. Varghese.  Campion: Debugging router configuration differences.  SIGCOMM ’21, page 748–761, New York, NY, US, 2021. Association for Computing Machinery.