Created in 2008, the Inria center at the University of Lille employs 360 people, including 305 scientists in 16 research teams. Recognized for its strong involvement in the socio-economic development of the Hauts-De-France region, the Inria center at the University of Lille maintains a close relationship with large companies and SMEs. By fostering synergies between researchers and industry, Inria contributes to the transfer of skills and expertise in the field of digital technologies, and provides access to the best of European and international research for the benefit of innovation and businesses, particularly in the region.

For over 10 years, the Inria center at the University of Lille has been at the heart of Lille's university and scientific ecosystem, as well as at the heart of Frenchtech, with a technology showroom based on avenue de Bretagne in Lille, on the EuraTechnologies site of economic excellence dedicated to information and communication technologies (ICT).

Benchmarks for Language Models

Hosting team: Inria Lille, CRIStAL (UMR 9189) Supervisor: Damien Sileo Duration: 36 months Project: TACTICS (PEPR)

Context

Language models have become surprisingly capable reasoners, but progress is bottlenecked by data. Both training (SFT, RLVR) and evaluation rely on problem sets with known answers, and the supply of high-quality, uncontaminated, difficulty-calibrated reasoning problems is running thin. Hand-curated benchmarks saturate quickly, leak into pretraining corpora, and cannot be regenerated at will. Web-scraped reasoning data carries licensing baggage and offers no correctness guarantees.

Procedural generation offers a way out. By coupling a problem generator with a symbolic solver, one can produce an effectively unbounded stream of fresh instances, each shipped with a certified solution and a tunable difficulty knob. The same pipeline serves three purposes at once: pretraining and SFT data with reasoning traces, verifiable rewards for RL, and contamination-free evaluation suites. Our group has been building this line of work through the Reasoning Core library, which already covers PDDL planning over randomized domains, full first-order logic, CFG parsing, causal inference over Bayesian networks, and equation solving.

Thesis topic

The PhD will extend this infrastructure toward harder formalisms and richer reasoning regimes. The core technical question is how to turn a solver plus a formalism into a good procedural generator: one whose output distribution is broad rather than templated, whose difficulty scales smoothly, and whose problems remain well-posed and human-readable as complexity grows.

Several directions are open and will be shaped with the candidate:

• Advanced logics and planning. Hierarchical planning (HTN/HDDL), multi-agent and epistemic planning, temporal logics, and modal logics for reasoning about knowledge and belief. Each formalism has mature solvers but no scalable generator that exposes their full expressive range.
• From solver to generator. Most solvers are built to consume problems, not produce them. Sampling instances that are non-trivial, non-degenerate, solvable within a budget, and distributionally diverse is a research problem in itself, and it gets harder as the formalism grows.
• Verbalization and alignment with human priors. A formal instance is only useful if its natural-language rendering is faithful, varied, and not artificially easy or hard. This involves grammar-based verbalization, controlling surface form independently of logical content, and understanding how phrasing interacts with model inductive biases.
• Pushing scalability where solvers struggle. At high difficulty, exact solvers time out. The thesis will explore approximate verification, compositional generation, and incremental construction strategies that preserve correctness guarantees while extending the reachable difficulty range.

Practical

• Location: Inria Lille, France
• Funding: full PhD scholarship (PEPR TACTICS), plus compute budget for frontier model inference
• Start date: flexible, ideally October 2026

The work will contribute directly to the Reasoning Core https://github.com/sileod/reasoning-core ecosystem and benefit from its existing infrastructure (gramforge grammar framework, containerized solvers, parallel generation pipeline). Evaluation will run on two fronts: zero-shot probing of frontier models to measure where current systems break, and supervised fine-tuning of small models to measure whether the generated data actually instills reasoning capabilities. Both regimes inform what makes a generator useful, and they often disagree in instructive ways.

Study related work

Propose new approaches

Evaluate them, iterate

Write papers

Languages :

• Good written English; French not required
• Solid Python; comfort with formal methods, logic, or symbolic AI is a strong plus

Good relational skills 

• Subsidized meals
• Partial reimbursement of public transport costs
• Leave: 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours) + possibility of exceptional leave (sick children, moving home, etc.)
• Possibility of teleworking and flexible organization of working hours
• Professional equipment available (videoconferencing, loan of computer equipment, etc.)
• Social, cultural and sports events and activities
• Access to vocational training
• Social security coverage

2 300 € Monthly Gross Salary