G Chen

M T Pham

T Maalej

H Fourati

R Moreau

S Sesmat

A Biomimetic steering robot for Minimally invasive surgery application

Minimally Invasive Surgery represents the future of many types of medical interventions such as keyhole neurosurgey or transluminal endoscopic surgery. These procedures involve insertion of surgical instruments such as needles and endoscopes into human body through small incision/ body cavity for biopsy and drug delivery. However, nearly all surgical instruments for these procedures are inserted manually and there is a long learning curve for surgeons to use them properly. Many research efforts have been made to design active instruments (endoscope, needles) to improve this procedure during last decades. New robot mechanisms have been designed and used to improve the dexterity of current endoscope. Usually these robots are flexible and can pass the constrained space for fine manipulations. In recent years, a continuum robotic mechanism has been investigated and designed for medical surgery. Those robots are characterized by the fact that their mechanical components do not have rigid links and discrete joints in contrast with traditional robot manipulators. The design of these robots is inspired by movements of natural animals such as tongues, elephant trunks and tentacles. The unusual compliance and redundant degrees of freedom of these robots provide strong potential to achieve delicate tasks successfully even in cluttered and unstructured environments. This chapter will present a complete application of a continuum robot for Minimally Invasive Surgery of colonoscopy. This system is composed of a micro-robotic tip, a set of position sensors and a real-time control system for guiding the exploration of colon. Details will be described on the modeling of the used pneumatic actuators, the design of the mechanical component, the kinematic model analysis and the control strategy for automatically guiding the progression of the device inside the human colon. Experimental results will be presented to check the performances of the whole system within a transparent tube.

Introduction

Robotics has increasingly become accepted in the past 20 years as a viable solution to many applications in surgery, particularly in the field of Minimally Invasive Surgery (MIS) [START_REF] Taylor | Medical robotics in computer-integrated surgery[END_REF]. Minimally Invasive Surgery represents the future of many types of medical interventions such as keyhole neurosurgey or transluminal endoscopic surgery. These procedures involve insertion of surgical instruments such as needles and endoscopes into human body through small incision/ body cavity for biopsy and drug delivery. However, nearly all surgical instruments for these procedures are inserted manually and they are lack of dexterity in small constrained spaces. As a consequence, there is a long learning curve for surgeons to use them properly. Many research efforts have been made to improve the functionalities of current instruments by designing active instruments (endoscope, needles) using robotic mechanisms during the last decades, such as snake robot for throat surgery [START_REF] Simaan | A dexterous system for laryngeal surgery-multibackbone bending snake-like slaves for teleoperated dexterous surgical tool manipulation[END_REF] or active cannula [START_REF] Webster | Mechanics of precurved-tube continuum robots[END_REF]. Studies are currently underway to evaluate the value of these new devices. Usually these robots are micro size and very flexible so that they can pass the constrained space for fine manipulations. Furthermore, how to steer these robots into targets safely during the insertion usually needs additional sensors, such as MRI imaging and US imaging, and path planning algorithms are also needed to be developped for the intervention.

Colonoscopy is a typical MIS procedure that needs the insertation of long endoscope inside the human colon for diagnostics and therapy of the lower gastrointestinal tract including the colon. The difficulty of the insertion of colonoscope into the human colon and the pain of the intervention brought to the patient hinders the diagnostics of colon cancer massively. This chapter will present a novel steerable robot and guidance control strategy for colonoscopy interventions which reduces the challenge associated with reaching the target.

Colonoscopy

Today, colon cancer is an increasing medical concern in the world, where the second frequent malignant tumor is found in industrialized countries [START_REF]Development and in vitro tests of a miniature robotic system for computer-assisted colonoscopy[END_REF]. There are several different solutions to detect this kind of cancer, but only colonoscopy can not only make diagnostics, but make therapy. Colonoscopy is a procedure which is characterized by insertion of endoscopes into the human colon for inspection of the lower gastrointestinal tract including the colon in order to stop or to slow the progression of the illness. The anatomy of the colon is showed in Fig. 1.

Fig. 1. The anatomy of the colon

The instrument used for diagnostics and operation of the human colon is called endoscope (also colonoscope) which is about 1.5cm in diameter and from 1.6 to 2 meters in length. Colonoscopy is one of the most technically demanding endoscopic examinations and tends to be very unpopular with patients because of many sharp bends and constrained workspace. The main reason lies in the characteristics of current colonoscopes, which are quite rigid and require the doctor to perform difficult manoeuvres for long insertion with minimal damage of the colon wall [START_REF] Sturges | A flexible, tendon-controlled device for endoscopy[END_REF][START_REF] Fukuda | Micro active catheter system with multi degrees of freedom[END_REF].

State of the art: Robotic colonoscopy

Since the human colon is a tortuous "tube" with several sharp bends, the insertion of the colonoscope requires the doctor to exert forces and rotations at shaft outside of the patient, thus causing discomfort to the patient. The complexity of the procedure for doctors and the discomfort experienced by the patient of current colonoscopies lead many researchers to choose the automated colonoscopy method. In [START_REF] Phee | Automation of colonoscopy, part one: Locomotion and steering aspects in automation of colonoscopy[END_REF], the authors proposed the concept of automated colonoscopy (also called robotic colonoscopy) from two aspects: locomotion and steering of the distal end, which are the two main actions during a colonoscopy. In order to facilitate the operation of colonoscopy, some studies on the robotic colonoscopy have been carried out from these two aspects. Most current research on autonomous colonoscopies have been focused on the selfpropelled robots which utilize various locomotion mechanisms [START_REF] Ikuta | Shape memory alloy servo actuator system with electric resistance feedback and application for active endoscope[END_REF][START_REF] Slatkin | The development of a robot endoscope[END_REF][START_REF] Dario | A miniature steerable end-effector for application in an integrated system for computer-assisted arthroscopy[END_REF][START_REF] Menciassi | Robotic solutions and mechanisms for a semi-autonomous endoscope[END_REF][START_REF] Kumar | Design of a vision-guided microrobotic colonoscopy system[END_REF][START_REF] Kassim | Review of locomotion techniques for robotic colonoscopy[END_REF]. Among them, inchworm-like locomotion attracted much more attention [START_REF] Slatkin | The development of a robot endoscope[END_REF][START_REF] Dario | A miniature steerable end-effector for application in an integrated system for computer-assisted arthroscopy[END_REF]. However, most of the current inchworm-based robotic systems [START_REF] Slatkin | The development of a robot endoscope[END_REF][START_REF] Dario | A miniature steerable end-effector for application in an integrated system for computer-assisted arthroscopy[END_REF][START_REF] Menciassi | Robotic solutions and mechanisms for a semi-autonomous endoscope[END_REF][START_REF] Kumar | Design of a vision-guided microrobotic colonoscopy system[END_REF] showed low efficiency of locomotion for exploring the colon because of the structure of the colon wall: slippery and different diameters at each section. Another aspect work that could improve the performance of current colonoscopies is to design an autonomous steering robot for guidance inside the colon during the colonoscopy. Fukuda et al. [START_REF] Fukuda | Micro active catheter system with multi degrees of freedom[END_REF] proposed Shape Memory Alloy (SMA) based bending devices, called as Micro-Active Catheter (MAC), with two degrees of freedom. With three MACs connected together in series, an angle of bend of nearly 80 • is possible. In [START_REF] Menciassi | Robotic solutions and mechanisms for a semi-autonomous endoscope[END_REF], a bendable tip has been also designed and fabricated by using a silicone bellows with a length of 30mm. It contains three small SMA springs with a 120 • layout. This device allows a 90 o bending in three directions. These flexible steering tips are are only parts of the whole self-propelling robots, however those works did not focus on how to control this special robot to endow it with a capability for autonomous guidance [START_REF] Menciassi | Robotic solutions and mechanisms for a semi-autonomous endoscope[END_REF][START_REF] Kumar | Design of a vision-guided microrobotic colonoscopy system[END_REF][START_REF] Piers | Design of an advanced tool guiding system for robotic surgery[END_REF][START_REF] Kim | Inchworm-like colonoscopic robot with hollow body and steering device[END_REF]. Since 2001, there is another method to perform colon diagnostics: capsule endoscopy [16,17]. With a camera, a light source, a transmitter and power supply integrated into a capsule, the patient can swallow and repel it through natural peristalsis without any pain. Although capsule endoscopy has the advantage in contrast with current endoscopy, capsule endoscopy can't be used to perform the diagnostics more thoroughly and actively. Recently, different active locomotion mechanisms have been investigated and designed to address this problem, such as clamping mechanism [START_REF] Menciassi | Shape memory alloy clamping devices of a capsule for monitoring tasks in the gastrointestinal tract[END_REF], SMA-based [START_REF] Gorini | A novel sma-based actuator for a legged endoscopic capsule[END_REF][START_REF] Kim | Design and fabrication of a locomotive mechanism for capsule-type endos using shape-memory alloys (sma)[END_REF], magnetbased [START_REF] Wang | ieee/rsj international conference on intelligent robots and systems[END_REF] locomotion and biomimetic gecko [START_REF] Glass | A legged anchoring mechanism for capsule endoscopes using micropatterned adhesives[END_REF] .

An approach to steering robot for colonoscopy

The objective of our work in this chapter is different from all the works from other laboratories, which is to design a robot with high dexterity capable of guiding the progression with minimal hurt to the colon wall. Our approach emphasizes a robotic tip with a novel design mounted on the end of the traditional colonoscope or similar instruments. The whole system for semi-autonomous colonoscopy will be presented in this chapter. It is composed of a microtip, which is based on a continuum robot mechanism, a proximity multi-sensor system and high level real-time control system for guidance control of this robot. The schema of the whole system, called Colobot, is shown in Fig. 2. Section 2 briefly presents the Colobot and its proximity sensor system. Then section 3 will present model analysis of Colobot system and the validation of kinematic model in section 4. In section 5 guidance control strategy is presented and control architecture and implementation will be described in Section 5.2. Finally, experimental results in a colon-like tube will be presented to verify the performance of this semiautonomous system. Biologically-inspired continuum robots [START_REF] Robinson | Continuum robots -a state of the art[END_REF] have attracted much interest from robotics researchers during the last decades to improve the capability of manipulation in constrained space. These kinds of systems are characterized by the fact that their mechanical components do not have rigid links and discrete joints in contrast with traditional industry robots. The design of these robots are inspired by movements of natural animals such as tongues, elephant trunks and tentacles etc. The unusual compliance and redundant degrees of freedom of these robots provide strong potential to achieve delicate tasks successfully even in cluttered and/or unstructured environments such as undersea operations [START_REF] Lane | The amadeus dextrous subsea hand: Design, modeling, and sensor processing[END_REF], urban search and rescue, wasted materials handling [START_REF] Immega | The KSI tentacle manipulator[END_REF], Minimally Invasive Surgery [START_REF] Simaan | A dexterous system for laryngeal surgery-multibackbone bending snake-like slaves for teleoperated dexterous surgical tool manipulation[END_REF][START_REF] Dario | A miniature steerable end-effector for application in an integrated system for computer-assisted arthroscopy[END_REF][START_REF] Piers | Design of an advanced tool guiding system for robotic surgery[END_REF][START_REF] Bailly | Modeling and control of a hybrid continuum active catheter for aortic aneurysm treatment[END_REF]. The Colobot [START_REF] Chen | Development and kinematic analysis of a silicone-rubber bending tip for colonoscopy[END_REF] designed for our work, is a small-scaled continuum robot. Due to the size requirement of the robot, there are challenges on how to miniaturize sensor system integrated into the small-scale robot to implement automatic guidance of progression inside the human colon. This section will present the detailed design of the Colobot and its fibre-optic proximity sensor system.

