skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.


Title: Learning to find proofs and theorems by learning to refine search strategies
We propose a new approach to automated theorem proving where an AlphaZero-style agent is self-training to refine a generic high-level expert strategy expressed as a nondeterministic program. An analogous teacher agent is self-training to generate tasks of suitable relevance and difficulty for the learner. This allows leveraging minimal amounts of domain knowledge to tackle problems for which training data is unavailable or hard to synthesize. As a specific illustration, we consider loop invariant synthesis for imperative programs and use neural networks to refine both the teacher and solver strategies.  more » « less
Award ID(s):
1739629
PAR ID:
10374037
Author(s) / Creator(s):
;
Editor(s):
Agarwal, Alekh; Belgrave, Danielle; Cho, Kyunghyun; Oh, Alice
Date Published:
Journal Name:
Advances in neural information processing systems
Volume:
35
ISSN:
1049-5258
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. Vision-based urban driving is hard. The autonomous system needs to learn to perceive the world and act in it. We show that this challenging learning problem can be simplified by decomposing it into two stages. We first train an agent that has access to privileged information. This privileged agent cheats by observing the ground-truth layout of the environment and the positions of all traffic participants. In the second stage, the privileged agent acts as a teacher that trains a purely vision-based sensorimotor agent. The resulting sensorimotor agent does not have access to any privileged information and does not cheat. This two-stage training procedure is counter-intuitive at first, but has a number of important advantages that we analyze and empirically demonstrate. We use the presented approach to train a vision-based autonomous driving system that substantially outperforms the state of the art on the CARLA benchmark and the recent NoCrash benchmark. Our approach achieves, for the first time, 100% success rate on all tasks in the original CARLA benchmark, sets a new record on the NoCrash benchmark, and reduces the frequency of infractions by an order of magnitude compared to the prior state of the art. 
    more » « less
  2. The options for Artificial intelligence (AI) tools used in teacher education are increasing daily, but more is only sometimes better for teachers working in already complex classroom settings. This team discusses the increase of AI in schools and provides an example from administrators, teacher educators, and computer scientists of an AI virtual agent and the research to support student learning and teachers in classroom settings. The authors discuss the creation and potential of virtual characters in elementary classrooms, combined with biometrics and facial emotional recognition, which in this study has impacted student learning and offered support to the teacher. The researchers share the development of the AI agent, the lessons learned, the integration of biometrics and facial tracking, and how teachers use this emerging form of AI both in classroom-based center activities and to support students’ emotional regulation. The authors conclude by describing the application of this type of support in teacher preparation programs and a vision of the future of using AI agents in instruction. 
    more » « less
  3. Real-world robotics applications demand object pose estimation methods that work reliably across a variety of scenarios. Modern learning-based approaches require large labeled datasets and tend to perform poorly outside the training domain. Our first contribution is to develop a robust corrector module that corrects pose estimates using depth information, thus enabling existing methods to better generalize to new test domains; the corrector operates on semantic keypoints (but is also applicable to other pose estimators) and is fully differentiable. Our second contribution is an ensemble self-training approach that simultaneously trains multiple pose estimators in a self-supervised manner. Our ensemble self-training architecture uses the robust corrector to refine the output of each pose estimator; then, it evaluates the quality of the outputs using observable correctness certificates; finally, it uses the observably correct outputs for further training, without requiring external supervision. As an additional contribution, we propose small improvements to a regression-based keypoint detection architecture, to enhance its robustness to outliers; these improvements include a robust pooling scheme and a robust centroid computation. Experiments on the YCBV and TLESS datasets show the proposed ensemble self-training outperforms fully supervised baselines while not requiring 3D annotations on real data. 
    more » « less
  4. Abstract Teacher leaders influence their peers by introducing innovative instructional methods and enhancing teaching quality. They have proven invaluable to school principals as they prioritize comprehensive teacher development, bolster teacher effectiveness, and promote teacher retention. Despite their importance, little to no research—prior to the present study—has shed light on the development of teacher leaders and the evolution of their leadership identity. While science, technology, engineering, and mathematics (STEM) teacher leaders offer a potential remedy for attrition in public schools, a substantial gap exists in understanding how a STEM teacher's self‐efficacy, values, and agency contribute to their transformation into effective STEM teacher leaders, especially in urban‐like learning environments. The present study focuses on STEM teacher leadership identity development and the challenges encountered. It ascertains the interplay between urban‐like learning environments, self‐efficacy, agency, the teacher leader's role within the school, and values in forecasting STEM teacher leadership identity. This research involved 100 in‐service PreK‐12 public school STEM teacher leaders. It yielded significant, positive, and meaningful relations between urban‐like learning environments, self‐efficacy/agency, teacher leader role, values, and STEM teacher leadership identity. These findings can enhance various facets of PreK‐12 STEM education, including educational programming, teacher training, and cultivating STEM teacher leadership. 
    more » « less
  5. Pre-trained code language models have achieved promising performance in code generation and improved the programming efficiency of human developers. However, their self-refinement capability is typically overlooked by the existing evaluations of code LMs, which focus only on the accuracy of the one-time prediction. For the cases when code LMs fail to implement the correct program, developers actually find it hard to debug and fix the faulty prediction since it is not written by the developers themselves. Unfortunately, our study reveals that code LMs cannot efficiently self-refine their faulty generations as well. In this paper, we propose CYCLE framework, learning to self-refine the faulty generation according to the available feedback, such as the execution results reported by the test suites. We evaluate CYCLE on three popular code generation benchmarks, HumanEval, MBPP, and APPS. The results reveal that CYCLE successfully maintains, sometimes improves, the quality of one-time code generation, while significantly improving the self-refinement capability of code LMs. We implement four variants of CYCLE with varied numbers of parameters across 350M, 1B, 2B, and 3B, and the experiments show that CYCLE consistently boosts the code generation performance, by up to 63.5 
    more » « less