Xiaokai Zhang

Global energy challenges establish building‐integrated photovoltaics as a pivotal decarbonization frontier, where semitransparent organic photovoltaics (ST‐OPVs) represent a promising technology for simultaneous power generation and daylight transmission. However, their widespread application is constrained by a fundamental efficiency and transparency trade‐off governed by complex photon management. Herein, we introduce a physics‐enhanced deep learning (PDL) framework that embeds optical physical priors into neural network, significantly reducing the reliance on extensive experimental datasets while enhancing predictive accuracy beyond conventional simulation and purely data driven methods. Building on a novel halogen‐additive engineering strategy, that enables opaque devices with a power conversion efficiency exceeding 20%, our PDL‐guided optimal optical design delivers corresponding ST‐OPVs with a record light utilization efficiency of 6.09%. When scaled to large‐area manufactured modules, multi‐scale building energy modeling demonstrates that the nationwide deployment of such ST‐OPVs could meet up to one‐fifth of China's total energy demand, highlighting their transformative potential in advancing sustainable energy systems and supporting global carbon neutrality goals.

Euclidean plane geometry problem solving is a challenging benchmark for artificial intelligence because it requires complex diagram understanding, symbolic deduction, and multi-step reasoning. Constructing effective datasets for this task requires geometric instances that are realizable, non-degenerate, structurally diverse, and paired with human-like proofs. However, existing random or template-based generation pipelines often produce redundant, singular, or infeasible candidates, causing substantial computation to be spent before useful reasoning trajectories can be extracted. To address these limitations, we present FGeo-GCG, a hybrid geometric data synthesis framework built on the FormalGeo-V2 deductive engine. It formulates Geometric Configuration Generation as an incremental linear construction process that decomposes global constraint satisfaction into local construction steps, thereby pruning invalid branches during the generation process. To improve reliability and efficiency, FGeo-GCG combines two validation stages: a safe stochastic Jacobian-rank filter estimates whether local candidate constraints contribute independent algebraic restrictions, and progressive geometric validation checks whether the resulting partial construction remains realizable and non-degenerate. By encoding incidence-, metric-, and symmetry-related dependencies within unified constraint graphs, the framework also connects geometric data synthesis with structural symmetry analysis. Validated constraint graphs are then converted into problem instances through forward deduction, goal decomposition, and multi-dimensional complexity filtering, producing proof targets without manual annotation. Experiments show that the full validation pipeline reduces the failure rate for highly constrained instances. The resulting FGeo-GCG dataset contains more than 50,000 formally validated plane geometric configurations and provides engine-derived reasoning traces and targets for future training and evaluation of neuro-symbolic geometry problem-solving systems.

Geometric problem-solving has always been a great challenge in the field of deductive reasoning and artificial intelligence. Symmetry is a defining characteristic of geometric shapes and properties. Consequently, the application of symmetry principles to geometric reasoning arises as a natural choice. To address the efficiency degradation and limited generalization, we propose FGeo-ISRL, a neural-symbolic inverse search framework whose core is the synergistic integration of a task-fine-tuned large language model and Monte Carlo Tree Search. Under the formal framework of FormalGeo, geometric theorems are iteratively applied starting from the given conditions and the target conclusion, in order to infer the necessary supporting premises. The large language model simultaneously serves as a policy network and a value network, guiding theorem application decisions and evaluating intermediate proof states, whereas the Monte Carlo Tree Search performs structured exploration over the state space, both training for policy refinement and inference for online search. The reinforcement learning agent is trained with a hybrid reward scheme, combining immediate feedback from the value difference and a sparse success reward. Experiments demonstrate the effectiveness and correctness of FGeo-ISRL. It not only achieves a Single-Step Theorem Accuracy of 90.2% and a Geometric Problem-Solving Accuracy of 83.14%, but also ensures that every step of the proof process remains readable, verifiable, and traceable.

Geometric problem-solving (GPS) has been a long-standing challenge in the fields of formal mathematics and artificial intelligence. To address the limitations of unidirectional approaches, we developed a neuro-symbolic system that integrates forward and backward reasoning. The neural component employs a gating-enhanced attention network to select candidate theorems, guiding the heuristic search and pruning irrelevant branches. The symbolic component is a bidirectional solver built on FormalGeo, which performs rigorous geometric relational reasoning and algebraic computation. The neural component predicts the theorems based on the current problem state, while the symbolic component applies these theorems and updates the problem state. These two parts interact iteratively until the problem is solved. The solving process is organized as a graph structure where facts and goals serve as nodes and theorems as edges, thereby generating a human-readable solution. The proposed neuro-symbolic system achieved an 89.63% problem-solving success rate (PSSR) on the FormalGeo7K dataset, surpassing the previous best result.