Colobot

The difference between our robotic tip and other existing continuum robots is the size. Our design is inspired by pioneer work [START_REF] Suzumori | Applying a flexible-micro-actuator robotic mechanisms[END_REF] on a flexible microactuator (FMA) based on silicone rubber. Fig. 3(a) shows our design of the Colobot. The robotic tip has 3 DOF (Degree of Freedom), which is a unique unit with 3 active pneumatic chambers regularly disposed at 120 degrees apart. These three chambers are used for actuation; three other chambers shown in fig. 3(b) are designed to optimize the mechanical structure in order to reduce the radial expansion of active chambers under pressure. The outer diameter of the tip is 17 mm that is lesser than the average diameter of the colon. The diameter of the inner hole is 8mm, which is used in order to place the camera or other lighting tools. The weight of the prototype is 20 grams. The internal pressure of each chamber is independently controlled by using pneumatic jet-pipe servovalves. The promising result obtained from the preliminary experiment showed that this tip could bend up to 120 • and the resonance frequency is 20 Hz.

Modeling and experimental characterization of pneumatic servovalves

During an electro-pneumatic control, the follow up of the power transfer from the source to the actuator is achieved through one or several openings with varying cross-section called restrictions: this monitoring organ is the servovalve [START_REF] Sesmat | Modélisation, simulation et commande d'une servovalve electropneumatique[END_REF]. The COLOBOT device is provided by three jet pipe microservovalves Atchley 200PN [START_REF] Controls | [END_REF], which allow the desired modulation of air inside the different active chambers in Fig. 3(b). In this component, a motor is connected to an oscillating nozzle, which deflects the gas stream to one of the two cylinder chambers (Fig. 4(a)). A voltage/current amplifier allows to control the servovalves by the voltage [START_REF] Atchley | A more reliable electrohydraulic servovalve[END_REF]. A first pneumatic output of this component is directly connected to one of the robot chambers, and a second output is left unconnected. A sensor pressure (UCC model PDT010131) (Fig. 4(b)) is used to measure the pressure in each of the three COLOBOT robot chambers. The measured pressure, comprised between 0 and 10 bars, was used to determine the servovalve control voltage. As the three servo valves used for the COLOBOT actuator are identical, a random servovalve was chosen for the mass flow and pressure characterization. The pressure gain curve is the relationship between the pressure and the current control when the mass flow rate is null. It is performed by means of the pneumatic test bench shown in Fig 5 . A manometer was placed downstream of the servovalve close by the utilization orifice in order to measure the pressures. Fig. 6 shows the pressure measurements P n and P p carried out for an increasing and a decreasing input current. It appears that the behavior of the servovalve is quite symmetric but with a hysteresis cycle. Arrival in stop frame couple creates pressure saturation at -18 mA, respectively +18 mA, for the negative current, respectively for the positive current. In the Fig. 5, we substitute the manometer on the test bench for a static mass flow-meter to plot the mass flow rate gain curve (mass flow rate with respect to the input current). This curve presented in Fig. 7 shows a non linear hysteresis.

Because of the specific size of Colobot's chambers, the experimental mass flow rate inside the the chamber is very small, the current input and the pressure variations are small enough to neglect the hysteresis and consider linear characteristics for Fig. 6 and Fig. 7.

Optical Fibre proximity sensors

The purpose of this robotic system is to guide the insertion of the colonoscope through the colon. So it is necessary to integrate the sensors to detect the position of the tip inside the colon. Due to the specific operation environments and the small space constraint, two important criteria must be taken into account to choose the distance sensors:

• the flexibility and size of the colonoscope, • the cleanliness of the colon wall.

Tests have been performed using ultrasound and magnetic sensors as well as optical fibre. We decided to use optical fibre because of its flexibility, small size, high resolution, and the possibility of reflecting light off the porcine intestinal wall [16].This optical fibre system consists of one emission fibre and a group of four reception fibres (Fig. 8(a)). The light is emitted from a cold light source and conveyed by transmission fibres. After reflection on an unspecified body in front of the emission fibre, the reception fibres surrounding the emission fibre detect the reflected light. The amount of reflected light detected is a function of the distance between the sensor and the body. Figure 8(b) shows the output voltage determined by the distance between the sensor and the porcine intestinal wall. This curve shows that the sensor's resolution is sufficient for detecting the intestinal wall up to 8 mm. Fig. 9 shows the Colobot integrated three fibre optic proximity sensors. The first optical fibre is placed in front of the first pneumatic chamber and the other two in front of their individual pneumatic chambers.

Kinematic analysis of the robotic tip

Fig. 10 shows the robot shape parameters and the corresponding frames. The deformation shape of ColoBot is characterized by three parameters as done in our previous prototype EDORA [START_REF] Chen | Design and control of an actuator for colonoscopy[END_REF]. It is worth to note that [START_REF] Simaan | A dexterous system for laryngeal surgery-multibackbone bending snake-like slaves for teleoperated dexterous surgical tool manipulation[END_REF][START_REF] Lane | The amadeus dextrous subsea hand: Design, modeling, and sensor processing[END_REF][START_REF] Bailly | Modeling and control of a hybrid continuum active catheter for aortic aneurysm treatment[END_REF][START_REF] Suzumori | Applying a flexible-micro-actuator robotic mechanisms[END_REF][START_REF] Ohno | Design of slim slime robot and its gait of locomotion[END_REF][START_REF] Jones | Kinematics for multi-section continuum robots[END_REF] used almost the same set of parameters for the modeling:

• L is the length of the virtual center line of the robotic tip • α is the bending angle in the bending plane • φ is the orientation of the bending plane

The frame R u (O-xyz) is fixed at the base of the actuator. The X-axis is the one that passed by the center of the bottom end and the center of the chamber 1. The XY-plane defines the plane of the bottom of the actuator, and the z-axis is orthogonal to this plane. The frame R s (u, v, w) is attached to the top end of the manipulator. So the bending angle α is defined as the angle between the o-z axis and o-w axis. The orientation angle φ is defined as the angle between the o-x axis and o-t axis, where o-t axis is the project of o-w axis on the plan x-o-y. Given the assumption that the shape at the bending moment is an arc of a circle, the geometry-based kinematic model [START_REF] Chen | Design and control of an actuator for colonoscopy[END_REF] relating the robot shape parameters to the actuator inputs (chamber length) is expressed as follows:

                     L = 1 3 3 i=1 L i φ = atan2 √ 3(L 2 -L 3 ) L 3 + L 2 -2L 1 α = 2 √ λ L 3r (1)
where

λ L = L 1 2 + L 2 2 + L 3 2 -L 1 L 2 -L 2 L 3 -L 3 L 1 and
r is the radius of the Colobot. And the direct kinematic equations with respect to the input pressures are represented by:

                       L = L 0 + 1 3 3 I=1 f i (P i ) φ = atan2 √ 3(f 2 (P 2 ) -f 3 (P 3 )) f 3 (P 3 ) + f 2 (P 2 ) -2f 1 (P 1 ) α = λ p h (2)
where:

λ p = f 1 (P 1 ) 2 + f 2 (P 2 ) 2 + f 3 (P 3 ) 2 -f 1 (P 1 )f 2 (P 2 ) -f 2 (P 2 )f 3 (P 3 ) -f 3 (P 3 )f 1 (P 1 )
The function f i (P i ) (i = 1, 2, 3) shows the relationship relating the stretch length of the chamber to the pressure variation of the silicone-based actuator as described as:

∆L i = f i (P i ) (3)
Where ∆L i (i = 1, 2, 3) is the stretch length of each chamber with corresponding pressure and f i (i = 1, 2, 3) is a nonlinear function of P i . The corresponding results can be written as:

                                                       if P 1min < P 1 < P 1max ∆L 1 = 37(P 1 -P 1min ) 3 -54(P 1 -P 1min ) 2 -9.5(P 1 -P 1min ) if P 2min < P 2 < P 2max ∆L 2 = -9(P 2 -P 2min ) 3 -18(P 2 -P 2min ) 2
-11(P 2 -P 2min ) if P 3min < P 3 < P 3max ∆L 3 = 0.8(P 3 -P 3min ) 3 -8.9(P 3 -P 3min ) 2 -34(P 3 -P 3min ) [START_REF]Development and in vitro tests of a miniature robotic system for computer-assisted colonoscopy[END_REF] where P imin (i = 1, 2, 3) is the threshold of the working point of each chamber and their values equal: P 1min = 0.7 bar, P 2min = 0.8 bar, P 3min = 0.8 bar and P imax (i = 1, 2, 3) is the maximum pressure that can be applied into each chamber. The detailed deduction of these equations can be found in [START_REF] Chen | Design and control of an actuator for colonoscopy[END_REF]. The Cartesian coordinates (x, y, z) of the distal end of Colobot in the task space related to the robot bending parameters is obtained through a cylindrical coordinate transformation:

                     x = L α (1 -cos α) cos φ y = L α (1 -cos α) sin φ z = L α sin α (5)
And the state-space form of this model is given by:

X = f (Q p ) (6)
where X = (α, φ, L) T , Q p = (P 1 , P 2 , P 3 ) T .

Modeling and calibration of optical fibre sensors

