Files
FELTUS_79982400_POUCET_77472000_2026.pdf
Open access - Adobe PDF
- 5.11 MB
Details
- Supervisors
- Faculty
- Degree label
- Abstract
- Constraint programming (CP) decides in fields of high impact. Consequently, European regulation now gives a person the right to understand a decision that affects them. Fortunately, a CP solver can already justify itself, for example, with minimal unsatisfiable subsets and step-wise deductions. Those justifications are exact. But they are written in the formal language of the solver, so a non-expert cannot read them. A large language model can rewrite those justifications in plain words. However, it can also invent them. Indeed, an explanation can be plausible and still be unfaithful to the reasoning actually performed. Our thesis couples the two. We build an AI agent that reaches the IDP-Z3 solver through the Model Context Protocol. The solver certifies every fact. The language model only puts it into words, at one of ten levels of expertise, from a six-year-old child to a formal proof. Therefore, it never computes the logic of the problem. We evaluate the system along five axes: the construction of the search tree, the separation of the ten explanation levels, the contribution of the certified context, the component that picks the level on its own, and a human evaluation with two questionnaires. Results show that, in 162 solving runs, no run ever ended on a wrong model: when the agent fails, it stops early, it does not invent. When we hide the certified context, on the other hand, the model fills the gap with facts it was never given. Readers with no expertise still understand the explanations produced. Overall, the guarantee therefore comes from the architecture, not from the language model.