Plane geometry problem solving has been a long-term challenge in mathematical reasoning and symbolic artificial intelligence. With the continued advancement of automated methods, the need for large-scale datasets and rigorous evaluation frameworks has become increasingly critical for benchmarking and guiding system development. However, existing resources often lack sufficient scale, systematic difficulty modeling, and quantifiable, process-based evaluation metrics. To address these limitations, we propose FGeo-Eval, a comprehensive evaluation system for plane geometry problem solving, and introduce the FormalGeo30K dataset, an extended dataset derived from FormalGeo7K. The evaluation system includes a problem completion rate metric PCR to assess partial progress, theorem weight computation to quantify knowledge importance, and a difficulty coefficient based on reasoning complexity. By analyzing problem structures and solution dependencies, this system enables fine-grained difficulty stratification and objective performance measurement. Concurrently, FormalGeo30K expands the dataset to 30,540 formally annotated problems, supporting more robust model training and evaluation. Experimental results demonstrate that the proposed metrics effectively evaluate problem difficulty and assess solver capabilities. With the augmented dataset, the average success rate across all difficulty levels for the FGeo-HyperGNet model increases from 77.43% to 85.01%, while the average PCR increases from 88.57% to 91.79%. These contributions provide essential infrastructure for advancing plane geometry reasoning systems, offering standardized benchmarks for model development and guiding optimization of geometry-solving models.

Automatic geometric problem-solving is an active and challenging subfield at the intersection of AI and mathematics, where geometric problem parsing plays a critical role. It involves converting geometric diagram and text into certain formal language. Due to the complexity of geometric shapes and the diversity of geometric relationships, geometric problem parsing demands that the parser exhibit cross-modal comprehension and reasoning capabilities. In this paper, we propose an enhanced geometric problem parsing method called FGeo-Parser, which converts problem diagrams and text into the formal language of the FormalGeo. It also supports reverse formalization to generate human-like solutions, reflecting the symmetry between parsing and generating. Specifically, diagram parser leverages the BLIP to generate the construction CDL and image CDL, while text parser employs the T5 to produce the text CDL and goal CDL where these neural networks are both based on a symmetric encoder–decoder architecture. With the assistance of a theorem predictor, these CDLs were automatically parsed and step-by-step reasoning was executed within FGPS. Finally, the reasoning process was input into a solution generator, which subsequently produced a human-like solution process. Additionally, we re-annotated problem diagrams and text based on the FormalGeo7K dataset. The formalization experiments on the new dataset achieved a match accuracy of 91.51% and a perfect accuracy of 56.47%, while the combination with the theorem predictor achieved a problem-solving accuracy of 63.45%.

Human-like automatic deductive reasoning has always been one of the most challenging open problems in the interdisciplinary field of mathematics and artificial intelligence. This paper is the third in a series of our works. We built a neural-symbolic system, named FGeo-DRL, to automatically perform human-like geometric deductive reasoning. The neural part is an AI agent based on deep reinforcement learning, capable of autonomously learning problem-solving methods from the feedback of a formalized environment, without the need for human supervision. It leverages a pre-trained natural language model to establish a policy network for theorem selection and employ Monte Carlo Tree Search for heuristic exploration. The symbolic part is a reinforcement learning environment based on geometry formalization theory and FormalGeo, which models geometric problem solving (GPS) as a Markov Decision Process (MDP). In the formal symbolic system, the symmetry of plane geometric transformations ensures the uniqueness of geometric problems when converted into states. Finally, the known conditions and objectives of the problem form the state space, while the set of theorems forms the action space. Leveraging FGeo-DRL, we have achieved readable and verifiable automated solutions to geometric problems. Experiments conducted on the formalgeo7k dataset have achieved a problem-solving success rate of 86.40%.

The application of contemporary artificial intelligence techniques to address geometric problems and automated deductive proofs has always been a grand challenge to the interdisciplinary field of mathematics and artificial intelligence. This is the fourth article in a series of our works, in our previous work, we established a geometric formalized system known as FormalGeo. Moreover, we annotated approximately 7000 geometric problems, forming the FormalGeo7k dataset. Despite the fact that FGPS (Formal Geometry Problem Solver) can achieve interpretable algebraic equation solving and human-like deductive reasoning, it often experiences timeouts due to the complexity of the search strategy. In this paper, we introduced FGeo-TP (theorem predictor), which utilizes the language model to predict the theorem sequences for solving geometry problems. The encoder and decoder components in the transformer architecture naturally establish a mapping between the sequences and embedding vectors, exhibiting inherent symmetry. We compare the effectiveness of various transformer architectures, such as BART or T5, in theorem prediction, and implement pruning in the search process of FGPS, thereby improving its performance when solving geometry problems. Our results demonstrate a significant increase in the problem-solving rate of the language model-enhanced FGeo-TP on the FormalGeo7k dataset, rising from 39.7% to 80.86%. Furthermore, FGeo-TP exhibits notable reductions in solution times and search steps across problems of varying difficulty levels.

Geometric problem solving (GPS) has always been a long-standing challenge in the fields of automated reasoning. Its problem representation and solution process embody rich symmetry. This paper is the second in a series of our works. Based on the Geometry Formalization Theory and the FormalGeo geometric formal system, we have developed the Formal Geometric Problem Solver (FGPS) in Python 3.10, which can serve as an interactive assistant or as an automated problem solver. FGPS is capable of executing geometric predicate logic and performing relational reasoning and algebraic computation, ultimately achieving readable, traceable, and verifiable automated solutions for geometric problems. We observed that symmetry phenomena exist at various levels within FGPS and utilized these symmetries to further refine the system’s design. FGPS employs symbols to represent geometric shapes and transforms various geometric patterns into a set of symbolic operation rules. This maintains symmetry in basic transformations, shape constructions, and the application of theorems. Moreover, we also have annotated the formalgeo7k dataset, which contains 6981 geometry problems with detailed formal language descriptions and solutions. Experiments on formalgeo7k validate the correctness and utility of the FGPS. The forward search method with random strategy achieved a 39.71% problem-solving success rate.