For the preliminary test of our system, a transparent tube will be used which will be detailed in section6. So the distance model of the optical fibre sensors with respect to this tube needs to obtained before performing the test. Experimental methods are uses to obtain the model of each sensor. The voltage (u i in volts) with respect to the distance (d i in mm) between the sensor and the tube wall is measured. Fig. 11 shows the measurements and the approximation model of the third sensor. The model of each sensor is obtained as follows: Since the kinematics of Colobot has been described as the relationship between the deflected shape and the lengths of the three chambers (three pressures of each chamber), the validation of the kinematic model needs to have a sensor to measure the deflected shape, i.e. the bending angle, the arc length and the orientation angle. This section first presents sensor choice and its experimental setup for determining these system parameters, and presents the validation of the static kinematic model.

u 1 = -40 3.2d 2 1 + 3 (7) u 2 = -50 1.6d 2 2 + 2.2 (8)
u 3 = -38 1.7d 2 3 + 2.3 (9)

The sensor choice and experimental setup

For most continuum style robots, the determination of the manipulator shape is a big problem because of the dimension and the inability to mount measurement device for the joint angles. Although there are several technologies that could solve this problem for large size robots [START_REF] Ohno | Design of slim slime robot and its gait of locomotion[END_REF], they are difficult to implement on a micro-robot. Since a Cartesian frame has been analyzed with relation to the deflected shape parameters, an indirect method is used to validate the kinematic model with the 3D position measurement. For this purpose, an electromagnetic miniBIRD sensor is used for the experimental validation.

MiniBIRD is a six degree-of-freedom (position and orientation) measuring device from Ascension Technology Corporation [35]. It consists of one or more Ascension Bird electronic units, a transmitter and one or more sensors, see Fig. 12. It offers full functionality of other magnetic trackers, with miniaturized sensors as small as 5mm wide. For data acquisition, the bottom of Colobot 2). As for the validation of bending angle, one orientation of Colobot movement is used for validation. The bending angle is directly measured from the miniBIRD sensor and compared with theoretical results from actual pressure obtained from the proportional valves. As shown in Fig. 14, the bending angle concerning the chamber length and the chamber pressure respectively has almost the same characteristics compared with the actual measurements.

To check the orientation angle, the position in the XY frame coordinate of the top-end of Colobot are measured for the six principal directions of the manipulator. Firstly, expected pressure combinations were used for Colobot to follow the six principal orientation angles (0 • , 60 • , 120 • , 180 • , 240 • , 300 • ) while the bending angle varied from 0 • to the maximum. Then the measured positions of the top-end of Colobot were plotted relative to the original position of Colobot without deformation. This experimental protocol leads to Fig. 15. This figure highlights that the six orientation angles are in accordance with the theoretical values except for high pressures in the chambers.

Verification of the coupling between each chamber

Section 4.2 validated the bending angle and orientation angle separately in static. However, most of the time the motion of the device results from the pressure differentials between each chamber, this is to say, the interaction of each chamber. So it is necessary to check this mutual interaction between each chamber. To achieve this goal, sinus reference signals of pressure with 120 • delay are applied to each servovalve. They are employed to make Colobot turn around its vertical axis with a constant velocity (see the experimental setup Fig. 13) to see the mutual interaction of each chamber. By using miniBIRD, the endpoint coordinates of Colobot can be obtained in XOY plane. Thus the comparison between these coordinates and those obtained from the simulation of the kinematic model (Eq. 5) allows us to check if there are interactions of each chamber on the elongation of the prototype. Two comparisons are then proposed in Figures 16 and17. For the first case, three sinus signals of pressure with amplitude of 0.4 bar and an offset of 0.9 bar are applied in the chambers of the prototype. The path of the endpoint of Colobot is a form of triangle (Fig. 16) because these actuators of Colobot work across the threshold of their dead zones. For the latter case, three sinus signals of pressure with amplitude of 0.4 bar and an offset of 1.2 bar are applied in the chamber of Colobot. In this case, Colobot works in the working zone and the endpoint path of Colobot lead to a circular shape (Fig. 17). The lines in the outer layer are the simulation result from the kinematic model relating XY coordinates to the corresponding pressure of each chamber (Eq. 4). Since the characteristics of deformation under pressure is performed each chamber by each chamber independently (Eq. 4), the difference between the results of simulation and the experimental results showed in Figure 16 and Figure 17 suggests that there exist interactions among each chamber. This interaction is taken into account in section 4.4.

Estimation of a correction parameter

In this section, new parameters are chosen to represent the interactions between each chamber. Thus, six stiffness parameters are introduced to describe the coupling effect of stretching of one chamber to that of other two chambers. Let denotes k ij the mutual stiffness that determines the effect of P i (i=1,2,3) on the length of the chamber j (j = 1,2,3) (where i does not equal j). The coefficients are obtained by minimizing the difference between the operational coordinates (X s , Y s ) measured by miniBIRD and the operational coordinates (X m , Y m ) obtained by simulation of the kinematic model (Fig. 18).

A classical non-linear optimization based on the Levenberg-Marquardt algorithm is proceeded to adjust the unknown parameters k ij . The cost criterion

J(k ij ) = (X s ) 2 + (Y s ) 2 -k ij (X m ) 2 + k ij (Y m ) 2 ) ( 10
)
The numerical results roughly lead to the same coefficient k = 0.3 for the unknown parameters k ij . Thus the new expression of the kinematic model is given by:

             ∆L 1 = f 1 (P 1 ) + 0.3(f 2 (P 2 ) + f 3 (P 3 )) ∆L 2 = f 2 (P 2 ) + 0.3(f 1 (P 1 ) + f 3 (P 3 )) ∆L 3 = f 3 (P 3 ) + 0.3(f 1 (P 1 ) + f 2 (P 2 )) (11)
It is noteworthy that the elongation expression ∆L 1 (respectively ∆L 2 , ∆L 3 ) in (Eq. 11) is equivalent to (Eq. 3) when the relative pressures P 2 and P 3 (respectively P 1 , P 3 and P 1 , P 2 ) are equal to zero.

To check this new kinematic model a cross validation is made with three other experiments. Three sinus input pressures with amplitude from 0.1 bar to 0.3 bar are applied into three chambers of Colobot. The improved kinematic model with the correction coefficient k is used to a straightforward comparison with the sets of data. Results shown in Fig. 19 and Fig. 20 are testimony to the behavior of the proposed model in these two cases.

5 Guidance control strategy based on proximity multi-sensor system

Guidance control strategy

The objective of sensor-based guidance strategy is to calculate the safe position of the distal-end of Colobot compared to the colon wall in real-time based on the measurements of three distance sensors for guidance inside the colon. For the sake of simplicity but without loss of generality, it is assumed that a colon is a cylindrical tube and its cross section is an ellipse at the sensor plane. Fig. 21 illustrates the sensor plane, the distal end of ColoBot and the colon axis. With these assumptions, the safe position will be the central axis of the colon. To approximate the colon axis, a method based on a circumscribed circle is proposed. Since three points D 1 , D 2 and D 3 (Fig. 22) of sensor measurements

Colon

Colon axis

Sensor plan form a triangle, the center of the circumscribed circle of this triangle is chosen as the safe position. This approach iterates as following:

• Three sensor measurements are collected.

• Position P n in the frame R s (Fig. 22) is evaluated with these three measurements. • If P n is a safe position, then it's necessary to go back to the first step for the next period; otherwise, next the safe position P n+1 described in the Frame R u (Fig. 22) is calculated through the circumscribed method and is provided to the kinematic control for execution.

For more details about the guidance control strategy, please find the reference [START_REF] Chen | Sensor-based guidance control of a continuum robot for a semi-autonomous colonoscopy[END_REF].

Guidance control architecture

The control of Colobot is organized in three hierarchical levels, as shown in Fig. 23. The first level consists of local pressure control of each chamber of the Colobot through three servovalves. Three independent PI controllers are used to implement the closed-loop pressure control of the chamber. The position and orientation of Colobot are controlled at level 2 using an instantaneous inverse Jacobian method. This section will describe the implementation detail. Level 3 is the sensor-based planning for automatic navigation described in section 5.1.

Initialisation

Formulation of task space control of Colobot

After determining the desired trajectory from sensor-based planning, the kinematic control of Colobot will be described in this section. It should be noted that two variables are used to represent the position of Colobot inside the colon. However, the Colobot has 3 degrees of freedom. So this manipulator becomes redundant for the chosen task. The velocity kinematic equations are rewritten as following:

X = f (Q p ) Ẋ = ∂X ∂(α, φ, L) ∂(α, φ, L) ∂Q L ∂Q L ∂Q P Qp or Ẋ = J s J l J p Qp = J Qp (12)
where X = (x, y) T , Q L = (L 1 , L 2 , L 3 ) T , Q p = (P 1 , P 2 , P 3 ) T and J = J s J l J p is the Jacobian matrix with relation to the three levels of pressure in the chambers.

Resolution of the inverse kinematics with redundancy

In the case of a redundant manipulator with respect to a given task, the inverse kinematic problem admits infinite solutions. This suggests that redundancy can be conveniently exploited to meet additional constraints on the kinematic control problem in order to obtain greater manipulability in terms of the manipulator configurations and interaction with the environment. A viable solution method is to formulate the problem as a constrained linear optimization problem. Work on resolved-rate control [START_REF] Whitney | Resolved motion rate control of manipulators and human prostheses[END_REF] proposed to use the Moore-Penrose pseudo inversion of the Jacobian matrix as:

Qp = J + Ẋ = (J T (JJ T ) -1 ) Ẋ (13)
In our case, however, there is a mechanical limit range for the elongation of each chamber and the corresponding pressure applied into the chamber of the Colobot. The objective function is constructed to be included in the inverse Jacobian algorithms as the second criteria also called the null-space method [START_REF] Hollerbach | Redundancy resolution of manipulator through torque optimization[END_REF][START_REF] Nakamura | Advanced robotics, Redundancy and Optimization[END_REF].

Qp = J + Ẋ + µ[I -J + J] ġ ( 14
)
where I is the identity matrix, µ is constant and g is a second criterion for the optimization of the solution. This objective function evaluates the pressure difference between the applied pressure in the chamber and the average pressure applied in the chamber. So the cost function w(P ) is expressed as follows:

w(P ) = 1 3 This section will present the implementation of the whole system and experimental results of automatic guidance capability of this system in a colon-like tube.

Hardware implementation

Fig. 24 shows the low-level control system of ColoBot. The pressurized air comes through the compressor (1) and the general pressure is adjusted thanks to the device (2). The pressure in the chambers are controlled by three Jetpipe servovalves (3a, 3b and 3c). Three pressure sensors (4a, 4b and 4c) are connected between the servovalves and the Colobot (5) for the pressure feedback control. Suitable drivers and amplifiers in the rack (6) were designed to amplify control signals applied to the actuator. A real-time controller is implemented through a DSpace board and coupled with the Real-Time Workshop of Simulink. The Simulink block diagram designed for path planning and kinematics algorithms are expressed with Simulink block diagram which will be compiled as real-time executable under the DSP Processor of the DSpace board. The system runs at 500 Hz for a real-time control loop.

