ERC FUNDED PROJECTS

The goal of the AI4REASON project is a breakthrough in what is considered a very hard problem in AI and automation of reasoning, namely the problem of automatically proving theorems in large and complex theories. Such complex formal theories arise in projects aimed at verification of today's advanced mathematics such as the Formal Proof of the Kepler Conjecture (Flyspeck), verification of software and hardware designs such as the seL4 operating system kernel, and verification of other advanced systems and technologies on which today's information society critically depends. It seems extremely complex and unlikely to design an explicitly programmed solution to the problem. However, we have recently demonstrated that the performance of existing approaches can be multiplied by data-driven AI methods that learn reasoning guidance from large proof corpora. The breakthrough will be achieved by developing such novel AI methods. First, we will devise suitable Automated Reasoning and Machine Learning methods that learn reasoning knowledge and steer the reasoning processes at various levels of granularity. Second, we will combine them into autonomous self-improving AI systems that interleave deduction and learning in positive feedback loops. Third, we will develop approaches that aggregate reasoning knowledge across many formal, semi-formal and informal corpora and deploy the methods as strong automation services for the formal proof community. The expected outcome is our ability to prove automatically at least 50% more theorems in high-assurance projects such as Flyspeck and seL4, bringing a major breakthrough in formal reasoning and verification. As an AI effort, the project offers a unique path to large-scale semantic AI. The formal corpora concentrate centuries of deep human thinking in a computer-understandable form on which deductive and inductive AI can be combined and co-evolved, providing new insights into how humans do mathematics and science.

1 499 500 €

Start date: 2015-09-01, End date: 2020-10-31

This proposal outlines an agenda that aims to improve our understanding of economies with inattentive agents. Attention to detail, not only to current news, but also to how the world works in general, is central to how we interact with the environment. In the first part of the agenda, we will study how agents come up with the simplified mental models they use in their decision-making. The aim is to provide a new alternative to rational expectations. We will address the question of endogenous model uncertainty by sidestepping the largely statistical nature of previous work. Our agents learn about a model directly, i.e., all information on the details of the correct model is readily available. The envisioned implications can speak to issues such as the expectations formation and formation of narratives, polarization of opinions, and demand for public policy. In the second part, we will study how a government optimally intervenes in markets if it finds it costly to get the necessary information. On one hand, a government does not possess the local information of decentralized markets. On the other, markets on their own often generate suboptimal social outcomes. We will explore what information the government should collect, how to use it for regulation, and when instead it should leave markets unaffected. In the third part, we will leverage recent theories of attention allocation and use uniquely detailed data on attention and treatment choices by hospital personnel (including physicians and nurses). This will allow us to explore in more detail than before what theories describe realistic choices well. Moreover, we will eventually aim at a very practical goal: how to help clinicians decrease their cognitive load and improve medical choices.

1 162 664 €

Start date: 2021-04-01, End date: 2026-03-31

This project proposes a collaborative, ethnographic investigation of the relationship between three understudied subjects in anthropology: veterinary medicine, European hunting and wild boars. In recent decades, the wild boar has proliferated, (re)conquering the natural, rural and urban landscapes of Europe, and increasingly clashing with human practices and worlds. Classified as a game animal, the boar is primarily killed and managed by recreational hunters. Yet, hunters are proving incapable of stemming the tide of this intelligent, adaptable being, an interspecies relation that challenges hunting’s value and legitimacy in European society. This tension has amplified with the arrival of African Swine Fever (ASF) to the continent: a fatal virus that travels between wild boar and domestic pig, forest and farm, and threatens to infect and ruin the pig industry. In the name of biosecurity, and informed by veterinary knowledge, some States have intervened and conducted mass culls, erected dividing fences across Schengen space, or instituted no-go zones. During this crisis we witnessed how veterinary medicine’s role can extend beyond mediating human-animal relations, and work to structure and govern human lives in general. At the intersection of boars, hunting, ASF and veterinary medicine, this project has two main objectives: first, to examine how European hunting and porcine futures are intertwined, and the role of veterinarians in shaping these futures, and; second, through human-boar relations, study how society is becoming increasingly veterinarized and thus shape the conceptual and methodological development of the emerging field of veterinary anthropology. This project will further contribute to anthropology by opening a novel empirical and theoretical niche for the anthropology of hunting, and experiment with ethnography as a tool of engagement with near futures. The emerging and uncertain impact of ASF in Europe is an excellent moment to conduct such a project.

1 999 875 €

Start date: 2020-07-01, End date: 2025-06-30

Viral infection or retrotransposon expansion in the genome often result in production of double-stranded RNA (dsRNA). dsRNA can be intercepted by RNase III Dicer acting in the RNA interference (RNAi) pathway, an ancient eukaryotic defense mechanism. Notably, endogenous mammalian RNAi appears dormant while its common and unique physiological roles remain poorly understood. A factor underlying mammalian RNAi dormancy is inefficient processing of dsRNA by the full-length Dicer. Yet, a simple truncation of Dicer leads to hyperactive RNAi, which is naturally present in mouse oocytes. The D-FENS project will use genetic animal models to define common, cell-specific and species-specific roles of mammalian RNAi. D-FENS has three complementary and synergizing objectives: (1) Explore consequences of hyperactive RNAi in vivo. A mouse expressing a truncated Dicer will reveal at the organismal level any negative effect of hyperactive RNAi, the relationship between RNAi and mammalian immune system, and potential of RNAi to suppress viral infections in mammals. (2) Define common and species-specific features of RNAi in the oocyte. Functional and bioinformatics analyses in mouse, bovine, and hamster oocytes will define rules and exceptions concerning endogenous RNAi roles, including RNAi contribution to maternal mRNA degradation and co-existence with the miRNA pathway. (3) Uncover relationship between RNAi and piRNA pathways in suppression of retrotransposons. We hypothesize that hyperactive RNAi in mouse oocytes functionally complements the piRNA pathway, a Dicer-independent pathway suppressing retrotransposons in the germline. Using genetic models, we will explore unique and redundant roles of both pathways in the germline. D-FENS will uncover physiological significance of the N-terminal part of Dicer, fundamentally improve understanding RNAi function in the germline, and provide a critical in vivo assessment of antiviral activity of RNAi with implications for human therapy.

1 950 000 €

Start date: 2015-07-01, End date: 2020-06-30