Experimental results in a colon-like tube

A more realistic experiment to test the performance of this semi-autonomous colonoscopy system is to use a colon-like transparent tube to see if Colobot can cross the tube with minimal contact with the tube wall. The diameter of the tube is 26 mm and its length is 50 cm (Fig. 25). For this guidance experiment, the calibration of the optical fibres was adapted to the transparent tube. It is highly probable that results for the distance sensors in a porcine intestine will be similar to those obtained in the human bowel. However, the locomotion of the system is manually operated. The evolution of the measurements of three

CONCLUSIONS AND FUTURE WORKS

This paper presented a complete robotic system for semi-autonomous colonoscopy. It is composed of a microtip, a proximity multi-sensor system and high level real-time control system for guidance control of this robot. This system was focused on its guidance ability of endoscope inside the human colon with the In the near future, the proposed method will be tested in a vitro environment.

Fig. 2 .

 2 Fig. 2. The scheme of the whole system

Fig. 3 .

 3 Fig. 3. Colobot and its cross section

Fig. 4 .

 4 Fig. 4. Atchley servovalve and pressure sensor

Fig. 5 .Fig. 7 .

 57 Fig. 5. Pressure gain pneumatic characterization bench

  Fig. 8. Proximity sensors and its characterisation

Fig. 9 .Fig. 10 .

 910 Fig. 9. Prototype integrated with optical fibre proximity sensors

Fig. 11 .

 11 Fig. 11. modeling of optical fiber sensor

Fig. 12 .

 12 Fig. 12. MiniBIRD 6 DOF magnetic sensor

Fig. 13 .

 13 Fig. 13. Measurement configuration

Fig. 14 .Fig. 15 .

 1415 Fig. 14. Comparisons of the bending angle with relation to the chamber length and chamber pressure

Fig. 16 .

 16 Fig. 16. Simulation et experimental results of the movement of the Colobot's tip (across dead zone)

Fig. 17 .

 17 Fig. 17. Simulation and experimental results of the movement of the endpoint of Colobot

Fig. 18 .

 18 Fig. 18. Optimization model

Fig. 19 .Fig. 20 .

 1920 Fig. 19. Verification of corrected with different pressure inputs (across dead zone)

Fig. 21 .Fig. 22 .

 2122 Fig. 21. Position of Colobot inside the colon

Evaluation of d 1 ,Fig. 23 .

 123 Fig. 23. sensor-based planning and guidance control procedure

Fig. 24 .

 24 Fig.[START_REF] Lane | The amadeus dextrous subsea hand: Design, modeling, and sensor processing[END_REF]. The implementation of the whole system optical fibres are represented in the left Fig.26(a). During the entire movement, the distances are never less than 0.8 mm. This demonstrates that the colonoscope tip is moving through the tube without touching it. For a better representation and visualization, Fig.26(b)shows the extreme positions of the top-end of Colobot as it progresses (with a velocity of 4 cm/s). The position of the Colobot at the centre of the tube is represented by the smallest circle. The larger circle represents the tube wall and the line shows the extreme positions of Colobot. This experiment demonstrates that Colobot has the capability to guide the exploration of the tube with a sensor-based steering control method.

Fig. 25 .

 25 Fig. 25. Guidance control test in a colon-like tube

Fig. 26 .

 26 Fig.[START_REF] Bailly | Modeling and control of a hybrid continuum active catheter for aortic aneurysm treatment[END_REF]. Guidance control result analysis fiber optic proximity sensors. Colobot is a continuum robot made of silicone rubber. It has three DoF with its outer diameter of 17mm and the weight of 20 gram. The pneumatic actuators of ColoBot are independently driven through three servovalves. The kinematic model of this soft robot was developed based on the geometric deformation and validated its correction. A method based on a circumscribed circle is utilized to calculate the safe reference position and orientation of the Colobot. While kinematic-based orientation control used these reference paths to adjust the position of Colobot inside the colon to achieve guidance. Experimental results of guidance control with a transparent tube verified the effectivity of kinematic control and guidance control strategy. In the near future, the proposed method will be tested in a vitro environment.


Leonardo Trujillo
email: leonardo.trujillo.ttl@gmail.com

Sara Silva

Pierrick Legrand
email: pierrick.legrand@u-bordeaux2.fr

Leonardo Vanneschi
email: vanneschi@disco.unimib.it

An empirical study of functional complexity as an indicator of overfitting in Genetic Programming

Recently, it has been stated that the complexity of a solution is a good indicator of the amount of overfitting it incurs. However, measuring the complexity of a program, in Genetic Programming, is not a trivial task. In this paper, we study the functional complexity and how it relates with overfitting on symbolic regression problems. We consider two measures of complexity, Slope-based Functional Complexity, inspired by the concept of curvature, and Regularity-based Functional Complexity based on the concept of H ölderian regularity. In general, both complexity measures appear to be poor indicators of program overfitting. However, results suggest that Regularity-based Functional Complexity could provide a good indication of overfitting in extreme cases.

Introduction

In the field of Genetic Programming (GP), a substantial amount of research focuses on the bloat phenomenon Bloat is an excess of code growth without a corresponding improvement in fitness [START_REF] Silva | Dynamic limits for bloat control in genetic programming and a review of past and current bloat theories[END_REF], and it can cause several types of problems during a GP run. For instance, bloat can stagnate a GP search because when program trees become excessively large then fitness evaluation can turn into a computational bottleneck. Moreover, it is also assumed that bloat is related to overfitting, one of the most important problems in machine learning. It is often stated that simpler solutions will be more robust and will generalize better than complex ones, with the latter being more likely to overfit the training data [START_REF] Mitchell | Machine Learning[END_REF][START_REF] Vanneschi | Measuring bloat, overfitting and functional complexity in genetic programming[END_REF]. The GP community has tacitly assumed that simple solutions can be equated with small program trees, and that very large programs correspond to complex solutions [START_REF] Rosca | Generality versus size in genetic programming[END_REF]. Therefore, bloat was assumed to be a good indicator of program overfitting. However, recent experimental work suggests that this assumption is not reliable [START_REF] Vanneschi | Measuring bloat, overfitting and functional complexity in genetic programming[END_REF]. In particular, [START_REF] Vanneschi | Measuring bloat, overfitting and functional complexity in genetic programming[END_REF] showed that a causal link between bloat and overfitting did not exist on three test cases. From this it follows that bloated programs should not be a priori regarded as complex. This leads us towards two important questions. First, how can program complexity be measured? And second, can program complexity be used as an indicator of program overfitting? Here, we study the measure of functional complexity proposed in [START_REF] Vanneschi | Measuring bloat, overfitting and functional complexity in genetic programming[END_REF], which we call Slope-based Functional Complexity (SFC). SFC in inspired by the concept of curvature, and represents the first measure of complexity that is explicitly intended to be an indicator of program overfitting. While SFC is based on a reasonable intuition, the methodological approach it requires can become complicated for multidimensional problems. Therefore, we propose a measure of complexity based on the concept of H ölderian regularity, and we call it Regularity-based Functional Complexity (RFC), which captures the underlying justification of SFC without being hampered by some of its practical difficulties. Both measures are experimentally tested on two real world problems and compared based on their correlation with overfitting [START_REF] Vanneschi | Measuring bloat, overfitting and functional complexity in genetic programming[END_REF].

Overfitting

Based on [START_REF] Mitchell | Machine Learning[END_REF][START_REF] Vanneschi | Measuring bloat, overfitting and functional complexity in genetic programming[END_REF], for a GP search in program space P an individual program p ∈ P overfits the training data if an alternative program p ′ ∈ P exists such that p has a smaller error than p ′ over the training samples, but p ′ has a smaller error over the entire distribution of instances. In the above terms, overfitting is practically impossible to measure because it requires an exhaustive search over P and the entire distribution of instances. Nevertheless, [START_REF] Vanneschi | Measuring bloat, overfitting and functional complexity in genetic programming[END_REF] argues that a good approximation can be obtained with the relationship between fitness computed on the training set and fitness computed on an independent test set. In our work, we use the measure for overfitting proposed in [START_REF] Vanneschi | Measuring bloat, overfitting and functional complexity in genetic programming[END_REF]; which proceeds as follows for a minimization problem. If at generation g test fitness is better than training fitness, then (overf itting(g) = 0); if test fitness is better than the best test fitness obtained thus far then (overf itting(g) = 0); otherwise, overfitting is quantified by the difference of the distance between training and test fitness at generation g and the distance between training and test fitness at the generation when the best test fitness was obtained. In this procedure, test fitness is computed only for the best individual of the population, the individual with the best training fitness. This individual is chosen because we want to measure the overfitting of the best GP solution, since this is the individual that will be returned at the end of the search. If elitism is used then training fitness will be monotonically decreasing, thus overf itting(g) ≥ 0 ∀g.

Therefore, overfitting depends on the performance of a program on the test dataset. In the best case scenario, the test set is a representative sample of the unseen data that a program might encounter during on-line operation. However, it might also be true that an independent test set could be difficult to produce or might be unavailable. Therefore, an indicator of program overfitting would be a useful practical tool. In this sense, [START_REF] Vanneschi | Measuring bloat, overfitting and functional complexity in genetic programming[END_REF] suggests that program complexity could indicate if overfitting is present during a GP run.

Program complexity could be measured in different ways. For instance, [START_REF] Vladislavleva | Order of nonlinearity as a complexity measure for models generated by symbolic regression via pareto genetic programming[END_REF] proposed two measures. The first is to equate complexity with tree size, based on the assumption that bloated programs are also complex. The second addresses the complexity of the program output or functional complexity, measured as the degree of the Chebyshev polynomial that approximates the output. In [START_REF] Vladislavleva | Order of nonlinearity as a complexity measure for models generated by symbolic regression via pareto genetic programming[END_REF] complexity is studied as an objective that should be optimized, not as an indicator of program overfitting, which could be studied in future work.

Functional complexity

If we are describing the complexity of a program, focusing on the functional output seems to be the best approach for several reasons. First, the size and shape of a program might be misleading if many nodes are introns, in which case they have no bearing on program output. Moreover, even a large program might be simplified and expressed as a compact expression. The size of the program influences the dynamics of the evolutionary process, but tells us little with respect to the output of each program. Secondly, the genotype-phenotype distinction is not clear in GP, where an explicit phenotype is normally not defined [START_REF] Mcdermott | A fine-grained view of GP locality with binary decision diagrams as ant phenotypes[END_REF]. Therefore, it is easier to focus on the functional output of a program in order to describe its behavior. Here, we describe two measures of functional complexity. We begin with the SFC measure proposed in [START_REF] Vanneschi | Measuring bloat, overfitting and functional complexity in genetic programming[END_REF], and afterwards present our proposed RFC measure. It is important to state that despite the differences between SFC and RFC, it should become clear that both are concerned with measuring the same underlying characteristic of functional behavior.

Slope-based Functional Complexity

The complexity measure proposed in [START_REF] Vanneschi | Measuring bloat, overfitting and functional complexity in genetic programming[END_REF] is inspired by the concept of function curvature. Curvature is the amount by which the geometric representation of a function deviates from being flat or straight. In [START_REF] Vanneschi | Measuring bloat, overfitting and functional complexity in genetic programming[END_REF], the authors correctly point out that a program tree with a response that tends to be flat, or smooth, should be characterized as having a low functional complexity, and that such a function will tend to have a lower curvature at each sampled point. Conversely, a complex functional output would exhibit a larger amount of curvature at each point. This basic intuition seems reasonable, but computing a measure of curvature is not trivial [START_REF] Morvan | Generalized Curvatures[END_REF], especially for multidimensional real-world problems. In order to overcome this, [START_REF] Vanneschi | Measuring bloat, overfitting and functional complexity in genetic programming[END_REF] proposes a heuristic measure based on the slope of the line segments that join each pair of adjacent points. Consider a bi-dimensional regression problem, for which the graphical representation of the output of a program is a polyline. This polyline is produced by plotting the points that have fitness cases in the abscissa, the corresponding values of the program output as ordinates, and sorting the points based on the fitness cases. Then, these points are joined by straight line segments and the slope of each segment is computed. The SFC is calculated by summing the differences of adjacent line segments. If the slopes are identical, the value of the measure is zero, thus a low complexity score. Conversely, if the sign of the slope of all adjacent segments changes then complexity is high.

The intuition behind SFC seems to be a reasonable first approximation of a complexity measure that could serve as a predictor of GP overfitting. However, the formal definition of SFC can become complicated for multidimensional problems and require a somewhat heuristic implementation for the following reasons [START_REF] Vanneschi | Measuring bloat, overfitting and functional complexity in genetic programming[END_REF]. First, the SFC considers each problem dimensions independently by projecting the output of a function onto each dimension and obtaining a complexity measure for each dimension separately. In [START_REF] Vanneschi | Measuring bloat, overfitting and functional complexity in genetic programming[END_REF] the final SFC was the average of all such measures, while in this paper we test the average, median, max and min values. The decision to consider each dimension separately might be problematic since the complexity of a function in a multidimensional space could be different from the complexity of the function as projected onto each individual dimension. Second, by employing such a strategy, the data might become inconsistent. Namely, if we order the data based on a single dimension then the case might arise in which multiple values at the ordinates (program output) correspond with a single value on the abscissa (fitness cases). In such a case a slope measure cannot be computed, and an ad-hoc heuristic is required.

Regularity-based Functional Complexity

Following the basic intuition behind the SFC measure, we propose a similar measure of complexity that focuses on the same functional behavior. Another way to interpret the output we expect from an overfitted function, is to use the concept of H ölderian regularity. In the areas of signal processing and image analysis it is quite clear that the most prominent and informative regions of a signal correspond with those portions where signal variation is highest [START_REF] Trujillo | Optimization of the h ölder image descriptor using a genetic algorithm[END_REF]. It is therefore useful to be able to characterize the amount of variation, or regularity, that is present at each point on signal. One way to accomplish this is to use the concept of H ölderian regularity, which characterizes the singular or irregular signal patterns [START_REF] Tricot | Curves and Fractal Dimension[END_REF]. The regularity of a signal at each point can be quantified using the pointwise H ölder exponent.

Definition 1: Let f : R → R, s ∈ R + * \ N and x 0 ∈ R. f ∈ C s (x 0 ) if and only if ∃η ∈ R + * ,
and a polynomial P n of degree n < s and a constant c such that

∀x ∈ B(x 0 , η), |f (x) -P n (x -x 0 )| ≤ c|x -x 0 | s , (1)
where B(x 0 , η) is the local neighborhood around x 0 with a radius η. The pointwise H ölder exponent of f at

x 0 is α p (x 0 ) = sup s {f ∈ C s (x 0 )}.
In the above definition, P n represents the Taylor series approximation of function f . When a singularity (or irregularity) is present at x 0 then f is nondifferentiable at that point, and P n represents the function itself. In this case, Eq. 1 describes a bound on the amount by which a signal varies, or oscillates, around point x 0 within an arbitrary local neighborhood B(x 0 , η). Hence, when the singularity is large at x 0 , with a large variation of the signal, then α p → 0 as x → x 0 . Conversely, α p → 1 when the variation of the signal (f (x) -P n ) → 0 as x → x 0 , the point is smoother or more regular. Figure 1 shows the envelope that bounds the oscillations of f expressed by the H ölder exponent α p at x 0 .

The basic intuition of SFC is that a complex functional output should exhibit an irregular behavior (high curvature). Conversely, a simple function should produce a smoother, or more regular, output. Therefore, we propose to use the H ölder exponent as the basis for a complexity measure which we call Regularitybased Functional Complexity, or RFC. The idea is to compute the H ölder exponent at each fitness case and use these measures to characterize the overall regularity of the functional output. The final RFC measure could be a variety of statistics computed from the set of H ölder exponents obtained from each fitness case; here, as for SFC, we test the average, median, max and min values. There are several estimators for the H ölder exponent [START_REF] Jaffard | Fractal Geometry and Applications: A Jubilee of Benoit Mandelbrot[END_REF][START_REF] Trujillo | The estimation of h ölderian regularity using genetic programming[END_REF]; however, here we use the oscillations method, which can be derived directly from Definition 1 [START_REF] Tricot | Curves and Fractal Dimension[END_REF].

Estimation of the pointwise H ölder exponent through oscillations

The H ölder exponent of function f (x) at point x 0 is the sup(α p ) ∈ [0, 1], for which a constant c exists such that ∀x ′ in a neighborhood of x 0 ,

|f (x 0 ) -f (x ′ )| ≤ c|x 0 -x ′ | αp . (2)
In terms of signal oscillations, a function f (x) is H ölderian with exponent α p ∈ [0, 1] at x 0 if ∃c ∀τ such that osc τ (t) ≤ cτ αp , with

osc τ (x 0 ) = sup x ′ ,x ′′ ∈[x0-τ,x0+τ ] |f (x ′ ) -f (x ′′ )| . (3)
Now, since x ′ = x 0 + h in Eq. 2, we can also write that

α p (x 0 ) = lim inf h→0 log |f (x 0 + h) -f (x 0 )| log |h| . (4)
Therefore, the problem is that of finding an α p that satisfies 2 and 3, and in order to simplify this process we can set τ = β r . Then, we can write osc τ ≈ cτ α p = β (αpr+b) , which is equivalent to log β (osc τ ) ≈ α p r + b.

Therefore, an estimation of the regularity can be built at each point by computing the slope of the regression between the logarithm of the oscillations osc τ The implicit difficulties of applying SFC are not an issue for RFC, since it is not necessary to consider each problem dimension separately. Moreover, unlike the concept of curvature, estimating signal regularity does not require derivatives in a multidimensional space. Therefore, the RFC provides a straightforward measure of the intuitive functional behavior that SFC attempts to capture.

Experiments

Test problems and experimental setup In order to test both SFC and RFC we use the same two real world problems as [START_REF] Vanneschi | Measuring bloat, overfitting and functional complexity in genetic programming[END_REF]. They consist on predicting the value of two pharmacokinetic parameters for a set of candidate drug compounds based on their molecular structure. The first data set relates to the parameter of human oral bioavailability, and contains 260 samples in a 241 dimensional space. The second data set relates to the median lethal those of a drug, or toxicity, and contains 234 samples from a 626 dimensional space. The experimental setup for our GP is summarized in Table 1. Most parameters are the same as those in [START_REF] Vanneschi | Measuring bloat, overfitting and functional complexity in genetic programming[END_REF], except for the probabilities of each genetic operator. The reason for this is that we want a GP system that does not bloat, however the Operator Equalisation technique used in [START_REF] Vanneschi | Measuring bloat, overfitting and functional complexity in genetic programming[END_REF] was considered to be too computationally costly. Therefore, we combine simple one-point crossover with standard subtree mutation in order to avoid code bloat and still achieve good fitness scores. The choice of a GP without bloat instead of a typical GP was made because we want to confirm that a causal relationship between bloat and overfitting is not a general one.

In Section 3 we presented SFC and RFC, however there is one more important consideration that must be accounted for before computing these scores. Since we are to compute a complexity score for any program tree, it will sometimes be the case that a particular program will use only a fraction of the total dimensions (expressed as terminals) of the problem. Therefore, a decision must be made regarding which dimensions to include when either SFC or RFC are computed. In this case we only use those dimensions that are part of a programs computations. Finally, we point out that all of our code was developed using Matlab 2009a, using the GPLAB toolbox for our GP system [START_REF] Silva | Gplab: A genetic programming toolbox for matlab[END_REF], and the FracLab toolbox to compute the H ölder exponents of the RFC measure [START_REF] Lévy | Thinking in Patterns, chapter Signal and Image Processing with FRACLAB[END_REF].

Results

We begin by presenting the results obtained for training fitness, test fitness, bloat and overfitting for the bioavailability and toxicity problems, shown in figures 2 and 3 respectively. In each case we present the median and average performance over all runs. There are several noticeable patterns in these plots. First, in both cases we can see that our GP systems converges to good fitness scores [START_REF] Vanneschi | Measuring bloat, overfitting and functional complexity in genetic programming[END_REF]. Second, the GP system does not incur bloat, in fact the median values in both problems fall below zero, which means that the average population size actually decreased with respect to the initial population. This is an interesting result, where bloat is eliminated from our runs using a simple strategy. Third, we see that in both problems there is only a small amount of overfitting based on the median scores, with values much lower than those published in [START_REF] Vanneschi | Measuring bloat, overfitting and functional complexity in genetic programming[END_REF]. However, the average overfitting is substantially larger than the median value, this indicates that our runs produced outliers.

The evolution of the complexity measures are presented in figures 4 and 5 for the bioavailability and toxicity problems respectively. Each plot considers a different representative statistics for each measure, as stated in Section 3, and shows the median value of this statistics over all the runs. However, it is not possible to draw a clear conclusion regarding the relationship, or correlation, between complexity and the overfitting curves shown in figures 2(d) and 3(d). Therefore, scatter plots of complexity and overfitting are shown in figures 6 and 7 for the bioavailability and toxicity problems respectively. These plots take the best individual from each generation and each run, and their overfit- ting and complexity scores as ordered pairs. Additionally, each plot shows the Pearson's correlation coefficient ρ between each complexity score and overfitting. For analysis, we follow the empirical estimates of [START_REF] Jones | Fitness distance correlation as a measure of problem difficulty for genetic algorithms[END_REF] and consider values of ρ > 0.15 as an indication of positive correlation, ρ < -0.15 as negative correlation, and -0.15 ≤ ρ ≤ 0.15 as an indication of no correlation. It is important to point out that SFC is expected to have a positive correlation with overfitting while RFC should have a negative one given the definition of each. Most tests show and absence of correlation, with only SFC-max achieving the expected result on toxicity, and RFC-min on bioavailability.

Since the best case scenario would be to have a complexity measure that predicts when a program is overfitted, then it is more informative to discard those individuals with low overfitting, and focus on individuals with a large amount of overfitting. In other words, if a complexity measure cannot be used as an indicator of extreme cases of overfitting, then its usefulness would be quite low. Therefore, in figures 8 and 9 we show the same scatter plots as before, however in this case we only present the 5% of individuals with the highest amount of overfitting. First, consider the results for the SFC measure. In most cases, SFC shows a negative correlation with overfitting on both problems, the exact opposite of what we expected. It is only SFC-min that shows the expected correlation on the toxicity problem. Second, for RFC on the bioavailability problem, only RFC-median and RFC-min show the expected negative correlation. However, given the low overfitting on this problem, we should only expect to detect a small amount of correlation in the best case scenario. On the other hand, for the toxicity problem all RFC variants show the expected correlation. Hence, in this case for the higher overfitting values (the top 5%), the RFC measure could provide an indication of program overfitting.

It appears that the above results are not very strong, given low correlation values achieved even in the best cases. Nonetheless, we would like to stress the difficulty of the problem at hand. In both test cases we have a small sample of data that lies within a highly multidimensional space. Therefore, extracting a proper description of program behavior, and thus functional complexity, is not trivial. For instance, the RFC measures relies on the pointwise H ölder exponent, and in order to estimate it at any point it is necessary to consider how the function oscillates within a series of progressively larger and concentric local neighborhoods. However, in both of our test cases it becomes extremely difficult to correctly estimate the oscillations of the function, and sometimes it cannot be done, because of the sparseness of the data. One possible way to solve this problem is to generate or interpolate the missing data in a way that preserves the regularity of the function [START_REF] Legrand | Local regularity-based interpolation[END_REF], however this is left as future work. In summary, if any measure can produce, even a slight indication of overfitting, this should suggest that we are proceeding in a promising direction.

Summary and concluding remarks

This work presents an empirical study of functional complexity in GP. It is commonly stated that simpler solutions to a problem should be preferred because they are less likely to be overfitted to the training examples. In this work, we study two complexity measures, Slope-based Functional Complexity [START_REF] Vanneschi | Measuring bloat, overfitting and functional complexity in genetic programming[END_REF], and Regularity-based Functional Complexity derived from the concept of H ölderian regularity. We measure the evolution of SFC and RFC on a bloat-free GP system using two real-world problems, in order to evaluate if they can serve as indicators of overfitting during a GP run. Overall, the results show almost no correlation between both complexity measures and program overfitting. However, when we consider only highly overfitted solutions, then the RFC measures does appear to provide a somewhat useful indicator of overfitting. On the other hand, the SFC measure fails to achieve any useful correlation with program overfitting, and in some cases it produces the opposite of what is expected. Nonetheless, it is important to stress that this should be taken as an initial, and partial, empirical study of functional complexity in GP. Therefore, further research should focus on a more comprehensive evaluation of these, and possibly other, measures of complexity as indicators of GP overfitting.

Fig. 1 .

 1 Fig. 1. H ölderian envelope of signal f at point x0.

Fig. 2 .

 2 Fig. 2. Evolution of the bioavailability problem.

Fig. 3 .

 3 Fig. 3. Evolution of the toxicity problem.

Fig. 4 .Fig. 5 .

 45 Fig. 4. Evolution of both complexity measures for the bioavailabitly problem. (a)-(d) correspond to the SFC measure and show the average, median, max and min of the SFC values of all problem dimensions. (a)-(d) correspond to the RFC measure and show the average, median, max and min of all the H ölder exponents computed for each fitness case. All plots show the median value obtained over all 30 runs.

Fig. 6 .Fig. 7 .

 67 Fig. 6. Scatter plots of both complexity measures for the bioavailabitly problem. (a)-(d) correspond to the SFC measure and show the average, median, max and min. (a)-(d) correspond to the RFC measure and show the average, median, max and min. All plots also show Pearson's correlation coefficient ρ.

Fig. 8 .Fig. 9 .

 89 Fig. 8. Scatter plots of both complexity measures for the bioavailabitly problem with the 5% of individuals that have the highest overfitting scores. (a)-(d) SFC measure, showing the average, median, max and min. (a)-(d) RFC measure, showing the average, median, max and min. All plots also show Pearson's correlation coefficient ρ.

Table 1 .

 1 GP parameters used for real world experiments. of the dimension of the neighborhood at which the oscillations τ are computed. Here, we use least squares regression to compute the slope, with β = 2.1 and r = 0.1, 0.2, . . . , 9. Also, it is preferable not to use all sizes of neighborhoods between two values τ min and τ max . Hence, we calculate the oscillation at point x 0 only on intervals of the form [x 0τ r : x 0 + τ r ]. For a function in R D , τ r is defines a hyper-volume around x 0 , such that d(x ′ , x 0 ) ≤ τ r and d(x ′′ , x 0 ) ≤ τ r , where d(a, b) is the Euclidean distance between a and b.

	Parameter	Description
	Population size	500 individuals
	Iterations	100 generations
	Initialization	Ramped Half-and-Half
	Crossover probability	pc = 0.5
	Mutation probability	pµ = 0.5
	Initial max. depth	Six levels
	Selection	Lexicographic Parsimony Tournament
	Survival	Elitism
	Runs	30
	and the logarithm

Acknowledgements

This work was partially supported by FCT (INESC-ID multiannual funding) through the PIDDAC Program funds. Sara Silva and Leonardo Vanneschi acknowledge project PTDC/EIA-CCO/103363/2008 from FCT, Portugal.


Frédéric Besson
email: frederic.besson@inria.fr

Pascal Fontaine
email: pascal.fontaine@loria.fr

Laurent Théry
email: laurent.thery@inria.fr

A Flexible Proof Format for SMT: a Proposal *

The standard input format for Satisfiability Modulo Theories (SMT) solvers has now reached its second version and integrates many of the features useful for users to interact with their favourite SMT solver. However, although many SMT solvers do output proofs, no standardised proof format exists. We, here, propose for discussion at the PxTP Workshop a generic proof format in the SMT-LIB philosophy that is flexible enough to be easily recast for any SMT solver. The format is configurable so that the proof can be provided by the solver at the desired level of detail.

Introduction

Satisfiability Modulo Theory (SMT) consists in deciding the satisfiability of formulae belonging to a combination of theories. Over the past few years, the quality of SMT-provers has greatly improved. This is evaluated at the SMT-COMP, the annual competition for SMT. Current SMT-provers are highly optimised and engineered tools that are capable of deciding formulae of industrial size. For the moment, the output of most SMT-provers is just the simple answer: sat or unsat. This information is enough to evaluate their speed and relative soundness -especially when the status of formulae is known beforehand. But this may not be sufficient, and particularly when trusting the SMT solver is not an option, like in a skeptical cooperation of solvers.

The purpose of the current proposal is to tackle this problem and propose a generic proof format for SMT-provers. Compared to existing approaches our objective is to aim at a format that is sufficiently generic so that:

-any SMT-solver could generate a proof without too much effort; -the proof could be checked by a trustworthy external verifier.

Our assessment is that previous attempts have produced formats that are either easy to generate but hard to check or hard to generate and easy to check. For instance, the SMT-solver clsat generates proofs that are already genuine proofs objects of the logical framework LF [START_REF] Stump | Faster Proof Checking in the Edinburgh Logical Framework[END_REF]. This approach is very challenging and intellectually attractive. Yet efficient generation and checking of LF proofs is still an open research area. Unlike [START_REF] Stump | Faster Proof Checking in the Edinburgh Logical Framework[END_REF], we advocate for a clear distinction between the proof generated by the SMT-solver and the proof-object that would be built by the checker. As a pay-off our proof format should be easier to produce and not require a substantial re-engineering of the SMT-solver. There are other proof-generating SMTprovers such as CVC3 [START_REF] Barrett | CVC3[END_REF], veriT [START_REF] Bouton | veriT: an open, trustable and efficient SMTsolver[END_REF] and Z3 [START_REF] De Moura | Z3: An Efficient SMT Solver[END_REF][START_REF] De Moura | Proofs and Refutations, and Z3[END_REF]. For those, the proof format is not totally formalised and proof reconstruction in a skeptical proof assistant is not a trivial task [START_REF] Mclaughlin | Cooperating theorem provers: A case study combining HOL-Light and CVC Lite[END_REF][START_REF] Böhme | Fast LCF-style proof reconstruction for Z3. In ITP[END_REF]. One difficulty lies in the fact that certain proof steps of the SMT-provers are kept implicit and do not appear in the proof trace. We aim at providing a proof format that is proof-assistant friendly.

Proof of satisfiability/unsatisfiability

When a formula is satisfiable, a checkable account of the satisfiability is a detailed model of the formula, such that every term, atom, literal, and sub-formula has a precise value. Giving this detailed model may be problematic when handling formulae with quantifiers. When the formula is unsatisfiable, SMTsolvers derive an inconsistency from the original formula. A proof of unsatisfiability is thus a checkable derivation from the original formula to an object which is trivially inconsistent. The context of such a proof is the set of all deduced facts. Initially, the context contains the original formula. Logical rules are applied to derive new formulae from formulae in the context. These new formulae are then added to the context. At the end of the proof, the empty clause (noted ()) should belong to the final context.

Our proof format aims at providing a clear interface between SMT-solvers that generate proofs and checkers that verify the correctness of the generated proofs. We voluntarily restrict ourselves to a specific and limited fragment of the logics current SMT-solvers can deal with. This will let us experiment rapidly and get feedback on how the format should evolve and be improved. As a result, we are considering quantifier-free formulae with uninterpreted functions, equality and linear arithmetic only. In particular, we do not take quantifiers into account. This means that tasks such as skolemization and instantiation are not covered yet.

The work of the solver is usually composed of several phases that the proof format has to address:

-First, the formula may be rewritten: the formula is transformed to a somewhat simpler and equivalent one. This is done by identifying sub-formulae and sub-terms that clearly can be rewritten to simpler equivalent forms. Provers implement this by some rewriting rules, and those rewriting rules should have their derivation counterparts.

-SMT-solvers, being based on the SAT-solvers technology, also require conjunctive normal forms (CNF). The transformation phase, that translates the original formula to a set of clauses also requires a proof. Each clause of the CNF becomes a new fact added to the context. From those clauses, new clauses can be derived using resolution. Resolution is a complete method for the satisfiability of propositional formulae.

-Reasoning about theories can be understood as adding conflict clauses to the SAT-solver. These conflict clauses are tautologies according to the theories in action. To each theory will correspond a set of rules that will add clauses in the context. Equality exchange between different parts of the reasoner can simply be seen as resolution.

Rationale for the proof format

The SMT-LIB 2.0 format [START_REF] Barret | The SMT-LIB standard: Version 2.0[END_REF] is the de facto input standard of the SMT community. It provides a set of commands for interacting with solvers. While designing our proof format, we have been careful at being fully compatible with the SMT-LIB format. Other existing formats like TSTP [START_REF] Sutcliffe | TSTP Data-Exchange Formats for Automated Theorem Proving Tools[END_REF] could have been valid candidates to represent SMT proofs but we wanted to have a format whose syntax was a direct extension of SMT-LIB syntax. For this reason, we inherit the syntax of terms and formulae but also certain wellformedness conditions from the SMT-LIB. This does not prevent the possibility of developing a translator to other formats like TSTP in the future. The core of the proof format specifies the syntax and semantics for the existing SMT-LIB command get-proof -currently left unspecified. To our opinion, a fixed proof format is not viable because of the variety of existing SMT-provers. Our proposal is a proof format that is built upon a generic kernel enriched by prover-specific proof rules that can be obtained by a dedicated get-proof-header command (see Section 2.2).

Overall, the proof format is a trade-off between the requirements from proof consumers, who want a non-ambiguous syntax and semantics, and developers of SMT-solvers, who favour freedom in outputting proofs in a structure that their solvers can generate without sacrificing efficiency. In Section 2.5, we list a set of recommendations for getting a maximal benefit from the proof format.

The rest of the paper is organised as follows. Section 2 explains the syntax of the proof format. The format is illustrated by an example discussed in details in Section 3. Section 4 provides an operational semantics of the format by providing a reference implementation for a proof-checker.

Syntax

Data structures

This document inherits the syntax for terms (and thus formulae) from the SMT-LIB 2.0 standard [START_REF] Barret | The SMT-LIB standard: Version 2.0[END_REF]. Furthermore, clauses are used in several places. A clause is a list of formulae. For instance: ((= x y) (= (f x) (f y)))) represents a clause which is a disjunction of the formula x = y and the formula f (x) = f (y). The empty clause is the empty list (). For convenience, one can use the trivially valid clause (true).

Proof header

The format is generic and therefore has to be instantiated with solver-specific proof rules. To ease proof-reconstruction by third-party tools, proof rules are declared belonging to a certain SMT-LIB logic, with an attached informal description. The header may be output on request by the SMT solver with a supplementary command get-proof-header, an addition to SMT-LIB 2.0. An example of such a header is given in Figure 2. Here is its syntax: where attribute is defined as in SMT-LIB 2.0. Note that attribute values can be sexpr so they could possibly contain code (for instance for proof checkers). All keywords used as attributes in rule def should be defined; there is currently no predefined keyword. Keywords are used to identify collection of rules. For example, they could be used to qualify rules that are handling quantifiers, skolemizations, or specific operations on connectors (e.g., conjunctions). A rule using logic should be such that SMT solvers implementing only the SMT-LIB 2.0 logic must be able to verify every clause deduced by this rule.

Proof script

An example proof script is presented in Figure 3. A proof script is a pair made of a proof context and a sequence of proof steps proof ::= context proof step *

where the context is an SMT-LIB 2.0 script using only commands set-logic, declare-sort, define-sort, declare-fun, define-fun, assert. The context is generally just a subset of the SMT-LIB 2.0 input script. Furthermore, in asserts, in order to identify formulae, we require them to be explicitly named using the following SMT-LIB 2.0 notation:

(assert (! term :named clause id ))
where term is the formula asserted, written in the SMT-LIB 2.0 syntax, and clause id is an SMT-LIB 2.0 symbol . A proof step is defined by the following rule: where -(define term id term ) declares term id as a short-name for the term term .

-(set clause id gen clause ) constructs a new clause named clause id using the clause generation rule gen clause (see below). The identifier clause id is an SMT-LIB 2.0 symbol and is used to refer to the clause in the current environment -(seth clause id clause ) is used to assert the hypotheses of a sub-proof. Again, clause id is an SMT-LIB 2.0 symbol .

Note that this version of the proof format does not cover quantifiers yet. So term is just a ground term.

Derived clauses

A clause can either be explicit or derived. Here we describe how it is derived: There exist three ways to derive a clause:

-clause id is used to retrieve a clause formerly assigned a clause id in the current environment (where clause id is an SMT-LIB 2.0 symbol ).

-A clause can be derived using a (named) rule: as arguments an optional list of terms, and an optional result can be provided. When :clauses is used, the conclusion is a logical consequence of the given set of clauses. When :all-clauses is used, the conclusion is a logical consequence of an unspecified set of local hypotheses. When neither the tag :clauses nor :all-clauses is used, the rule introduces a tautology.

-A local proof can be declared. For simplicity, only local proofs from an empty context are supported; references to the current context in a local proof is not allowed. The clause attached to a local proof is composed of all the literals in all clauses introduced by the seth in the proof steps (these literals are negated) and the literals in the clause given after the :conclusion attribute. When this attribute is omitted, it is the clause attached to the last step that is considered as conclusion.

Recommendations

Figure 1 presents the whole grammar of the format. The format is very flexible and tries to avoid unnecessary constraints. Nevertheless, some obvious recommendations can already be made in order to allow effective validation by third-party tools:

-rules should be carefully described in the header;

-term sharing should be maximised in order to improve memory management; -all the hypotheses in local proofs should be specified first.

These are recommendations and not requirements since external tools could always refactor proofs in order to meet these recommendations.

An example

In Figure 3, we present a proof in our format of the following formula

¬((a = c) ∧ (b = c) ∧ (( f (a) = f (b)) ∨ (p(a) ∧ ¬(p(b)))))
For readability, the proof does not use the facility of the format for sharing terms. It starts with the context which is just a subset of the SMT-LIB 2.0 input script. Every following command introduces a new clause (with the set command) until the final clause, the empty clause (). The proof relies on elementary rules. The description of these rules can be obtained using the command (get-proof-header) which could return (among other rule definitions) the definitions in Figure 2. In those definitions, the :clauses, :terms and :conclusion attributes respectively give the expected number of clauses (-1 if arbitrary), terms, and conclusion (0 if no conclusion is provided, that is, if the checker is expected to recompute the conclusion).

The and rule is used to deduce new clauses from conjunctive unit clauses: every conjunct of a conjunctive unit clause can indeed be itself introduced as a unit clause, as are clauses c2, c3 and c4 in the example in Figure 3. The and pos rule generates a tautology of the form ¬ ∧ i a i ∨ a j for some j (see clauses c5 and c6). The or rule introduces a clause from a disjunctive unit clause, by simply building the clause of the disjuncts (e.g. clause c7). Clauses c2 to c7 constitute the CNF of the input formula. Notice that the CNF transformation is not a naive transformation, but it does not explicitly introduce new (Tseitin) Boolean variables. Indeed, as a side effect of the fact that clauses are sets of formulae (and not just literals), it is easy to introduce definitional CNF transformations without introducing new Boolean variables: the formulae themselves stand for those Boolean variables. Using sharing, the CNF would be linear with respect to the size of the initial formula.

Rules eq_congruent, eq_congruent_pred, and eq_transitive introduce equational tautologies (for instance c8, c9, c15 and c16). The resolution rule implements chain resolution. Note that this rule serves several purposes here. It is used for instance for resolution executed within the SAT-solver (e.g. to deduce c18), and it is used to build conflict clauses from generic tautologies (e.g. to build c10).

The subproof construct (see Figure 1) can always be inlined -maybe at the cost of adding more proof-rules. It does not change the expressive power of the proof-format but allows for more structured proofs. The subproof construct can also be used to minimise the number of proof rules. For instance, in the proof-script of Figure 3, the clause c5 can alternatively be obtained by the following sub-proof. Note that the conclusion of a sub-proof (if omitted) can exactly be reconstructed as soon as the proof rule for the last derived clause in the sub-proof has an explicit conclusion. Here, the obtained clause is therefore ((not (and (p a) (not (p b)))) (p a)).

Proof checking

In this section, we provide a reference implementation for a proof verifier for the generic proof format. The proof verifier is parametrised by prover-specific proof rules declared in the proof header. As a result, the validity of the proof verifier relies on the fact that proof rules are logically sound i.e., only derive clauses that are logic consequences of the current known clauses. The proof verifier takes as input a proof π ∈ context × proof step * (see Section 2.3). and verifies that the proof steps indeed derive the empty clause i.e., the conjunctions of the formulae asserted by the context part of the proof is unsatisfiable. The state of the verifier is made of a quadruple (Sig, N, S, cl) where -Sig is a SMT-LIB signature built from the commands declare-sort and declare-fun of the proof context. Its purpose is to ensure that terms are well-sorted. -S is a stack of named assertions tagged with a boolean flag. The assert commands of the context construct an initial singleton stack where all the asserted formulae are tagged true. During the proof, derived clauses introduced by the set command are also tagged by true. The tag false is reserved to clauses introduced by the seth command. Those clauses are local hypotheses to be discharged by sub-proofs. cl is the last derived clause. It is initialised to true ( true ) and for a valid proof is eventually set to the empty clause () .

The proof checking succeeds if the empty clause is eventually generated in a singleton stack for which all the formulae are tagged true.

The proof-verifier is executed in a state constructed by running the context commands. After running the context commands the proof state is such that:

-The signature Sig contains sort and function declarations (Sig is thereafter immutable) -N contains constant and function declarations (during the proof checking, only new constants can be defined) -S is a singleton stack of the form {n 1 → cl tt 1 , . . . , n i → cl tt i } where a binding (n i , cl i ) is the result of the assert command (assert (! f i :named n i )). cl i being then the clause containing the sole formula f i .

Conventions and auxiliary functions

The verifier makes use of auxiliary functions and predicates. Several of them are already part of the SMT-LIB 2.0 where they are used to give a semantics to SMT-LIB scripts. The pseudo-code does not introduce an explicit abstract syntax for the proof constructs. Instead we use directly the concrete syntax with the conventions that optional attributes are given a default value. More precisely, missing attributes of type list (for instance :clauses, :terms, :attributes) are given as default value the empty list and a missing attribute of type clause (for instance :conclusion) is given as default value the symbol null.

Well-formedness

As in the SMT-LIB we only consider well-formed terms.

Definition 1 (Well-formed terms). A term t is well-formed with respect to a signature Sig and an environment of names N (isWellFormed(Sig, N,t)) if -all the symbols in the term are bound in N; -the term is well-sorted according to the signature Sig.

To ensure that a well-formed term will never be invalidated, the signature Sig and the environment N can only be augmented by additional declarations. It is therefore forbidden to overwrite a declaration. In case of violation, the verification is aborted.

Assertion stack

Proof scripts feature a notion of subproof to describe scoped proofs. As already stated, this construct does not increase the expressive power of the format. Its purpose is to structure proofs and thus facilitate their checking. For instance, each theory reasoner of the SMT solver can generate a sub-proof for each theory lemma or conflict clause. The advantage of sub-proof is that such theory lemma can be checked in isolation. To implement scoped proofs, the assertion stack is updated by push and pop operations

Prover-specific proof rules

The verifier is parametrised by prover-specific proof rules that are trusted and could therefore be responsible for an invalid proof. Each proof rule is implemented by a function named according to the rule id taking as arguments an optional list of clauses, terms and attributes and either returning a clause or reporting an error. An error immediately aborts the verification of the proof. The soundness requirement is that the generated clause must be a logic consequence of the clauses passed as arguments. A proof rule also takes as arguments the signature Sig and the environment of bindings N.

Pseudo-code of the verifier

The verifier is written in an imperative style and therefore updates in-place the proof state (Sig, N, S, cl). The verifier is presented top-down and consists of 4 functions:

-checker is the top-level function and evaluates a whole proof. Upon success, it concludes that the input problem is not satisfiable.

-eval proof evaluates all the proof steps in turn and updates the proof state accordingly;

-eval proof step performs a case analysis over the proof command;

-eval gen clause is responsible for deriving from the proof state new logic consequences by combining prover-specific proof rules.

A proof is valid if after executing the proof steps the clause cl is the empty clause () and there are no introduced local hypotheses (all clauses are tagged tt).

Acknowledgements

The work presented here has been funded by the French ANR Decert initiative. This format is the result of many stimulating conversations with its members. We want to thank Aaron Stump for his remarks on a previous version of this document, and for numerous informal discussions. We also thank the anonymous reviewers for their insightful comments.

Conclusion and further work

The proof format presented in this paper is an extension of the SMT-LIB 2.0 format. We have tried as much as possible to find a good compromise between what can be output by an SMT-solver and what is needed in order for a simple checker to be able to verify a proof. We are aware that this format is not perfect and some subtle issues still need to be further investigated and discussed. Nevertheless we hope that the format can serve as a common basis that can be used by the SMT community.

The format is currently being implemented in the veriT solver distributed as open-source using the BSD licence. We are also currently investigating proofs for quantifier reasoning [START_REF] Déharbe | Quantifier inference rules for SMT proofs[END_REF]; Skolemization, as a satisfiability preserving transformation which does not preserve logical equivalence, may raise difficult

  rule tag def ::= (define-rule-kw keyword string ) rule def ::= ( rule id logic attribute * ) header ::= rule tag def * rule def *

  proof step ::= (define term id term ) | (set clause id gen clause ) | (seth clause id clause )

  gen clause ::= clause id | ( rule id (:clauses ( gen clause * ) | :all-clauses)? (:terms ( term * ))? attribute * (:conclusion clause )?) | (subproof proofstep * (:conclusion clause )? )

Figure 1 :

 1 Figure 1: The complete proof format

(

  set c5 (subproof (seth h (and (p a) (not (p b))) ) (set res (and :clauses (h) :conclusion (p a)))))

;Figure 2 :

 2 Figure 2: The proof header

  logic QF_UF) (declare-sort U 0) (declare-fun p (Bool) U) (declare-fun f (U) U) (declare-fun a () U) (declare-fun b () U) (declare-fun c () U) (assert (! (and (= a c) (= b c) (or (not (= (f a) (f b))) (and (p a) (not (p b))))) :named c1)) ; Proof (set c2 (and :clauses (c1) :conclusion ((= a c)))) (set c3 (and :clauses (c1) :conclusion ((= b c)))) (set c4 (and :clauses (c1) :conclusion ((or (not (= (f a) (f b))) (and (p a) (not (p b))))))) (set c5 (and_pos :conclusion ((not (and (p a) (not (p b)))) (p a)))) (set c6 (and_pos :conclusion ((not (and (p a) (not (p b)))) (not (p b))))) (set c7 (or :clauses (c4) :conclusion ((not (= (f a) (f b))) (and (p a) (not (p b))))) (set c8 (eq_congruent :conclusion ((not (= b a)) (= (f a) (f b)))) (set c9 (eq_transitive :conclusion ((not (= b c)) (not (= a c)) (= b a))) (set c10 (resolution :clauses (c8 c9) :conclusion ((= (f a) (f b)) (not (= b c)) (not (= a c))))) (set c11 (resolution :clauses (c10 c2 c3) :conclusion ((= (f a) (f b))))) (set c12 (resolution :clauses (c7 c11) :conclusion ((and (p a) (not (p b)))))) (set c13 (resolution :clauses (c5 c12) :conclusion ((p a)))) (set c14 (resolution :clauses (c6 c12) :conclusion ((not (p b))))) (set c15 (eq_congruent_pred :conclusion ((not (= b a)) (p b) (not (p a))))) (set c16 (eq_transitive :conclusion ((not (= b c)) (not (= a c)) (= b a)))) (set c17 (resolution :clauses (c15 c16) :conclusion ((p b) (not (p a)) (not (= b c)) (not (= a c))))) (set c18 (resolution :clauses (c17 c2 c3 c13 c14) :conclusion ())

Figure 3 :

 3 Figure 3: A simple example with its proof.

2 .

 2 Given a tagged clause cl b , clause(cl b ) returns the clause cl and tag(cl b ) returns the boolean b. The verifier always accesses and updates the topmost assertion set. We write top[s] for the clause bound to the symbol s in the topmost assertion set. Accessing a non-existent symbol aborts the verification. Overwriting a clause tagged with ff also aborts the verification i.e., an assignment of the form top[s] := cl b where tag(top[s]) = ff aborts the verification.

  rule id : Sig × N × clause * × term * × attributes * → clause | error

  b o o l c h e c k e r ( Π ) { e v a l p r o o f ( Π ) ; r e t u r n ( c l = ( ) ) & ( ∀ i , t a g ( t o p [ i ] ) = tt ) ; } The function eval proof executes in turn the proof steps. v o i d e v a l p r o o f ( Π ) { f o r -e a c h ( π ∈ Π ) e v a l p r o o f s t e p ( π ) ; } The function eval proof step performs a case analysis and updates the last derived clause. v o i d e v a l p r o o f s t e p ( π ) { s w i t c h ( π ) { c a s e ( define t i d t r m ) : r e q u i r e s ( i s W e l l F o r m e d ( t r m ) ) ; N[ t i d ] : = t r m c a s e ( set c i d g e n c l ) : c l : = e v a l g e n c l a u s e ( g e n c l ) ; t o p [ c i d ] : = c l tt ; c a s e ( seth c i d hyp ) : r e q u i r e s ( i s W e l l F o r m e d ( hyp ) & h a s S o r t B o o l ( hyp ) ) ; t o p [ c i d ] : = hyp ff ; } F. Besson, P. Fontaine and L. Théry The core of the verifier is the function eval gen clause which generates a novel clause logic consequence of the current proof state. c l a u s e e v a l g e n c l a u s e ( g e n c l ) { s w i t c h ( c l g e n ) { c a s e c l i d : r e t u r n c l a u s e ( t o p [ c l i d ] ) c a s e ( r i d :clauses ( gc1 , . . . , g c i ) :terms ( t 1 , . . . , t k ) :attributes ( a1 , . . . , an ) :conclusion c o n c l ) : / * R e c u r s i v e l y g e n e r a t e c l a u s e s * / g c s : = ( e v a l g e n c l a u s e ( gc1 ) , . . . , e v a l g e n c l a u s e ( g c i ) ) ; / * C a l l t h e p r o v e r s p e c i f p r o o f r u l e * / c l : = r i ( Sig , N, gcs , ( t 1 , . . . , t k ) , ( a1 , . . . , an ) , c o n c l ) ; / * Check t h e c o n c l u s i o n i f any * / i f c o n c l ! = n u l l & c o n c l ! = c l t h e n a b o r t r e t u r n c l ; c a s e ( subproof p r f :conclusion c o n c l ) p u s h ( ) ; / * L o c a l a s s e r t i o n s e t * / e v a l p r o o f ( p r f ) ; i f c o n c l ! = n u l l & c l ! = c o n c l t h e n a b o r t / * G e n e r a t i o n o f t h e c o n f l i c t -c l a u s e * / c o n f l i c t : = ( n o t ( h1 ) , . . . . , n o t ( hn ) , c l ) ; where {h1 , . . . , hn } = { c l a u s e ( t o p [ i ] ) | t a g ( t o p [ i ] ) = ff } pop ( ) ; r e t u r n c o n f l i c t ; }

For more flexibility, this restriction might be lifted in the future.

They correspond to the functions push 1 and pop 1 of the SMT-LIB

F. Besson, P. Fontaine and L. Théry issues. The CNF transformation presented here does not require Tseitin variables; if such variables are required by other solvers, then similar issues may also appear for CNF transformation.

In Section 4, we presented the code of a proof checker. A standalone checker for the format is one of our long term goals. However, in addition to the infrastructure presented in Section 4, this requires to implement the term data-structure, and the operators to manipulate terms. This comes to reimplementing (parts of) a kernel like those found in mainstream proof assistants. We are currently implementing a module to replay proofs in the present format within Coq, and we plan to study replaying this proof format within LFSC.

This work was funded by the ANR Decert project.